# 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

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

In [3]:
unary_mult_reduction = Forall(a, Equals(Mult(a), a))

unary_mult_reduction (conjecture without proof):

In [4]:
mult_def_rev = \
Forall((n, x), Forall(a_1_to_n,
domain=Set(x)),
domains=(Natural, Complex))

mult_def_rev (conjecture without proof):

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)))

mult_in_zero_set_bin (conjecture without proof):

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)

mult_in_zero_set (conjecture without proof):

In [8]:
mult_nat_closure_bin = Forall((a, b), InSet(Mult(a, b), Natural), domain=Natural)

mult_nat_closure_bin (conjecture without proof):

In [9]:
mult_nat_from_double_nonpos = Forall((a, b), InSet(Mult(a, b), Natural),
domain=IntegerNonPos)

mult_nat_from_double_nonpos (conjecture without proof):

In [10]:
mult_nat_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), Natural),
domain=Natural),
domain=Natural)

mult_nat_closure (conjecture without proof):

In [11]:
mult_nat_pos_closure_bin = Forall((a, b), InSet(Mult(a, b), NaturalPos), domain=NaturalPos)

mult_nat_pos_closure_bin (conjecture without proof):

In [12]:
mult_nat_pos_from_double_neg = Forall((a, b), InSet(Mult(a, b), Natural),
domain=IntegerNeg)

mult_nat_pos_from_double_neg (conjecture without proof):

In [13]:
mult_nat_pos_closure = \
Forall(n, Forall(a_1_to_n,
InSet(Mult(a_1_to_n), NaturalPos),
domain=NaturalPos),
domain=Natural)

mult_nat_pos_closure (conjecture without proof):

In [14]:
mult_int_closure_bin = Forall((a, b), InSet(Mult(a, b), Integer), domain=Integer)

mult_int_closure_bin (conjecture without proof):

In [15]:
mult_int_neg_from_left_neg = Forall((a, b), InSet(Mult(a, b), IntegerNeg),
domains=(IntegerNeg, NaturalPos))

mult_int_neg_from_left_neg (conjecture without proof):

In [16]:
mult_int_neg_from_right_neg = Forall((a, b), InSet(Mult(a, b), IntegerNeg),
domains=(NaturalPos, IntegerNeg))

mult_int_neg_from_right_neg (conjecture without proof):

In [17]:
mult_int_nonpos_from_left_nonpos = Forall((a, b), InSet(Mult(a, b), IntegerNonPos),
domains=(IntegerNonPos, Natural))

mult_int_nonpos_from_left_nonpos (conjecture without proof):

In [18]:
mult_int_nonpos_from_right_nonpos = Forall((a, b), InSet(Mult(a, b), IntegerNonPos),
domains=(Natural, IntegerNonPos))

mult_int_nonpos_from_right_nonpos (conjecture without proof):

In [19]:
mult_int_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), Integer),
domain=Integer),
domain=Natural)

mult_int_closure (conjecture without proof):

In [20]:
mult_int_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), IntegerNonZero),
domain=IntegerNonZero)

mult_int_nonzero_closure_bin (conjecture without proof):

In [21]:
mult_int_nonzero_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), IntegerNonZero),
domain=IntegerNonZero),
domain=Natural)

mult_int_nonzero_closure (conjecture without proof):

In [22]:
mult_rational_closure_bin = Forall((a, b), InSet(Mult(a, b), Rational),
domain=Rational)

mult_rational_closure_bin (conjecture without proof):

In [23]:
mult_rational_closure = \
Forall(n, Forall(a_1_to_n,
InSet(Mult(a_1_to_n), Rational),
domain=Rational),
domain=Natural)

mult_rational_closure (conjecture without proof):

In [24]:
mult_rational_pos_closure_bin = Forall((a, b), InSet(Mult(a, b), RationalPos),
domain=RationalPos)

mult_rational_pos_closure_bin (conjecture without proof):

In [25]:
mult_rational_pos_from_double_neg = Forall((a, b), InSet(Mult(a, b), RationalPos),
domain=RationalNeg)

mult_rational_pos_from_double_neg (conjecture without proof):

In [26]:
mult_rational_neg_from_left_neg = Forall((a, b), InSet(Mult(a, b), RationalNeg),
domains=(RationalNeg, RationalPos))

mult_rational_neg_from_left_neg (conjecture without proof):

In [27]:
mult_rational_neg_from_right_neg = Forall((a, b), InSet(Mult(a, b), RationalNeg),
domains=(RationalPos, RationalNeg))

mult_rational_neg_from_right_neg (conjecture without proof):

In [28]:
mult_rational_pos_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), RationalPos),
domain=RationalPos),
domain=Natural)

mult_rational_pos_closure (conjecture without proof):

In [29]:
mult_rational_nonneg_closure_bin = Forall((a, b), InSet(Mult(a, b), RationalNonNeg),
domain=RationalNonNeg)

mult_rational_nonneg_closure_bin (conjecture without proof):

In [30]:
mult_rational_nonneg_from_double_nonpos = Forall((a, b), InSet(Mult(a, b), RationalNonNeg), domain=RationalNonPos)

