logo

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 (
    Add, Neg, Mult, frac, Exp, 
    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))
unary_add_reduction (conjecture without proof):
In [4]:
add_zero_closure_bin = Forall((a, b), InSet(Add(a, b), ZeroSet), domain=ZeroSet)
add_zero_closure_bin (conjecture without proof):
In [5]:
add_zero_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),ZeroSet), domain = ZeroSet), domain=Natural)
add_zero_closure (conjecture without proof):
In [6]:
add_int_closure_bin = Forall((a, b), InSet(Add(a, b), Integer), domain=Integer)
add_int_closure_bin (conjecture without proof):
In [7]:
add_int_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Integer), domain = Integer), domain=Natural)
add_int_closure (conjecture without proof):
In [8]:
add_nat_closure_bin = Forall((a, b), InSet(Add(a, b), Natural), domain=Natural)
add_nat_closure_bin (conjecture without proof):
In [9]:
add_nat_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), Natural), domain=Natural), domain = Natural)
add_nat_closure (conjecture without proof):
In [10]:
add_nat_pos_closure_bin = Forall((a, b), InSet(Add(a, b), NaturalPos), domain=NaturalPos)
add_nat_pos_closure_bin (conjecture without proof):
In [11]:
add_nat_pos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), NaturalPos), domain=NaturalPos), domain = NaturalPos)
add_nat_pos_closure (conjecture without proof):
In [12]:
add_int_neg_closure_bin = Forall((a, b), InSet(Add(a, b), IntegerNeg), domain=IntegerNeg)
add_int_neg_closure_bin (conjecture without proof):
In [13]:
add_int_neg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), IntegerNeg), domain=IntegerNeg), domain = NaturalPos)
add_int_neg_closure (conjecture without proof):
In [14]:
add_int_nonpos_closure_bin = Forall((a, b), InSet(Add(a, b), IntegerNonPos), domain=IntegerNonPos)
add_int_nonpos_closure_bin (conjecture without proof):
In [15]:
add_int_nonpos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), IntegerNonPos), domain=IntegerNonPos), domain = Natural)
add_int_nonpos_closure (conjecture without proof):
In [16]:
add_nat_pos_from_nonneg = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j), 
                                            InSet(Add(a_1_to_i, b, c_1_to_j), NaturalPos), 
                                            domain=Natural, 
                                            condition=greater(b, zero)), 
                             domain=Natural)
add_nat_pos_from_nonneg (conjecture without proof):
In [17]:
add_int_neg_from_nonpos = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j), 
                                            InSet(Add(a_1_to_i, b, c_1_to_j), IntegerNeg), 
                                            domain=IntegerNonPos, 
                                            condition=Less(b, zero)), 
                             domain=Natural)
add_int_neg_from_nonpos (conjecture without proof):
In [18]:
add_rational_closure_bin = Forall((a, b), InSet(Add(a, b), Rational), domain=Rational)
add_rational_closure_bin (conjecture without proof):
In [19]:
add_rational_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Rational), domain=Rational), 
                        domain=Natural)
add_rational_closure (conjecture without proof):
In [20]:
add_rational_nonneg_closure_bin = Forall((a, b), InSet(Add(a, b), RationalNonNeg), domain=RationalNonNeg)
add_rational_nonneg_closure_bin (conjecture without proof):
In [21]:
add_rational_nonneg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RationalNonNeg), 
                                        domain=RationalNonNeg), 
                              domain=Natural)
add_rational_nonneg_closure (conjecture without proof):
In [22]:
add_rational_nonpos_closure_bin = Forall((a, b), InSet(Add(a, b), RationalNonPos), domain=RationalNonPos)
add_rational_nonpos_closure_bin (conjecture without proof):
In [23]:
add_rational_nonpos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RationalNonPos), 
                                        domain=RationalNonPos), 
                              domain=Natural)
add_rational_nonpos_closure (conjecture without proof):
In [24]:
add_rational_pos_closure_bin = Forall((a, b), InSet(Add(a, b), RationalPos), domain=RationalPos)
add_rational_pos_closure_bin (conjecture without proof):
In [25]:
add_rational_pos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),RationalPos), domain=RationalPos), 
                        domain=Natural)
add_rational_pos_closure (conjecture without proof):
In [26]:
add_rational_neg_closure_bin = Forall((a, b), InSet(Add(a, b), RationalNeg), domain=RationalPos)
add_rational_neg_closure_bin (conjecture without proof):
In [27]:
add_rational_neg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),RationalNeg), domain=RationalNeg), 
                        domain=NaturalPos)
