# Theorems (or conjectures) for the theory of proveit.numbers.addition¶

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.logic import Forall, Equals, NotEquals

from proveit import a, b, c, d, e
from proveit.core_expr_types import (
a_1_to_i, b_1_to_j, c_1_to_j, c_1_to_k, d_1_to_k)
from proveit import a, b, c, d, e, f, g, h, i,j,k, l, m, n, x, y
from proveit.numbers import zero, one, two, three
from proveit.numbers import (
Less, LessEq, greater, greater_eq,
ZeroSet, Natural, NaturalPos,
Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
Rational, RationalNonZero, RationalPos, RationalNeg,
RationalNonNeg, RationalNonPos,
Real, RealNonZero, RealPos, RealNeg, RealNonNeg, RealNonPos,
Complex, ComplexNonZero)
from proveit.logic.sets import InSet

In [2]:
%begin theorems

Defining theorems for theory 'proveit.numbers.addition'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

In [3]:
unary_add_reduction = Forall(a, Equals(Add(a), a))


In [4]:
add_zero_closure_bin = Forall((a, b), InSet(Add(a, b), ZeroSet), domain=ZeroSet)


In [5]:
add_zero_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),ZeroSet), domain = ZeroSet), domain=Natural)


In [6]:
add_int_closure_bin = Forall((a, b), InSet(Add(a, b), Integer), domain=Integer)


In [7]:
add_int_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Integer), domain = Integer), domain=Natural)


In [8]:
add_nat_closure_bin = Forall((a, b), InSet(Add(a, b), Natural), domain=Natural)


In [9]:
add_nat_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), Natural), domain=Natural), domain = Natural)


In [10]:
add_nat_pos_closure_bin = Forall((a, b), InSet(Add(a, b), NaturalPos), domain=NaturalPos)


In [11]:
add_nat_pos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), NaturalPos), domain=NaturalPos), domain = NaturalPos)


In [12]:
add_int_neg_closure_bin = Forall((a, b), InSet(Add(a, b), IntegerNeg), domain=IntegerNeg)


In [13]:
add_int_neg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), IntegerNeg), domain=IntegerNeg), domain = NaturalPos)


In [14]:
add_int_nonpos_closure_bin = Forall((a, b), InSet(Add(a, b), IntegerNonPos), domain=IntegerNonPos)


In [15]:
add_int_nonpos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), IntegerNonPos), domain=IntegerNonPos), domain = Natural)


In [16]:
add_nat_pos_from_nonneg = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j),
domain=Natural,
condition=greater(b, zero)),
domain=Natural)


In [17]:
add_int_neg_from_nonpos = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j),
domain=IntegerNonPos,
condition=Less(b, zero)),
domain=Natural)


In [18]:
add_rational_closure_bin = Forall((a, b), InSet(Add(a, b), Rational), domain=Rational)


In [19]:
add_rational_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Rational), domain=Rational),
domain=Natural)


In [20]:
add_rational_nonneg_closure_bin = Forall((a, b), InSet(Add(a, b), RationalNonNeg), domain=RationalNonNeg)


In [21]:
add_rational_nonneg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RationalNonNeg),
domain=RationalNonNeg),
domain=Natural)


In [22]:
add_rational_nonpos_closure_bin = Forall((a, b), InSet(Add(a, b), RationalNonPos), domain=RationalNonPos)


In [23]:
add_rational_nonpos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RationalNonPos),
domain=RationalNonPos),
domain=Natural)


In [24]:
add_rational_pos_closure_bin = Forall((a, b), InSet(Add(a, b), RationalPos), domain=RationalPos)


In [25]:
add_rational_pos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),RationalPos), domain=RationalPos),
domain=Natural)


In [26]:
add_rational_neg_closure_bin = Forall((a, b), InSet(Add(a, b), RationalNeg), domain=RationalPos)


In [27]:
add_rational_neg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),RationalNeg), domain=RationalNeg),
domain=NaturalPos)


In [28]:
add_rational_pos_from_nonneg = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j),
domain=RationalNonNeg,
condition=greater(b, zero)),
domain=Natural)


In [29]:
add_rational_neg_from_nonpos = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j),
domain=RationalNonPos,
condition=Less(b, zero)),
domain=Natural)


In [30]:
add_real_closure_bin = Forall((a, b), InSet(Add(a, b), Real), domain=Real)


In [31]:
add_real_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Real), domain=Real),
domain=Natural)


In [32]:
add_real_nonneg_closure_bin = Forall((a, b), InSet(Add(a, b), RealNonNeg), domain=RealNonNeg)


In [33]:
add_real_nonneg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RealNonNeg),
domain=RealNonNeg),
domain=Natural)


In [34]:
add_real_nonpos_closure_bin = Forall((a, b), InSet(Add(a, b), RealNonPos), domain=RealNonPos)


In [35]:
add_real_nonpos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RealNonPos),
domain=RealNonPos),
domain=Natural)


In [36]:
add_real_pos_closure_bin = Forall((a, b), InSet(Add(a, b), RealPos), domain=RealPos)


In [37]:
add_real_pos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),RealPos), domain=RealPos),
domain=NaturalPos)


In [38]:
add_real_neg_closure_bin = Forall((a, b), InSet(Add(a, b), RealNeg), domain=RealNeg)


