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

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.core_expr_types import x_j, x_1_to_n, w_1_to_m, z_1_to_n
from proveit.logic import Forall, InSet, Equals, NotEquals, Implies
from proveit.numbers import (ZeroSet, Integer, Natural, NaturalPos, Rational, RationalNonPos,
                             RationalNonZero, RationalPos, RationalNonNeg, RationalNeg,
                             Real, RealPos, RealNeg, RealNonPos, RealNonNeg, 
                             RealNonZero, Complex, ComplexNonZero)
from proveit.numbers import Div, frac, Add, subtract, Sum, Mult, Neg, Exp, zero, one
from proveit.numbers import Less, LessEq, greater, greater_eq, number_ordering
from proveit import a, b, c, d, e, j, k, m, n, w, x, y, z, P, S, Py

%begin theorems

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

div_rational_closure = Forall(
    [a, b],
    InSet(frac(a, b), Rational),
    domain=Rational,
    conditions=[NotEquals(b, zero)])

div_rational_closure (conjecture without proof):

div_rational_nonzero_closure = Forall(
    [a, b],
    InSet(frac(a, b), RationalNonZero),
    domain=RationalNonZero)

div_rational_nonzero_closure (conjecture without proof):

div_rational_pos_closure = Forall(
    [a, b],
    InSet(frac(a, b), RationalPos),
    domain=RationalPos)

div_rational_pos_closure (conjecture without proof):

div_rational_pos_from_double_neg = Forall(
    [a, b],
    InSet(frac(a, b), RationalPos),
    domain=RationalNeg)

div_rational_pos_from_double_neg (conjecture without proof):

div_rational_neg_from_neg_denom = Forall(
    [a, b],
    InSet(frac(a, b), RationalNeg),
    domains=(RationalPos, RationalNeg))

div_rational_neg_from_neg_denom (conjecture without proof):

div_rational_neg_from_neg_numer = Forall(
    [a, b],
    InSet(frac(a, b), RationalNeg),
    domains=(RationalNeg, RationalPos))

div_rational_neg_from_neg_numer (conjecture without proof):

div_rational_nonneg_closure = Forall(
    [a, b],
    InSet(frac(a, b), RationalNonNeg),
    domains=(RationalNonNeg, RationalPos))

div_rational_nonneg_closure (conjecture without proof):

div_rational_nonneg_from_double_neg = Forall(
    [a, b],
    InSet(frac(a, b), RationalNonNeg),
    domains=(RationalNonPos, RationalNeg))

div_rational_nonneg_from_double_neg (conjecture without proof):

div_rational_nonpos_from_neg_denom = Forall(
    [a, b],
    InSet(frac(a, b), RationalNonPos),
    domains=(RationalNonNeg, RationalNeg))

div_rational_nonpos_from_neg_denom (conjecture without proof):

div_rational_nonpos_from_nonpos_numer = Forall(
    [a, b],
    InSet(frac(a, b), RationalNonPos),
    domains=(RationalNonPos, RationalPos))

div_rational_nonpos_from_nonpos_numer (conjecture without proof):

div_real_nonzero_closure = Forall(
    [a, b],
    InSet(frac(a, b), RealNonZero),
    domain=RealNonZero)

div_real_nonzero_closure (conjecture without proof):

div_real_closure = Forall(
    [a, b],
    InSet(frac(a, b), Real),
    domain=Real,
    conditions=[NotEquals(b, zero)])

div_real_closure (conjecture without proof):

div_real_pos_closure = Forall([a, b], InSet(frac(a, b), RealPos), domain=RealPos, conditions=[NotEquals(b, zero)])

div_real_pos_closure (conjecture without proof):

div_real_pos_from_double_neg = Forall(
    [a, b],
    InSet(frac(a, b), RealPos),
    domain=RealNeg)

div_real_pos_from_double_neg (conjecture without proof):

div_real_neg_from_neg_denom = Forall(
    [a, b],
    InSet(frac(a, b), RealPos),
    domains=(RealPos, RealNeg))

div_real_neg_from_neg_denom (conjecture without proof):

