Theorems (or conjectures) for the theory of proveit.numbers.multiplication¶
In [1]:
import proveit
## 72 spaces ===========================================================
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
theory = proveit.Theory('.') # adds theory root to sys.path if necessary
from proveit import ExprTuple, ExprRange, IndexedVar
from proveit import a, b, c, d, f, i, j, k, n, x, y, Q, S
from proveit.core_expr_types import (
a_1_to_i, a_1_to_n, b_1_to_j, c_1_to_j, c_1_to_k, d_1_to_k)
from proveit.logic import Or, Forall, Set, InSet, Equals, NotEquals, Implies, Boolean
from proveit.numbers import (ZeroSet, Natural, NaturalPos, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
Rational, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos, RationalNonZero,
Real, RealPos, RealNeg, RealNonNeg, RealNonPos, RealNonZero,
Complex, ComplexNonZero)
from proveit.numbers import (Mult, Neg, Add, subtract, Abs, Sum, num, zero, one, two, Exp,
Less, LessEq, greater, greater_eq)
from proveit.numbers.summation import summation_b1toj_fQ
from proveit._core_.expression.operation import Function
In [2]:
%begin theorems
In [3]:
unary_mult_reduction = Forall(a, Equals(Mult(a), a))
In [4]:
mult_def_rev = \
Forall((n, x), Forall(a_1_to_n,
Equals(Add(a_1_to_n), Mult(x, n)),
domain=Set(x)),
domains=(Natural, Complex))
In [5]:
repeated_addition_to_mult = Forall((n, x), Equals(Add(ExprRange(k, x, one, n)),
Mult(x, n)),
domains=(Natural, Complex))
In [6]:
mult_in_zero_set_bin = Forall((a, b), InSet(Mult(a, b), ZeroSet), domain=Complex,
condition=Or(Equals(a, zero), Equals(b, zero)))
In [7]:
mult_in_zero_set = Forall(
n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), ZeroSet), domain=Complex,
condition=Or(*ExprTuple(a_1_to_n).map_elements(lambda x : Equals(x, zero)))),
domain=Natural)
In [8]:
mult_nat_closure_bin = Forall((a, b), InSet(Mult(a, b), Natural), domain=Natural)
In [9]:
mult_nat_from_double_nonpos = Forall((a, b), InSet(Mult(a, b), Natural),
domain=IntegerNonPos)
In [10]:
mult_nat_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), Natural),
domain=Natural),
domain=Natural)
In [11]:
mult_nat_pos_closure_bin = Forall((a, b), InSet(Mult(a, b), NaturalPos), domain=NaturalPos)
In [12]:
mult_nat_pos_from_double_neg = Forall((a, b), InSet(Mult(a, b), Natural),
domain=IntegerNeg)
In [13]:
mult_nat_pos_closure = \
Forall(n, Forall(a_1_to_n,
InSet(Mult(a_1_to_n), NaturalPos),
domain=NaturalPos),
domain=Natural)
In [14]:
mult_int_closure_bin = Forall((a, b), InSet(Mult(a, b), Integer), domain=Integer)
In [15]:
mult_int_neg_from_left_neg = Forall((a, b), InSet(Mult(a, b), IntegerNeg),
domains=(IntegerNeg, NaturalPos))
In [16]:
mult_int_neg_from_right_neg = Forall((a, b), InSet(Mult(a, b), IntegerNeg),
domains=(NaturalPos, IntegerNeg))
In [17]:
mult_int_nonpos_from_left_nonpos = Forall((a, b), InSet(Mult(a, b), IntegerNonPos),
domains=(IntegerNonPos, Natural))
In [18]:
mult_int_nonpos_from_right_nonpos = Forall((a, b), InSet(Mult(a, b), IntegerNonPos),
domains=(Natural, IntegerNonPos))
In [19]:
mult_int_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), Integer),
domain=Integer),
domain=Natural)
In [20]:
mult_int_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), IntegerNonZero),
domain=IntegerNonZero)
In [21]:
mult_int_nonzero_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), IntegerNonZero),
domain=IntegerNonZero),
domain=Natural)
In [22]:
mult_rational_closure_bin = Forall((a, b), InSet(Mult(a, b), Rational),
domain=Rational)
In [23]:
mult_rational_closure = \
Forall(n, Forall(a_1_to_n,
InSet(Mult(a_1_to_n), Rational),
domain=Rational),
domain=Natural)
In [24]:
mult_rational_pos_closure_bin = Forall((a, b), InSet(Mult(a, b), RationalPos),
domain=RationalPos)
In [25]:
mult_rational_pos_from_double_neg = Forall((a, b), InSet(Mult(a, b), RationalPos),
domain=RationalNeg)
In [26]:
mult_rational_neg_from_left_neg = Forall((a, b), InSet(Mult(a, b), RationalNeg),
domains=(RationalNeg, RationalPos))
In [27]:
mult_rational_neg_from_right_neg = Forall((a, b), InSet(Mult(a, b), RationalNeg),
domains=(RationalPos, RationalNeg))
In [28]:
mult_rational_pos_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), RationalPos),
domain=RationalPos),
domain=Natural)
In [29]:
mult_rational_nonneg_closure_bin = Forall((a, b), InSet(Mult(a, b), RationalNonNeg),
domain=RationalNonNeg)
In [30]:
mult_rational_nonneg_from_double_nonpos = Forall((a, b), InSet(Mult(a, b), RationalNonNeg), domain=RationalNonPos)
In [31]:
mult_rational_nonpos_from_left_nonpos = Forall((a, b), InSet(Mult(a, b), RationalNonPos),
domains=(RationalNonPos, RationalNonNeg))
In [32]:
mult_rational_nonpos_from_right_nonpos = Forall((a, b), InSet(Mult(a, b), RationalNonPos),
domains=(RationalNonNeg, RationalNonPos))
In [33]:
mult_rational_nonneg_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RationalNonNeg),
domain=RationalNonNeg), domain=Natural)
In [34]:
mult_rational_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), RationalNonZero),
domain=RationalNonZero)
In [35]:
mult_rational_nonzero_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RationalNonZero),
domain=RationalNonZero),
domain=Natural)
In [36]:
mult_real_closure_bin = Forall((a, b), InSet(Mult(a, b), Real), domain=Real)
In [37]:
mult_real_closure = \
Forall(n, Forall(a_1_to_n,
InSet(Mult(a_1_to_n), Real),
domain=Real),
domain=Natural)
In [38]:
mult_real_pos_closure_bin = Forall((a, b), InSet(Mult(a, b), RealPos), domain=RealPos)
In [39]:
mult_real_pos_from_double_neg = Forall((a, b), InSet(Mult(a, b), RealPos), domain=RealNeg)
In [40]:
mult_real_neg_from_left_neg = Forall((a, b), InSet(Mult(a, b), RealNeg), domains=(RealNeg, RealPos))
In [41]:
mult_real_neg_from_right_neg = Forall((a, b), InSet(Mult(a, b), RealNeg), domains=(RealPos, RealNeg))
In [42]:
mult_real_pos_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), RealPos),
domain=RealPos),
domain=Natural)
In [43]:
mult_real_nonneg_closure_bin = Forall((a, b), InSet(Mult(a, b), RealNonNeg), domain=RealNonNeg)
In [44]:
mult_real_nonneg_from_double_nonpos = Forall((a, b), InSet(Mult(a, b), RealNonNeg), domain=RealNonPos)
In [45]:
mult_real_nonpos_from_left_nonpos = Forall((a, b), InSet(Mult(a, b), RealNonPos), domains=(RealNonPos, RealNonNeg))
In [46]:
mult_real_nonpos_from_right_nonpos = Forall((a, b), InSet(Mult(a, b), RealNonPos), domains=(RealNonNeg, RealNonPos))
In [47]:
mult_real_nonneg_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RealNonNeg),
domain=RealNonNeg),
domain=Natural)
In [48]:
mult_real_nonzero_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RealNonZero),
domain=RealNonZero),
domain=Natural)
In [49]:
mult_real_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), RealNonZero),
domain=RealNonZero)
In [50]:
mult_complex_closure_bin = Forall((a, b), InSet(Mult(a, b), Complex), domain=Complex)
In [51]:
mult_complex_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),Complex),
domain=Complex),
domain=Natural)
In [52]:
mult_complex_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), ComplexNonZero),
domain=ComplexNonZero)
In [53]:
mult_complex_nonzero_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),ComplexNonZero),
domain=ComplexNonZero),
domain=Natural)
In [54]:
mult_not_eq_zero = \
Forall(n, Forall(a_1_to_n,
NotEquals(Mult(a_1_to_n), zero),
domain=ComplexNonZero),
domain=Natural)
In [55]:
elim_one_left = Forall(x, Equals(Mult(one, x), x), domain=Complex)
In [56]:
elim_one_right = Forall(x, Equals(Mult(x, one), x), domain=Complex)
In [57]:
elim_one_any = \
Forall((i, j),
Forall((a_1_to_i, b_1_to_j),
Equals(Mult(a_1_to_i, one, b_1_to_j),
Mult(a_1_to_i, b_1_to_j)),
domain=Complex),
domain=Natural)
In [58]:
mult_zero_left = Forall(x, Equals(Mult(zero, x), zero), domain=Complex)
In [59]:
mult_zero_right = Forall(x, Equals(Mult(x, zero), zero), domain=Complex)
In [60]:
mult_zero_any = \
Forall((i, j),
Forall((a_1_to_i, b_1_to_j),
Equals(Mult(a_1_to_i, zero, b_1_to_j), zero),
domain=Complex),
domain=Natural)
In [61]:
mult_neg_left = Forall((x, y), Equals(Mult(Neg(x), y), Neg(Mult(x, y))), domain=Complex)
In [62]:
mult_neg_right = Forall((x, y), Equals(Mult(x, Neg(y)), Neg(Mult(x, y))), domain=Complex)
In [63]:
mult_neg_left_double = Forall((x, y), Equals(Neg(Mult(Neg(x), y)), Mult(x, y)), domain=Complex)
In [64]:
mult_neg_right_double = Forall((x, y), Equals(Neg(Mult(x, Neg(y))), Mult(x, y)), domain=Complex)
Theorems for number relations¶
In [65]:
left_mult_eq = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Natural)
In [66]:
left_mult_eq_int = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Integer)
In [67]:
left_mult_eq_rational = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Rational)
In [68]:
left_mult_eq_real = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Real)
In [69]:
left_mult_eq = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Complex)
In [70]:
right_mult_eq_nat = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Natural)
In [71]:
right_mult_eq_int = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Integer)
In [72]:
right_mult_eq_rational = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Rational)
In [73]:
right_mult_eq_real = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Real)
In [74]:
right_mult_eq = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y))
Note: proving left_mult_neq and right_mult_neq for the complex domain is a bit more challenging than just real numbers, but should still be applicable. Using a polar coordinate representations, such as $r \textrm{exp}(i \theta)$, makes it more clear. Suppose $x = x_r \textrm{exp}(i \cdot x_{\theta})$ and $y = y_r \textrm{exp}(i \cdot y_{\theta})$; if $x \neq y$, either $x_r \neq y_r$ or $x_{\theta} \neq y_{\theta}$ (or both), so either the length or angle (or both) will differ on either side.
In [75]:
left_mult_neq_nat = Forall((a, x, y), NotEquals(Mult(a, x), Mult(a, y)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Natural)
In [76]:
left_mult_neq_int = Forall((a, x, y), NotEquals(Mult(a, x), Mult(a, y)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Integer)
In [77]:
left_mult_neq_rational = Forall((a, x, y), NotEquals(Mult(a, x), Mult(a, y)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Rational)
In [78]:
left_mult_neq_real = Forall((a, x, y), NotEquals(Mult(a, x), Mult(a, y)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Real)
In [79]:
left_mult_neq = Forall((a, x, y), NotEquals(Mult(a, x), Mult(a, y)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Complex)
In [80]:
right_mult_neq_nat = Forall((a, x, y), NotEquals(Mult(x, a), Mult(y, a)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Natural)
In [81]:
right_mult_neq_int = Forall((a, x, y), NotEquals(Mult(x, a), Mult(y, a)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Integer)
In [82]:
right_mult_neq_rational = Forall((a, x, y), NotEquals(Mult(x, a), Mult(y, a)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Rational)
In [83]:
right_mult_neq_real = Forall((a, x, y), NotEquals(Mult(x, a), Mult(y, a)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Real)
In [84]:
right_mult_neq = Forall((a, x, y), NotEquals(Mult(x, a), Mult(y, a)),
conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Complex)
In [85]:
strong_bound_via_right_factor_bound = (
Forall((a, x, y), Less(Mult(a, x), Mult(a, y)),
conditions=[Less(x, y), greater(a, zero)], domain=Real))
In [86]:
strong_bound_via_left_factor_bound = (
Forall((a, x, y), Less(Mult(x, a), Mult(y, a)),
conditions=[Less(x, y), greater(a, zero)], domain=Real))
In [87]:
strong_bound_via_factor_bound = (
Forall((i, j), Forall((x, y), Forall((a_1_to_i, b_1_to_j),
Less(Mult(a_1_to_i, x, b_1_to_j), Mult(a_1_to_i, y, b_1_to_j)),
domain=RealPos, condition=Less(x, y))),
domain=Natural))
In [88]:
weak_bound_via_right_factor_bound = (
Forall((a, x, y), LessEq(Mult(a, x), Mult(a, y)),
conditions=[LessEq(x, y), greater_eq(a, zero)], domain=Real))
In [89]:
weak_bound_via_left_factor_bound = (
Forall((a, x, y), LessEq(Mult(x, a), Mult(y, a)),
conditions=[LessEq(x, y), greater_eq(a, zero)],
domain=Real))
In [90]:
weak_bound_via_factor_bound = (
Forall((i, j), Forall((x, y), Forall((a_1_to_i, b_1_to_j),
LessEq(Mult(a_1_to_i, x, b_1_to_j), Mult(a_1_to_i, y, b_1_to_j)),
domain=RealNonNeg, condition=LessEq(x, y))),
domain=Natural))
In [91]:
reversed_strong_bound_via_right_factor_bound = (
Forall((a, x, y), greater(Mult(a, x), Mult(a, y)),
conditions=[Less(x, y), Less(a, zero)], domain=Real))
In [92]:
reversed_weak_bound_via_right_factor_bound = (
Forall((a, x, y), greater_eq(Mult(a, x), Mult(a, y)),
conditions=[LessEq(x, y), LessEq(a, zero)], domain=Real))
In [93]:
reversed_strong_bound_via_left_factor_bound = (
Forall((a, x, y), greater(Mult(x, a), Mult(y, a)),
conditions=[Less(x, y), Less(a, zero)], domain=Real))
In [94]:
reversed_weak_bound_via_left_factor_bound = (
Forall((a, x, y), greater_eq(Mult(x, a), Mult(y, a)),
conditions=[LessEq(x, y), LessEq(a, zero)], domain=Real))
In [95]:
mult_neg_any = \
Forall((i, j),
Forall((a_1_to_i, b, c_1_to_j),
Equals(Mult(a_1_to_i, Neg(b), c_1_to_j),
Neg(Mult(a_1_to_i, b, c_1_to_j))),
domain=Complex),
domain=Natural)
In [96]:
mult_neg_any_double = \
Forall((i, j),
Forall((a_1_to_i, b, c_1_to_j),
Equals(Neg(Mult(a_1_to_i, Neg(b), c_1_to_j)),
Mult(a_1_to_i, b, c_1_to_j)),
domain=Complex),
domain=Natural)
In [97]:
distribute_through_sum = \
Forall((i,j,k),
Forall((a_1_to_i, b_1_to_j, c_1_to_k),
Equals(
Mult(a_1_to_i, Add(b_1_to_j), c_1_to_k),
Add(ExprRange(n,Mult(a_1_to_i,
IndexedVar(b, n),
c_1_to_k),
one, j))).with_wrapping_at(2),
domain=Complex).with_wrapping(),
domain=Natural)
In [98]:
distribute_through_abs_sum = \
Forall((i,j,k),
Forall((a_1_to_i, c_1_to_k),
Forall(b_1_to_j,
Equals(
Mult(a_1_to_i, Abs(Add(b_1_to_j)), c_1_to_k),
Abs(Add(ExprRange(n, Mult(a_1_to_i, IndexedVar(b, n), c_1_to_k),
one, j)))).with_wrapping_at(2),
domain=Complex).with_wrapping(),
domain=RealNonNeg).with_wrapping(),
domain=Natural)
In [99]:
distribute_through_subtract = \
Forall((i,j),
Forall((a_1_to_i, x, y, b_1_to_j),
Equals(
Mult(a_1_to_i, subtract(x, y), b_1_to_j),
subtract(Mult(a_1_to_i, x, b_1_to_j),
Mult(a_1_to_i, y, b_1_to_j)))\
.with_wrapping_at(2),
domain=Complex),
domain=Natural)
In [100]:
distribute_through_summation = \
Forall((i,j,k),
Forall((f, Q),
Implies(Forall(b_1_to_j,
InSet(Function(f, b_1_to_j), Complex),
condition=Function(Q, b_1_to_j)),
Forall((a_1_to_i, c_1_to_k),
Equals(Mult(a_1_to_i,
summation_b1toj_fQ,
c_1_to_k),
Sum(b_1_to_j,
Mult(a_1_to_i,
Function(f, b_1_to_j),
c_1_to_k),
condition=Function(Q, b_1_to_j)))\
.with_wrapping_at(2),
domain=Complex).with_wrapping())
.with_wrap_after_operator()),
domains=(Natural, NaturalPos, Natural))
In [101]:
commutation = Forall((a, b), Equals(Mult(a, b), Mult(b, a)), domain=Complex)
In [102]:
rightward_commutation = \
Forall((i,j,k),
Forall((a_1_to_i,b,c_1_to_j,d_1_to_k),
Equals(Mult(a_1_to_i, b, c_1_to_j, d_1_to_k),
Mult(a_1_to_i, c_1_to_j, b, d_1_to_k)) \
.with_wrapping_at(2),
domain=Complex),
domain=Natural)
In [103]:
leftward_commutation = \
Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c,d_1_to_k),
Equals(Mult(a_1_to_i, b_1_to_j, c, d_1_to_k),
Mult(a_1_to_i, c, b_1_to_j, d_1_to_k)) \
.with_wrapping_at(2),
domain=Complex),
domain=Natural)
In [104]:
association = \
Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c_1_to_k),
Equals(Mult(a_1_to_i, b_1_to_j, c_1_to_k),
Mult(a_1_to_i, Mult(b_1_to_j), c_1_to_k)) \
.with_wrapping_at(2),
domain=Complex),
domain=Natural)
In [105]:
disassociation = \
Forall((i,j,k),
Forall((a_1_to_i,b_1_to_j,c_1_to_k),
Equals(Mult(a_1_to_i, Mult(b_1_to_j), c_1_to_k),
Mult(a_1_to_i, b_1_to_j, c_1_to_k)) \
.with_wrapping_at(2),
domain=Complex),
domain=Natural)
In [106]:
%end theorems