add_rational_neg_closure (conjecture without proof):
In [28]:
add_rational_pos_from_nonneg = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j), 
                                                     InSet(Add(a_1_to_i, b, c_1_to_j), RationalPos), 
                                             domain=RationalNonNeg, 
                                             condition=greater(b, zero)), 
                              domain=Natural)
add_rational_pos_from_nonneg (conjecture without proof):
In [29]:
add_rational_neg_from_nonpos = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j), 
                                                     InSet(Add(a_1_to_i, b, c_1_to_j), RationalNeg), 
                                             domain=RationalNonPos, 
                                             condition=Less(b, zero)), 
                              domain=Natural)
add_rational_neg_from_nonpos (conjecture without proof):
In [30]:
add_real_closure_bin = Forall((a, b), InSet(Add(a, b), Real), domain=Real)
add_real_closure_bin (conjecture without proof):
In [31]:
add_real_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Real), domain=Real), 
                        domain=Natural)
add_real_closure (conjecture without proof):
In [32]:
add_real_nonneg_closure_bin = Forall((a, b), InSet(Add(a, b), RealNonNeg), domain=RealNonNeg)
add_real_nonneg_closure_bin (conjecture without proof):
In [33]:
add_real_nonneg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RealNonNeg), 
                                        domain=RealNonNeg), 
                              domain=Natural)
add_real_nonneg_closure (conjecture without proof):
In [34]:
add_real_nonpos_closure_bin = Forall((a, b), InSet(Add(a, b), RealNonPos), domain=RealNonPos)
add_real_nonpos_closure_bin (conjecture without proof):
In [35]:
add_real_nonpos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RealNonPos), 
                                        domain=RealNonPos), 
                              domain=Natural)
add_real_nonpos_closure (conjecture without proof):
In [36]:
add_real_pos_closure_bin = Forall((a, b), InSet(Add(a, b), RealPos), domain=RealPos)
add_real_pos_closure_bin (conjecture without proof):
In [37]:
add_real_pos_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),RealPos), domain=RealPos), 
                        domain=NaturalPos)
add_real_pos_closure (conjecture without proof):
In [38]:
add_real_neg_closure_bin = Forall((a, b), InSet(Add(a, b), RealNeg), domain=RealNeg)
add_real_neg_closure_bin (conjecture without proof):
In [39]:
add_real_neg_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i), RealNeg), domain=RealNeg), 
                        domain=NaturalPos)
add_real_neg_closure (conjecture without proof):
In [40]:
add_real_pos_from_nonneg = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j), 
                                             InSet(Add(a_1_to_i, b, c_1_to_j), RealPos), 
                                             domain=RealNonNeg, 
                                             condition=greater(b, zero)), 
                              domain=Natural)
add_real_pos_from_nonneg (conjecture without proof):
In [41]:
add_real_neg_from_nonpos = Forall((i, j), Forall((a_1_to_i, b, c_1_to_j), 
                                             InSet(Add(a_1_to_i, b, c_1_to_j), RealNeg), 
                                             domain=RealNonPos, 
                                             condition=Less(b, zero)), 
                              domain=Natural)
add_real_neg_from_nonpos (conjecture without proof):
In [42]:
add_complex_closure_bin = Forall((a, b), InSet(Add(a, b), Complex), domain=Complex)
add_complex_closure_bin (conjecture without proof):
In [43]:
add_complex_closure = Forall(i, Forall(a_1_to_i, InSet(Add(a_1_to_i),Complex), domain = Complex), domain=Natural)
add_complex_closure (conjecture without proof):