div_real_neg_from_neg_numer = Forall(
    [a, b],
    InSet(frac(a, b), RealNeg),
    domains=(RealNeg, RealPos))

div_real_neg_from_neg_numer (conjecture without proof):

div_real_nonneg_closure = Forall(
    [a, b],
    InSet(frac(a, b), RealNonNeg),
    domains=(RealNonNeg, RealPos))

div_real_nonneg_closure (conjecture without proof):

div_real_nonneg_from_double_neg = Forall(
    [a, b],
    InSet(frac(a, b), RealNonNeg),
    domains=(RealNonPos, RealNeg))

div_real_nonneg_from_double_neg (conjecture without proof):

div_real_nonpos_from_neg_denom = Forall(
    [a, b],
    InSet(frac(a, b), RealNonPos),
    domains=(RealNonNeg, RealNeg))

div_real_nonpos_from_neg_denom (conjecture without proof):

div_real_nonpos_from_nonpos_numer = Forall(
    [a, b],
    InSet(frac(a, b), RealNonPos),
    domains=(RealNonPos, RealPos))

div_real_nonpos_from_nonpos_numer (conjecture without proof):

div_complex_nonzero_closure = Forall(
    [a, b],
    InSet(frac(a, b), ComplexNonZero),
    domain=ComplexNonZero)

div_complex_nonzero_closure (conjecture without proof):

div_complex_closure = Forall([a, b], InSet(frac(a, b), Complex), domain=Complex, conditions=[NotEquals(b, zero)])

div_complex_closure (conjecture without proof):

frac_not_eq_zero = Forall([a, b], NotEquals(frac(a,b), zero), domain=ComplexNonZero)

frac_not_eq_zero (conjecture without proof):

frac_zero_numer = Forall(
        x, Equals(frac(zero, x), zero), domain=Complex,
        conditions=[NotEquals(x, zero)])

frac_zero_numer (conjecture without proof):

frac_in_zero_set = Forall(
        (a, b), InSet(frac(a, b), ZeroSet), domain=Complex,
        conditions=[Equals(a, zero), NotEquals(b, zero)])

frac_in_zero_set (conjecture without proof):

frac_one_denom = Forall(x, Equals(frac(x, one), x), domain=Complex)

frac_one_denom (conjecture without proof):

div_by_frac_is_mult_by_reciprocal = (
        Forall((x, y, z),
        Equals(frac(x, frac(y, z)), Mult(x, frac(z, y))),
        domain=Complex,
        conditions=[NotEquals(y, zero), NotEquals(z, zero)]))

div_by_frac_is_mult_by_reciprocal (conjecture without proof):

numerator_frac_reduction = (
        Forall((x, y, z),
        Equals(frac(frac(x, y), z), frac(x, Mult(y, z))),
        domain=Complex,
        conditions=[NotEquals(y, zero), NotEquals(z, zero)]))

numerator_frac_reduction (conjecture without proof):

div_as_mult = Forall((x, y), Equals(frac(x, y), Mult(x, Exp(y, Neg(one)))),
                     domain=Complex, condition=NotEquals(y, zero))

div_as_mult (conjecture without proof):

Equals and not equals

div_eq_nat = Forall((a, x, y), Equals(frac(x, a), frac(y, a)), 
                    conditions=[Equals(x, y), NotEquals(a, zero)], domain=Natural)

div_eq_nat (conjecture without proof):

div_eq_int = Forall((a, x, y), Equals(frac(x, a), frac(y, a)), 
                    conditions=[Equals(x, y), NotEquals(a, zero)], domain=Integer)

div_eq_int (conjecture without proof):

div_eq_rational = Forall((a, x, y), Equals(frac(x, a), frac(y, a)), 
                         conditions=[Equals(x, y), NotEquals(a, zero)], domain=Rational)

div_eq_rational (conjecture without proof):

div_eq_real = Forall((a, x, y), Equals(frac(x, a), frac(y, a)), 
                     conditions=[Equals(x, y), NotEquals(a, zero)], domain=Real)

div_eq_real (conjecture without proof):

div_eq = Forall((a, x, y), Equals(frac(x, a), frac(y, a)), 
                conditions=[Equals(x, y), NotEquals(a, zero)], domain=Complex)