mult_rational_nonneg_from_double_nonpos (conjecture without proof):

In [31]:
mult_rational_nonpos_from_left_nonpos = Forall((a, b), InSet(Mult(a, b), RationalNonPos),
domains=(RationalNonPos, RationalNonNeg))

mult_rational_nonpos_from_left_nonpos (conjecture without proof):

In [32]:
mult_rational_nonpos_from_right_nonpos = Forall((a, b), InSet(Mult(a, b), RationalNonPos),
domains=(RationalNonNeg, RationalNonPos))

mult_rational_nonpos_from_right_nonpos (conjecture without proof):

In [33]:
mult_rational_nonneg_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RationalNonNeg),
domain=RationalNonNeg), domain=Natural)

mult_rational_nonneg_closure (conjecture without proof):

In [34]:
mult_rational_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), RationalNonZero),
domain=RationalNonZero)

mult_rational_nonzero_closure_bin (conjecture without proof):

In [35]:
mult_rational_nonzero_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RationalNonZero),
domain=RationalNonZero),
domain=Natural)

mult_rational_nonzero_closure (conjecture without proof):

In [36]:
mult_real_closure_bin = Forall((a, b), InSet(Mult(a, b), Real), domain=Real)

mult_real_closure_bin (conjecture without proof):

In [37]:
mult_real_closure = \
Forall(n, Forall(a_1_to_n,
InSet(Mult(a_1_to_n), Real),
domain=Real),
domain=Natural)

mult_real_closure (conjecture without proof):

In [38]:
mult_real_pos_closure_bin = Forall((a, b), InSet(Mult(a, b), RealPos), domain=RealPos)

mult_real_pos_closure_bin (conjecture without proof):

In [39]:
mult_real_pos_from_double_neg = Forall((a, b), InSet(Mult(a, b), RealPos), domain=RealNeg)

mult_real_pos_from_double_neg (conjecture without proof):

In [40]:
mult_real_neg_from_left_neg = Forall((a, b), InSet(Mult(a, b), RealNeg), domains=(RealNeg, RealPos))

mult_real_neg_from_left_neg (conjecture without proof):

In [41]:
mult_real_neg_from_right_neg = Forall((a, b), InSet(Mult(a, b), RealNeg), domains=(RealPos, RealNeg))

mult_real_neg_from_right_neg (conjecture without proof):

In [42]:
mult_real_pos_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n), RealPos),
domain=RealPos),
domain=Natural)

mult_real_pos_closure (conjecture without proof):

In [43]:
mult_real_nonneg_closure_bin = Forall((a, b), InSet(Mult(a, b), RealNonNeg), domain=RealNonNeg)

mult_real_nonneg_closure_bin (conjecture without proof):

In [44]:
mult_real_nonneg_from_double_nonpos = Forall((a, b), InSet(Mult(a, b), RealNonNeg), domain=RealNonPos)

mult_real_nonneg_from_double_nonpos (conjecture without proof):

In [45]:
mult_real_nonpos_from_left_nonpos = Forall((a, b), InSet(Mult(a, b), RealNonPos), domains=(RealNonPos, RealNonNeg))

mult_real_nonpos_from_left_nonpos (conjecture without proof):

In [46]:
mult_real_nonpos_from_right_nonpos = Forall((a, b), InSet(Mult(a, b), RealNonPos), domains=(RealNonNeg, RealNonPos))

mult_real_nonpos_from_right_nonpos (conjecture without proof):

In [47]:
mult_real_nonneg_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RealNonNeg),
domain=RealNonNeg),
domain=Natural)

mult_real_nonneg_closure (conjecture without proof):

In [48]:
mult_real_nonzero_closure = Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),
RealNonZero),
domain=RealNonZero),
domain=Natural)

mult_real_nonzero_closure (conjecture without proof):

In [49]:
mult_real_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), RealNonZero),
domain=RealNonZero)

mult_real_nonzero_closure_bin (conjecture without proof):

In [50]:
mult_complex_closure_bin = Forall((a, b), InSet(Mult(a, b), Complex), domain=Complex)

mult_complex_closure_bin (conjecture without proof):

In [51]:
mult_complex_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),Complex),
domain=Complex),
domain=Natural)

mult_complex_closure (conjecture without proof):

In [52]:
mult_complex_nonzero_closure_bin = Forall((a, b), InSet(Mult(a, b), ComplexNonZero),
domain=ComplexNonZero)

mult_complex_nonzero_closure_bin (conjecture without proof):

In [53]:
mult_complex_nonzero_closure = \
Forall(n, Forall(a_1_to_n, InSet(Mult(a_1_to_n),ComplexNonZero),
domain=ComplexNonZero),
domain=Natural)

mult_complex_nonzero_closure (conjecture without proof):

In [54]:
mult_not_eq_zero = \
Forall(n, Forall(a_1_to_n,
NotEquals(Mult(a_1_to_n), zero),
domain=ComplexNonZero),
domain=Natural)

mult_not_eq_zero (conjecture without proof):

In [55]:
elim_one_left = Forall(x, Equals(Mult(one, x), x), domain=Complex)