In [39]:
add_real_neg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RealNeg), domain=RealNeg),
domain=NaturalPos)


In [40]:
add_real_pos_from_nonneg = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j),
domain=RealNonNeg,
condition=greater(b, zero)),
domain=Natural)


In [41]:
add_real_neg_from_nonpos = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j),
domain=RealNonPos,
condition=Less(b, zero)),
domain=Natural)


In [42]:
add_complex_closure_bin = Forall((a, b), InSet(Add(a, b), Complex), domain=Complex)


In [43]:
add_complex_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Complex), domain = Complex), domain=Natural)


In [44]:
rational_pair_addition = Forall(
(a, b, c, d), Equals(Add(frac(a, b), frac(c, d)),
Mult(b, d))),
domain=Integer)


### Theorems for number relations¶

In [45]:
left_add_eq_nat = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Natural)


In [46]:
left_add_eq_int = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Integer)


In [47]:
left_add_eq_rational = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Rational)


In [48]:
left_add_eq_real = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Real)


In [49]:
left_add_eq = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Complex)


In [50]:
right_add_eq_nat = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Natural)


In [51]:
right_add_eq_int = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Integer)


In [52]:
right_add_eq_rational = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Rational)


In [53]:
right_add_eq_real = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Real)


In [54]:
right_add_eq = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Complex)


In [55]:
left_add_neq_nat = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Natural)


In [56]:
left_add_neq_int = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Integer)


In [57]:
left_add_neq_rational = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Rational)


In [58]:
left_add_neq_real = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Real)


In [59]:
left_add_neq = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Complex)


In [60]:
right_add_neq_nat = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Natural)


In [61]:
right_add_neq_int = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Integer)


In [62]:
right_add_neq_rational = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Rational)


In [63]:
right_add_neq_real = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Real)


In [64]:
right_add_neq = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Complex)


In [65]:
strong_bound_via_right_term_bound = (

strong_bound_via_right_term_bound (conjecture without proof):

In [66]:
strong_bound_via_left_term_bound = (

strong_bound_via_left_term_bound (conjecture without proof):

In [67]:
strong_bound_via_term_bound = (
Forall((i, j), Forall((x, y), Forall((a_1_to_i, b_1_to_j),
domain=Real, condition=Less(x, y))),
domain=Natural))

strong_bound_via_term_bound (conjecture without proof):

In [68]:
weak_bound_via_right_term_bound = (

weak_bound_via_right_term_bound (conjecture without proof):

In [69]:
weak_bound_via_left_term_bound = (

weak_bound_via_left_term_bound (conjecture without proof):

In [70]:
weak_bound_via_term_bound = (
Forall((i, j), Forall((x, y), Forall((a_1_to_i, b_1_to_j),
domain=Real, condition=LessEq(x, y))),
domain=Natural))

weak_bound_via_term_bound (conjecture without proof):

In [71]:
elim_zero_left = Forall(a, Equals(Add(zero, a), a), domain=Complex)

elim_zero_left (conjecture without proof):

In [72]:
elim_zero_right = Forall(a, Equals(Add(a, zero), a), domain=Complex)

elim_zero_right (conjecture without proof):

In [73]:
elim_zero_any = Forall((i, j), Forall((a_1_to_i, b_1_to_j), Equals(Add(a_1_to_i, zero, b_1_to_j),
domain=Complex),
domain=Natural)

elim_zero_any (conjecture without proof):

In [74]:
term_as_weak_lower_bound = \
Forall((i,j),
Forall((a_1_to_i, c_1_to_j),
domain=Real),
domain=RealNonNeg),
domain=Natural)

term_as_weak_lower_bound (conjecture without proof):

In [75]:
term_as_weak_upper_bound = \
Forall((i,j), Forall((a_1_to_i, c_1_to_j),
domain=Real),
domain=RealNonPos),
domain=Natural)

term_as_weak_upper_bound (conjecture without proof):

In [76]:
term_as_strong_lower_bound = \
Forall((i,j),
Forall((a_1_to_i, c_1_to_j),
domain=Real),
domain=RealPos),

term_as_strong_lower_bound (conjecture without proof):

In [77]:
term_as_strong_upper_bound = \
Forall((i,j), Forall((a_1_to_i, c_1_to_j),
domain=Real),
domain=RealNeg),

term_as_strong_upper_bound (conjecture without proof):

In [78]:
strictly_decreasing_additions = \
Forall((i,j), Forall((a_1_to_i, c_1_to_j),
domain=Real),
domain=RealNeg),
domain=Natural)


In [79]:
commutation = Forall((a, b), Equals(Add(a, b), Add(b, a)), domain=Complex)

commutation (conjecture without proof):

In [80]:
rightward_commutation = \
Forall((i,j,k),
Forall((a_1_to_i,b,c_1_to_j,d_1_to_k),
.with_wrapping_at(2),
domain=Complex),
domain=Natural)

rightward_commutation (conjecture without proof):

In [81]:
leftward_commutation = \
Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c,d_1_to_k),
.with_wrapping_at(2),
domain = Complex),
domain = Natural)

leftward_commutation (conjecture without proof):

In [82]:
association = \
Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c_1_to_k),
.with_wrapping_at(2),
domain=Complex),
domain=Natural)

association (conjecture without proof):

In [83]:
disassociation = \
Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c_1_to_k),

%end theorems

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