div_eq (conjecture without proof):

div_neq_nat = Forall((a, x, y), NotEquals(frac(x, a), frac(y, a)), 
                     conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Natural)

div_neq_nat (conjecture without proof):

div_neq_int = Forall((a, x, y), NotEquals(frac(x, a), frac(y, a)), 
                     conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Integer)

div_neq_int (conjecture without proof):

div_neq_rational = Forall((a, x, y), NotEquals(frac(x, a), frac(y, a)), 
                          conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Rational)

div_neq_rational (conjecture without proof):

div_neq_real = Forall((a, x, y), NotEquals(frac(x, a), frac(y, a)), 
                      conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Real)

div_neq_real (conjecture without proof):

div_neq = Forall((a, x, y), NotEquals(frac(x, a), frac(y, a)), 
                 conditions=[NotEquals(x, y), NotEquals(a, zero)], domain=Complex)

div_neq (conjecture without proof):

Bounding division

strong_div_from_numer_bound__pos_denom = Forall((a, x, y), Less(frac(x, a), frac(y, a)), 
                               conditions=[Less(x, y), greater(a, zero)], domain=Real)

strong_div_from_numer_bound__pos_denom (conjecture without proof):

weak_div_from_numer_bound__pos_denom = Forall(
    (a, x, y), LessEq(frac(x, a), frac(y, a)),
    conditions=[LessEq(x, y), greater(a, zero)], domain=Real)

weak_div_from_numer_bound__pos_denom (conjecture without proof):

strong_div_from_numer_bound__neg_denom = Forall(
    (a, x, y), greater(frac(x, a), frac(y, a)),
    conditions=[Less(x, y), Less(a, zero)], domain=Real)

strong_div_from_numer_bound__neg_denom (conjecture without proof):

weak_div_from_numer_bound__neg_denom = Forall(
    (a, x, y), greater_eq(frac(x, a), frac(y, a)),
    conditions=[LessEq(x, y), Less(a, zero)], domain=Real)

weak_div_from_numer_bound__neg_denom (conjecture without proof):

strong_div_from_denom_bound__all_pos = Forall(
    (a, x, y), greater(frac(a, x), frac(a, y)), 
    condition=Less(x, y), domain=RealPos)

strong_div_from_denom_bound__all_pos (conjecture without proof):

weak_div_from_denom_bound__all_pos = Forall(
    a, Forall((x, y), greater_eq(frac(a, x), frac(a, y)),
              condition=LessEq(x, y), domain=RealPos),
    domain=RealNonNeg)

weak_div_from_denom_bound__all_pos (conjecture without proof):

strong_div_from_denom_bound__all_neg = Forall(
    (a, x, y), Less(frac(a, x), frac(a, y)), 
    condition=Less(x, y), domain=RealNeg)

strong_div_from_denom_bound__all_neg (conjecture without proof):

weak_div_from_denom_bound__all_neg = Forall(
    a, Forall((x, y), LessEq(frac(a, x), frac(a, y)), 
              condition=LessEq(x, y), domain=RealNeg),
    domain=RealNonPos)

weak_div_from_denom_bound__all_neg (conjecture without proof):

strong_div_from_denom_bound__neg_over_pos = Forall(
    a, Forall((x, y), Less(frac(a, x), frac(a, y)), 
              condition=Less(x, y), domain=RealPos), 
    domain=RealNeg)

strong_div_from_denom_bound__neg_over_pos (conjecture without proof):

weak_div_from_denom_bound__neg_over_pos = Forall(
    a, Forall((x, y), LessEq(frac(a, x), frac(a, y)), 
              condition=LessEq(x, y), domain=RealPos), 
    domain=RealNonPos)

weak_div_from_denom_bound__neg_over_pos (conjecture without proof):

strong_div_from_denom_bound__pos_over_neg = Forall(
    a, Forall((x, y), greater(frac(a, x), frac(a, y)), 
              condition=Less(x, y), domain=RealNeg), 
    domain=RealPos)

strong_div_from_denom_bound__pos_over_neg (conjecture without proof):