elim_one_left (conjecture without proof):

In [56]:
elim_one_right = Forall(x, Equals(Mult(x, one), x), domain=Complex)

elim_one_right (conjecture without proof):

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)

elim_one_any (conjecture without proof):

In [58]:
mult_zero_left = Forall(x, Equals(Mult(zero, x), zero), domain=Complex)

mult_zero_left (conjecture without proof):

In [59]:
mult_zero_right = Forall(x, Equals(Mult(x, zero), zero), domain=Complex)

mult_zero_right (conjecture without proof):

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)

mult_zero_any (conjecture without proof):

In [61]:
mult_neg_left = Forall((x, y), Equals(Mult(Neg(x), y), Neg(Mult(x, y))), domain=Complex)

mult_neg_left (conjecture without proof):

In [62]:
mult_neg_right = Forall((x, y), Equals(Mult(x, Neg(y)), Neg(Mult(x, y))), domain=Complex)

mult_neg_right (conjecture without proof):

In [63]:
mult_neg_left_double = Forall((x, y), Equals(Neg(Mult(Neg(x), y)), Mult(x, y)), domain=Complex)

mult_neg_left_double (conjecture without proof):

In [64]:
mult_neg_right_double = Forall((x, y), Equals(Neg(Mult(x, Neg(y))), Mult(x, y)), domain=Complex)

mult_neg_right_double (conjecture without proof):

### 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)

left_mult_eq (conjecture without proof):

In [66]:
left_mult_eq_int = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Integer)

left_mult_eq_int (conjecture without proof):

In [67]:
left_mult_eq_rational = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Rational)

left_mult_eq_rational (conjecture without proof):

In [68]:
left_mult_eq_real = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Real)

left_mult_eq_real (conjecture without proof):

In [69]:
left_mult_eq = Forall((a, x, y), Equals(Mult(a, x), Mult(a, y)), condition=Equals(x, y), domain=Complex)

WARNING: Redefining left_mult_eq

left_mult_eq (conjecture without proof):

In [70]:
right_mult_eq_nat = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Natural)

right_mult_eq_nat (conjecture without proof):

In [71]:
right_mult_eq_int = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Integer)

right_mult_eq_int (conjecture without proof):

In [72]:
right_mult_eq_rational = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Rational)

right_mult_eq_rational (conjecture without proof):

In [73]:
right_mult_eq_real = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y), domain=Real)

right_mult_eq_real (conjecture without proof):

In [74]:
right_mult_eq = Forall((a, x, y), Equals(Mult(x, a), Mult(y, a)), condition=Equals(x, y))

right_mult_eq (conjecture without proof):

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)

left_mult_neq_nat (conjecture without proof):

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)

left_mult_neq_int (conjecture without proof):

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)

left_mult_neq_rational (conjecture without proof):

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)

left_mult_neq_real (conjecture without proof):

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)

left_mult_neq (conjecture without proof):

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)

right_mult_neq_nat (conjecture without proof):

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)

right_mult_neq_int (conjecture without proof):

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)

right_mult_neq_rational (conjecture without proof):

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)

right_mult_neq_real (conjecture without proof):

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)

right_mult_neq (conjecture without proof):

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))

strong_bound_via_right_factor_bound (conjecture without proof):

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))

strong_bound_via_left_factor_bound (conjecture without proof):

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))

strong_bound_via_factor_bound (conjecture without proof):

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))

weak_bound_via_right_factor_bound (conjecture without proof):

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))

weak_bound_via_left_factor_bound (conjecture without proof):

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))

weak_bound_via_factor_bound (conjecture without proof):

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))

reversed_strong_bound_via_right_factor_bound (conjecture without proof):

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))

reversed_weak_bound_via_right_factor_bound (conjecture without proof):

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))

reversed_strong_bound_via_left_factor_bound (conjecture without proof):

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))

reversed_weak_bound_via_left_factor_bound (conjecture without proof):

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)

mult_neg_any (conjecture without proof):

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)

mult_neg_any_double (conjecture without proof):

In [97]:
distribute_through_sum =  \
Forall((i,j,k),
Forall((a_1_to_i, b_1_to_j, c_1_to_k),
Equals(
IndexedVar(b, n),
c_1_to_k),
one, j))).with_wrapping_at(2),
domain=Complex).with_wrapping(),
domain=Natural)

distribute_through_sum (conjecture without proof):

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(
one, j)))).with_wrapping_at(2),
domain=Complex).with_wrapping(),
domain=RealNonNeg).with_wrapping(),
domain=Natural)

distribute_through_abs_sum (conjecture without proof):

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)

distribute_through_subtract (conjecture without proof):

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))

distribute_through_summation (conjecture without proof):

In [101]:
commutation = Forall((a, b), Equals(Mult(a, b), Mult(b, a)), domain=Complex)

commutation (conjecture without proof):

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)

rightward_commutation (conjecture without proof):

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)

leftward_commutation (conjecture without proof):

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)

association (conjecture without proof):

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)

disassociation (conjecture without proof):

In [106]:
%end theorems

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