Adding fractions

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

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)
left_add_eq_nat (conjecture without proof):
In [46]:
left_add_eq_int = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Integer)
left_add_eq_int (conjecture without proof):
In [47]:
left_add_eq_rational = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Rational)
left_add_eq_rational (conjecture without proof):
In [48]:
left_add_eq_real = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Real)
left_add_eq_real (conjecture without proof):
In [49]:
left_add_eq = Forall((a, x, y), Equals(Add(a, x), Add(a, y)), condition=Equals(x, y), domain=Complex)
left_add_eq (conjecture without proof):
In [50]:
right_add_eq_nat = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Natural)
right_add_eq_nat (conjecture without proof):
In [51]:
right_add_eq_int = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Integer)
right_add_eq_int (conjecture without proof):
In [52]:
right_add_eq_rational = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Rational)
right_add_eq_rational (conjecture without proof):
In [53]:
right_add_eq_real = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Real)
right_add_eq_real (conjecture without proof):
In [54]:
right_add_eq = Forall((a, x, y), Equals(Add(x, a), Add(y, a)), condition=Equals(x, y), domain=Complex)
right_add_eq (conjecture without proof):
In [55]:
left_add_neq_nat = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Natural)
left_add_neq_nat (conjecture without proof):
In [56]:
left_add_neq_int = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Integer)
left_add_neq_int (conjecture without proof):
In [57]:
left_add_neq_rational = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Rational)
left_add_neq_rational (conjecture without proof):
In [58]:
left_add_neq_real = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Real)
left_add_neq_real (conjecture without proof):
In [59]:
left_add_neq = Forall((a, x, y), NotEquals(Add(a, x), Add(a, y)), condition=NotEquals(x, y), domain=Complex)
left_add_neq (conjecture without proof):
In [60]:
right_add_neq_nat = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Natural)
right_add_neq_nat (conjecture without proof):
In [61]:
right_add_neq_int = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Integer)
right_add_neq_int (conjecture without proof):
In [62]:
right_add_neq_rational = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Rational)
right_add_neq_rational (conjecture without proof):
In [63]:
right_add_neq_real = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Real)
right_add_neq_real (conjecture without proof):
In [64]:
right_add_neq = Forall((a, x, y), NotEquals(Add(x, a), Add(y, a)), condition=NotEquals(x, y), domain=Complex)
right_add_neq (conjecture without proof):
In [65]:
strong_bound_via_right_term_bound = (
    Forall((a, x, y), Less(Add(a, x), Add(a, y)), condition=Less(x, y), domain=Real))
strong_bound_via_right_term_bound (conjecture without proof):
In [66]:
strong_bound_via_left_term_bound = (
    Forall((a, x, y), Less(Add(x, a), Add(y, a)), condition=Less(x, y), domain=Real))
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),
                                         Less(Add(a_1_to_i, x, b_1_to_j), Add(a_1_to_i, y, 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 = (
    Forall((a, x, y), LessEq(Add(a, x), Add(a, y)), condition=LessEq(x, y), domain=Real))
weak_bound_via_right_term_bound (conjecture without proof):
In [69]:
weak_bound_via_left_term_bound = (
    Forall((a, x, y), LessEq(Add(x, a), Add(y, a)), condition=LessEq(x, y), domain=Real))
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),
                                         LessEq(Add(a_1_to_i, x, b_1_to_j), Add(a_1_to_i, y, 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), 
                                                                 Add(a_1_to_i, 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), 
                  Forall(b, greater_eq(Add(a_1_to_i, b, c_1_to_j), b),
                         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), 
                         Forall(b, LessEq(Add(a_1_to_i, b, c_1_to_j), b),
                                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), 
                  Forall(b, greater(Add(a_1_to_i, b, c_1_to_j), b),
                         domain=Real),
                  domain=RealPos),
           domain=Natural, condition=greater(Add(i, j), zero))
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), 
                         Forall(b, Less(Add(a_1_to_i, b, c_1_to_j), b),
                                domain=Real),
                         domain=RealNeg), 
           domain=Natural, condition=greater(Add(i, j), zero))
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), 
                         Forall(b, Less(Add(a_1_to_i, b, c_1_to_j), b),
                                domain=Real),
                         domain=RealNeg), 
           domain=Natural)
strictly_decreasing_additions (conjecture without proof):
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), 
                  Equals(Add(a_1_to_i, b, c_1_to_j, d_1_to_k), 
                         Add(a_1_to_i, c_1_to_j, b, 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),
                  Equals(Add(a_1_to_i, b_1_to_j, c, d_1_to_k), 
                         Add(a_1_to_i, c, b_1_to_j, 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), 
                  Equals(Add(a_1_to_i, b_1_to_j, c_1_to_k),
                         Add(a_1_to_i, Add(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), 
                  Equals(Add(a_1_to_i, Add(b_1_to_j), c_1_to_k),
                         Add(a_1_to_i, b_1_to_j, c_1_to_k)) \
                  .with_wrapping_at(2),
                  domain=Complex),
           domain=Natural)
disassociation (conjecture without proof):
In [84]:
%end theorems

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