weak_div_from_denom_bound__pos_over_neg = Forall(
    a, Forall((x, y), greater_eq(frac(a, x), frac(a, y)), 
              condition=LessEq(x, y), domain=RealNeg), 
    domain=RealNonNeg)

weak_div_from_denom_bound__pos_over_neg (conjecture without proof):

distribute_frac_through_sum = Forall(
    n, Forall([x_1_to_n, y], Equals(frac(Add(x_1_to_n), y),
                                    Add(ExprRange(j, frac(x_j, y), one, n))), 
              domain=Complex, conditions=[NotEquals(y, zero)]),
    domain=NaturalPos)

distribute_frac_through_sum (conjecture without proof):

distribute_frac_through_subtract = Forall([x, y, z], 
                                          Equals(frac(subtract(x, y), z),
                                                 subtract(frac(x, z), frac(y, z))), 
                                          domain=Complex, conditions=[NotEquals(z, zero)])

distribute_frac_through_subtract (conjecture without proof):

# distribute_frac_through_summation = Forall([P, S],
#                                     Implies(Forall(y_multi, InSet(Py_etc, Complex), domain=S),
#                                             Forall(z,
#                                                    Equals(frac(Sum(y_multi, Py_etc, domain=S), z),
#                                                           Sum(y_multi, frac(Py_etc, z), domain=S)),
#                                                   domain=Complex)))

# Here is a best guess for the summation version:
distribute_frac_through_summation = (
    Forall((P, S),
       Implies(Forall(y, InSet(Py, Complex) , domain=S),
        Forall(z,
        Equals(frac(Sum(y, Py, domain=S), z), Sum(y, frac(Py, z), domain=S)),
        domain=Complex,
        conditions=[NotEquals(z, zero)]))))

distribute_frac_through_summation (conjecture without proof):

frac_in_prod = (
    Forall((m, n),
       Forall((w_1_to_m, x, y, z_1_to_n),
              Equals(Mult(w_1_to_m, frac(x, y), z_1_to_n), frac(Mult(w_1_to_m, x, z_1_to_n), y)),
              domain=Complex,
              conditions=[NotEquals(y, zero)]),
       domain=NaturalPos))

frac_in_prod (conjecture without proof):

We certainly should not be able to cancel when there is division by zero. However, equivalences when both sides have zero in the denominator could be okay if we have axioms that allow us to treat division flexibly -- both sides are undefined.

mult_frac_right = Forall([x, y, z], Equals(Mult(x, frac(y, z)),
                                              frac(Mult(x, y), z)), 
                         domain=Complex, condition=NotEquals(z, zero))

mult_frac_right (conjecture without proof):

mult_frac_left = Forall([x, y, z], Equals(Mult(frac(x, z), y),
                                             frac(Mult(x, y), z)), 
                        domain=Complex, condition=NotEquals(z, zero))

mult_frac_left (conjecture without proof):

prod_of_fracs = Forall((x, y), Forall((z, w), 
                                      Equals(Mult(frac(x, z), frac(y, w)),
                                             frac(Mult(x, y), Mult(z, w))), 
                                      domain=ComplexNonZero),
                       domain=Complex)

prod_of_fracs (conjecture without proof):

frac_cancel_left = (
    Forall((x, z),
        Forall(y,
            Equals(frac(Mult(x,y),Mult(x,z)),frac(y,z)),
        domain=Complex),
    domain=ComplexNonZero))

frac_cancel_left (conjecture without proof):

frac_cancel_right = (
    Forall((x, z),
        Forall(y,
            Equals(frac(Mult(y, x), Mult(z, x)), frac(y,z)),
        domain=Complex),
    domain=ComplexNonZero))

frac_cancel_right (conjecture without proof):

mult_frac_cancel_numer_left = Forall(
    (a, d), Forall((b, c, e),
                   Equals(Mult(frac(Mult(a, b), c), frac(d, Mult(b, e))),
                          Mult(frac(a, c), frac(d, e))),
                   domain=ComplexNonZero),
    domain=Complex)

mult_frac_cancel_numer_left (conjecture without proof):

