logo

Theorems (or conjectures) for the theory of proveit.numbers.negation

In [1]:
import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit import ExprRange, IndexedVar
from proveit import a, b, k, n, x, y
from proveit.core_expr_types import x_1_to_n
from proveit.logic import Forall, Equals, NotEquals, InSet
from proveit.numbers import zero, one
from proveit.numbers import ZeroSet, Natural, NaturalPos, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos
from proveit.numbers import Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos
from proveit.numbers import Real, RealNonZero, RealPos, RealNeg, RealNonNeg, RealNonPos
from proveit.numbers import Complex, ComplexNonZero
from proveit.numbers import Add, Div, Neg, subtract, Mult, Exp, Less, LessEq, greater, greater_eq
In [2]:
%begin theorems

Defining theorems for theory 'proveit.numbers.negation'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions
In [3]:
negated_zero = Equals(Neg(zero), zero)
negated_zero (conjecture without proof):
In [4]:
neg_in_zero_set = Forall(a, InSet(Neg(a), ZeroSet), domain=ZeroSet)
neg_in_zero_set (conjecture without proof):
In [5]:
nat_closure = Forall(a, InSet(Neg(a), Natural), domain=IntegerNonPos)
nat_closure (conjecture without proof):
In [6]:
nat_pos_closure = Forall(a, InSet(Neg(a), NaturalPos), domain=IntegerNeg)
nat_pos_closure (conjecture without proof):
In [7]:
int_closure = Forall(a, InSet(Neg(a), Integer), domain=Integer)
int_closure (conjecture without proof):
In [8]:
int_nonzero_closure = Forall(a, InSet(Neg(a), IntegerNonZero), domain=IntegerNonZero)
int_nonzero_closure (conjecture without proof):
In [9]:
int_neg_closure = Forall(a, InSet(Neg(a), IntegerNeg), domain=NaturalPos)
int_neg_closure (conjecture without proof):
In [10]:
int_nonpos_closure = Forall(a, InSet(Neg(a), IntegerNonPos), domain=Natural)
int_nonpos_closure (conjecture without proof):
In [11]:
rational_closure = Forall(a, InSet(Neg(a), Rational), domain=Rational)
rational_closure (conjecture without proof):
In [12]:
rational_nonzero_closure = Forall(a, InSet(Neg(a), RationalNonZero), domain=RationalNonZero)
rational_nonzero_closure (conjecture without proof):
In [13]:
rational_pos_closure = Forall(a, InSet(Neg(a), RationalPos), domain=RationalNeg)
rational_pos_closure (conjecture without proof):
In [14]:
rational_neg_closure = Forall(a, InSet(Neg(a), RationalNeg), domain=RationalPos)
rational_neg_closure (conjecture without proof):
In [15]:
rational_nonneg_closure = Forall(a, InSet(Neg(a), RationalNonNeg), domain=RationalNonPos)
rational_nonneg_closure (conjecture without proof):
In [16]:
rational_nonpos_closure = Forall(a, InSet(Neg(a), RationalNonPos), domain=RationalNonNeg)
rational_nonpos_closure (conjecture without proof):
In [17]:
real_closure = Forall(a, InSet(Neg(a), Real), domain=Real)
real_closure (conjecture without proof):
In [18]:
real_nonzero_closure = Forall(a, InSet(Neg(a), RealNonZero), domain=RealNonZero)
real_nonzero_closure (conjecture without proof):
In [19]:
real_pos_closure = Forall(a, InSet(Neg(a), RealPos), domain=RealNeg)
real_pos_closure (conjecture without proof):
In [20]:
real_neg_closure = Forall(a, InSet(Neg(a), RealNeg), domain=RealPos)
real_neg_closure (conjecture without proof):
In [21]:
real_nonneg_closure = Forall(a, InSet(Neg(a), RealNonNeg), domain=RealNonPos)
real_nonneg_closure (conjecture without proof):
In [22]:
real_nonpos_closure = Forall(a, InSet(Neg(a), RealNonPos), domain=RealNonNeg)
real_nonpos_closure (conjecture without proof):
In [23]:
complex_closure = Forall(a, InSet(Neg(a), Complex), domain=Complex)
complex_closure (conjecture without proof):
In [24]:
complex_nonzero_closure = Forall(a, InSet(Neg(a), ComplexNonZero), domain=ComplexNonZero)
complex_nonzero_closure (conjecture without proof):
In [25]:
negated_positive_is_negative = Forall(a, Less(Neg(a), zero), domain=Real, conditions=[greater(a, zero)])
negated_positive_is_negative (conjecture without proof):
In [26]:
neg_as_mult_one = Forall(x,Equals(Neg(x), Mult(Neg(one), x)), domain=Complex)
neg_as_mult_one (conjecture without proof):
In [27]:
distribute_neg_through_binary_sum = Forall((a, b), Equals(Neg(Add(a, b)), Add(Neg(a), Neg(b))),
                                      domain=Complex)
distribute_neg_through_binary_sum (conjecture without proof):
In [28]:
distribute_neg_through_subtract = Forall((a, b), Equals(Neg(subtract(a, b)), Add(Neg(a), b)),
                                      domain=Complex)
distribute_neg_through_subtract (conjecture without proof):
In [29]:
distribute_neg_through_sum = Forall(n, Forall(x_1_to_n, Equals(Neg(Add(x_1_to_n)),
                                                        Add(ExprRange(k, Neg(IndexedVar(x, k)), one, n))),
                                           domain=Complex), 
                                 domain=NaturalPos)
distribute_neg_through_sum (conjecture without proof):
In [30]:
distribute_neg_through_div_numerator = Forall(
        (x, y),
        Equals(Neg(Div(x, y)), Div(Neg(x), y)),
        domain=Complex,
        conditions=[NotEquals(y, zero)])
distribute_neg_through_div_numerator (conjecture without proof):
In [31]:
neg_not_eq_zero = Forall(a, NotEquals(Neg(a), zero), domain=Complex, conditions=[NotEquals(a, zero)])
neg_not_eq_zero (conjecture without proof):
In [32]:
mult_neg_one_left = Forall(x, Equals(Mult(Neg(one), x), Neg(x)), domain=Complex)
mult_neg_one_left (conjecture without proof):
In [33]:
mult_neg_one_right = Forall(x, Equals(Mult(x, Neg(one)), Neg(x)), domain=Complex)
mult_neg_one_right (conjecture without proof):
In [34]:
neg_times_pos = Forall([x, y], Equals(Mult(Neg(x), y), Neg(Mult(x, y))), domain=Complex)
neg_times_pos (conjecture without proof):
In [35]:
pos_times_neg = Forall([x, y], Equals(Mult(x, Neg(y)), Neg(Mult(x, y))), domain=Complex)
pos_times_neg (conjecture without proof):
In [36]:
neg_times_neg = Forall([x, y], Equals(Mult(Neg(x), Neg(y)), Mult(x, y)), domain=Complex)
neg_times_neg (conjecture without proof):
In [37]:
double_negation = Forall(x, Equals(Neg(Neg(x)), x), domain=Complex)
double_negation (conjecture without proof):
In [38]:
negated_weak_bound = Forall((x, y), greater_eq(Neg(x), Neg(y)),
                            condition=LessEq(x, y), domain=Real)
negated_weak_bound (conjecture without proof):
In [39]:
negated_strong_bound = Forall((x, y), greater(Neg(x), Neg(y)),
                              condition=Less(x, y), domain=Real)
negated_strong_bound (conjecture without proof):
In [40]:
%end theorems

These theorems may now be imported from the theory package: proveit.numbers.negation