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

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 a, b, c, k, m, n, p, x, y, z
from proveit.logic import And, Boolean, Equals, InSet, Forall, NotEquals, Not, Or
from proveit.numbers import zero, one, two, Complex, Integer, NaturalPos
from proveit.numbers import Add, Divides, Exp, GCD, greater, Mult, Neg, subtract

%begin theorems

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

def non_zero_conditions(non_zero_vars):
    temp_list = [NotEquals(_i, zero) for _i in non_zero_vars]
    return temp_list

Fundamental InBool theorem: a Divides(m,n) claim is Boolean.

# Proven
divides_is_bool = Forall(
        (x, y),
        InSet(Divides(x, y), Boolean))

divides_is_bool (conjecture with conjecture-based proof):

Divides is Transitive

divides_transitivity = Forall(
        (x, y, z),
        Divides(x, z),
        conditions=[Divides(x, y), Divides(y, z)])

divides_transitivity (conjecture without proof):

Divides is Reflexive

divides_reflexivity = Forall(
        x,
        Divides(x, x),
        domain=Complex,
        conditions=non_zero_conditions([x]))

divides_reflexivity (conjecture without proof):

Divides is Disjunctive Anti-Symmetric

divides_anti_symmetry = Forall(
        (x, y),
        Or(Equals(x, y), Equals(x, Neg(y))),
        conditions=[Divides(x, y), Divides(y, x)])

divides_anti_symmetry (conjecture without proof):

If $a|b$ and $a|c$, then $a|(b±c)$

divides_sum = Forall(
        (x, y, z),
        Divides(x, Add(y, z)),
        conditions=[Divides(x, y), Divides(x, z)])

divides_sum (conjecture without proof):

divides_difference = Forall(
        (x, y, z),
        Divides(x, subtract(y, z)),
        conditions=[Divides(x, y), Divides(x, z)])

divides_difference (conjecture without proof):

# We need to constrain to the set of integer numbers in the case of Euclid's Lemma
euclids_lemma = Forall(
        (x, y, z),
        Divides(x, z),
        domain=Integer,
        conditions=[Divides(x, Mult(y, z)), Equals(GCD(x, y), one)])

euclids_lemma (conjecture without proof):

non_zero_divides_zero = Forall(
        x,
        Divides(x, zero),
        domain=Complex,
        conditions=non_zero_conditions([x]))

non_zero_divides_zero (conjecture with conjecture-based proof):

# Here the restriction of y to the set of Integer numbers is related to the axiomatic def of Divides
# x|y = (y/x in Integer). Thus x|xy = (xy/x = y in Integer)
left_factor_divisibility = Forall(
    (x, y),
    Divides(x, Mult(x, y)),
    domains=(Complex, Integer),
    condition=NotEquals(x, zero))

left_factor_divisibility (conjecture without proof):

right_factor_divisibility = Forall(
    (x, y),
    Divides(y, Mult(x, y)),
    domains=(Complex, Integer),
    condition=NotEquals(x, zero))

right_factor_divisibility (conjecture without proof):

# later generalize those binary versions to a1,..,ai, b, c1,…,cj ?

# This can be generalized to any prime number. 
even__if__power_is_even = Forall(
    (a, n), Divides(two, a), domain=Integer,
    conditions = [Divides(two, Exp(a, n))])

even__if__power_is_even (conjecture without proof):

# might not need explicit restrictions here on k and a
common_exponent_elimination = (
    Forall(
    (k, a, n),
    Divides(k, a),
    domains = [Integer, Integer, NaturalPos],
    conditions = [Divides(Exp(k, n), Exp(a, n))]))

common_exponent_elimination (conjecture without proof):

common_exponent_introduction = (
    Forall(
    (k, a, n),
    Divides(Exp(k, n), Exp(a, n)),
    domains = [Integer, Integer, NaturalPos],
    conditions = [Divides(k, a)]))

common_exponent_introduction (conjecture without proof):

common_factor_elimination = (
       Forall((a, b, k),
              Divides(a,b),
              domain=Complex,
              conditions=[Divides(Mult(k,a), Mult(k,b)), NotEquals(k, zero)]))

common_factor_elimination (conjecture without proof):

GCD Theorems

# Defining/interpreting GCD(a,b)=1.
# Somewhat opaque because we are not explicitly restricting p <= a, p <= b
# BUT if p > a then p|a will be FALSE (b/c a/p will not be an integer)
GCD_one_def = Forall(
    (a, b),
    Forall(p,
           Not(And(Divides(p, a), Divides(p, b))),
           domain=NaturalPos,
           condition=greater(p, one)),
    domain=NaturalPos,
    condition = Equals(GCD(a, b), one))

GCD_one_def (conjecture without proof):

%end theorems

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