mult_frac_cancel_denom_left = Forall(
    (a, d), Forall((b, c, e), Equals(Mult(frac(a, Mult(b, c)),
                                          frac(Mult(c, d), e)),
                                     Mult(frac(a, b), frac(d, e))),
                   domain=ComplexNonZero), 
    domain=Complex)

mult_frac_cancel_denom_left (conjecture without proof):

# mult_frac_left_cancel = Forall([x,y],
#                       Equals(Mult(frac(x,y),y),x),
#                       domain = Complex, conditions = [NotEquals(y, zero)])

# mult_frac_left_partial_cancel = Forall(
#     [x,y,z], Equals(Mult(frac(x,Mult(y, z)),z),frac(x, y)),
#     domain = Complex, conditions = [NotEquals(y, zero), NotEquals(z, zero)])

# mult_frac_right_cancel = Forall([x,y],
#                              Equals(Mult(x, frac(y, x)),y),
#                              domain = Complex, conditions = [NotEquals(x, zero)])

# mult_frac_right_partical_cancel = Forall(
#     [x,y, z], Equals(Mult(x, frac(y, Mult(x, z))),frac(y, z)),
#     domain = Complex, conditions = [NotEquals(x, zero)])

frac_cancel_complete = Forall(x, Equals(frac(x, x), one), 
                            domain=Complex, conditions = [NotEquals(x, zero)])

frac_cancel_complete (conjecture without proof):

reverse_fraction_of_subtractions = Forall(
    [w, x, y, z], Equals(frac(subtract(w, x), subtract(y, z)),
                         frac(subtract(x, w), subtract(z, y))), 
    domain=Complex, condition=NotEquals(y, z))

reverse_fraction_of_subtractions (conjecture without proof):

cancel_negations = Forall(
    [x, y],
    Equals(frac(Neg(x), Neg(y)), frac(x, y)),
    domain=Complex,
    conditions=[NotEquals(y, zero)])

cancel_negations (conjecture without proof):

neg_frac_neg_numerator = Forall(
    [x, y],
    Equals(frac(Neg(x), y), Neg(frac(x, y))),
    domain=Complex,
    conditions=[NotEquals(y, zero)])

neg_frac_neg_numerator (conjecture without proof):

neg_frac_neg_numerator_gen = (
    Forall((m, n),
    Forall((w_1_to_m, x, y, z_1_to_n),
    Equals(frac(Mult(w_1_to_m, Neg(x), z_1_to_n), y), Neg(frac(Mult(w_1_to_m, x, z_1_to_n), y))),
    domain=Complex,
    conditions=[NotEquals(y, zero)])))

neg_frac_neg_numerator_gen (conjecture without proof):

neg_frac_neg_denominator = Forall(
    [x, y],
    Equals(frac(x, Neg(y)), Neg(frac(x, y))),
    domain=Complex,
    conditions=[NotEquals(y, zero)])

neg_frac_neg_denominator (conjecture without proof):

neg_frac_neg_denominator_gen = (
    Forall((m, n),
    Forall((w_1_to_m, x, y, z_1_to_n),
    Equals(frac(x, Mult(w_1_to_m, Neg(y), z_1_to_n)), Neg(frac(x, Mult(w_1_to_m, y, z_1_to_n)))),
    domain=Complex,
    conditions=[NotEquals(y, zero),
                ExprRange(k, NotEquals(IndexedVar(w, k), zero), one, m),
                ExprRange(k, NotEquals(IndexedVar(z, k), zero), one, n)])))

neg_frac_neg_denominator_gen (conjecture without proof):

# frac_int_exp = Forall(n, Forall((a, b), 
#                               Equals(frac(Exp(a, n), Exp(b, n)),
#                                      Exp(frac(a, b), n)),
#                              conditions = [NotEquals(a, zero), NotEquals(b, zero)]),
#                     domain=Integer)

# frac_nat_pos_exp = Forall(n, Forall((a, b), 
#                               Equals(frac(Exp(a, n), Exp(b, n)),
#                                      Exp(frac(a, b), n)),
#                              conditions = [NotEquals(b, zero)]),
#                     domain=NaturalPos)

%end theorems

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