# This file contains theorems related to natural number arithmetic. However, it does not # assume all numbers are natural numbers like peano_min.ghi and peano.gh. This proves # theorems that are valid for natural numbers, integers, rational numbers, and real # numbers. param (PROP prop.ghi () "") param (PREDICATE_EQ predicate_eq.ghi (PROP) "") tvar (wff ph ps ch th ta) tvar (nat A B C D) var (nat v w x y z) term (wff (< A B)) term (wff (>= A B)) term (wff (> A B)) term (wff (pos A)) term (wff (zneg A)) term (nat (ifn ph A B)) term (nat (2)) term (nat (3)) term (nat (4)) term (nat (5)) term (nat (6)) term (nat (7)) term (nat (8)) term (nat (9)) term (nat (10)) ## ## redirect ../common/add_multiply_min.ghi ## term (nat (+ A B)) term (nat (* A B)) term (nat (0)) term (nat (1)) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (addass () () (= (+ (+ A B) C) (+ A (+ B C)))) ## Additive Identity ## auto-right('Simplify', '0') stmt (addid () () (= (+ A (0)) A)) ## Commutative Property ## ## (= (+ A B) (+ B A)) ##
## right('Commute', '+') stmt (addcom () () (= (+ A B) (+ B A))) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (mulass () () (= (* (* A B) C) (* A (* B C)))) ## Commutative Property ## ## (= (* A B) (* B A)) ##
## right('Commute', '*') stmt (mulcom () () (= (* A B) (* B A))) # Distribution of addition through multiplication ## Distributive Property ## ## (= (* A (+ B C)) (+ (* A B) (* A C))) ##
## right('Distribute', 'R') left('Distribute', '-R') stmt (distr () () (= (* A (+ B C)) (+ (* A B) (* A C)))) ## Multiplicative Identity ## right('Simplify', '1') ## ## (= (* A (1)) A) ##
## auto-right('Simplify') stmt (mulid () () (= (* A (1)) A)) # Equality axiom for addition ## Addition of Equal Numbers Axiom ## ## When two equal numbers are added, their sums are equal. ## ## stmt (addeq12 () () (-> (/\ (= A B) (= C D)) (= (+ A C) (+ B D)))) ## Multiplication of Equal Numbers Axiom ## ## When two equal numbers are added, their products are equal. ## ## stmt (muleq12 () () (-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))) ## Cancellation of addition ## right('Cancel', '+') stmt (addcan () () (<-> (= (+ B A) (+ C A)) (= B C))) ## ## redirect mulcan_min.ghi ## ## Cancel Multiplication stmt (mulcan () () (-> (-. (= C (0))) (<-> (= (* A C) (* B C)) (= A B)))) ## ## redirect ../common/mulcan.ghi ## stmt (mulcan0 () () (-> (-. (= A (0))) (<-> (= (* B A) (0)) (= B (0))))) ## Cancel Multiplication stmt (mulcan2 () () (-> (-. (= A (0))) (<-> (= (* A B) (* A C)) (= B C)))) ## Cancel Multiplication ## ## (-. (= A ] (0))) ] ] ## (= (* B ] A) ] (* [ C A)) ## (= B ] ] [ C) ##
stmt (mulcani () ((-. (= A (0))) (= (* B A) (* C A))) (= B C)) ## Cancel Multiplication ## ## (-. (= A ] ] (0))) ] ## (= (* A [ B ) ] (* A [ C )) ## (= [ B ] [ C) ##
stmt (mulcan2i () ((-. (= A (0))) (= (* A B) (* A C))) (= B C)) ## Zero Product Property stmt (zeroProductz () () (-> (/\ (-. (= A (0))) (-. (= B (0)))) (-. (= (* A B) (0))))) ## Zero Product Property stmt (zeroFactors () () (<-> (= (* A B) (0)) (\/ (= A (0)) (= B (0))))) ## Zero Product Property stmt (nonzeroProduct () () (-> (-. (= A (0))) (<-> (= B (0)) (= (* A B) (0))))) ## Zero Product Property stmt (nonzeroProduct2 () () (<-> (-. (= (* A B) (0))) (/\ (-. (= A (0))) (-. (= B (0)))))) ## Multiply Nonequal Numbers stmt (neqmul () () (-> (/\ (-. (= A B)) (-. (= C (0)))) (-. (= (* A C) (* B C))))) ## ## redirect ../common/inequality_min.ghi ## term (wff (<= A B)) ## Reflexive Property stmt (leid () () (<= A A)) ## Same upper and lower bound implies equality ## Trichotomy law (may be a poor choice of name) ## left('Simplify', '=') stmt (lesym () () (<-> (= A B) (/\ (<= A B) (<= B A)))) ## Total Relationship ## Less than or equal is a total relationship stmt (letot () () (\/ (<= A B) (<= B A))) ## Transitive Property ## right('Simplify', '≤ ≤') stmt (letr () () (-> (/\ (<= A B) (<= B C)) (<= A C))) ## Inequality Multiplication stmt (lemul1 () () (-> (/\ (<= A B) (<= (0) C)) (<= (* A C) (* B C)))) ## 0 is not equal to 1 stmt (0ne1 () () (-. (= (0) (1)))) ## 0 is less than or equal to 1 stmt (0le1 () () (<= (0) (1))) ## 0 is less than 1 stmt (0less1 () () (< (0) (1))) ## 1 is more than 0 stmt (1greater0 () () (> (1) (0))) ## Inequality Equivalence stmt (leeq1 () () (-> (= A B) (<-> (<= A C) (<= B C)))) ## Inequality Equivalence stmt (leeq2 () () (-> (= A B) (<-> (<= C A) (<= C B)))) ## Less Than or Equal from Nonnegative Difference stmt (exle ((A x)(B x)) () (<-> (<= A B) (E. x (/\ (<= (0) x) (= (+ A x) B))))) ## ## redirect ../common/add_multiply.ghi ## ## Additive Identity ## auto-right('Simplify', '0') stmt (addidr () () (= (+ (0) A) A)) ## Definition of 2 stmt (df-2 () () (= (2) (+ (1) (1)))) ## Definition of 3 stmt (df-3 () () (= (3) (+ (2) (1)))) ## Definition of 4 stmt (df-4 () () (= (4) (+ (3) (1)))) ## Definition of 5 stmt (df-5 () () (= (5) (+ (4) (1)))) ## Definition of 6 stmt (df-6 () () (= (6) (+ (5) (1)))) ## Definition of 7 stmt (df-7 () () (= (7) (+ (6) (1)))) ## Definition of 8 stmt (df-8 () () (= (8) (+ (7) (1)))) ## Definition of 9 stmt (df-9 () () (= (9) (+ (8) (1)))) ## Definition of 10 stmt (df-10 () () (= (10) (+ (9) (1)))) ## Multiplicative Identity ## auto-right('Simplify', '1') stmt (mulidr() () (= (* (1) A) A)) ## Inequality Conversion ## left('Simplify', '<') stmt (axlttri2 () () (<-> (< A B) (/\ (-. (= A B)) (<= A B)))) ## Inequality Conversion ## left('Simplify', '>') stmt (axgrtri () () (<-> (> A B) (/\ (-. (= A B)) (>= A B)))) ## Inequality over Addition ## ## (-. (= [ A ] [ [ B )) ## (-. (= (+ C [ A ] ) (+ [ C [ B))) ##
stmt (addneq2i () ((-. (= A B))) (-. (= (+ C A) (+ C B)))) stmt (dist_ax6 () () (= (* A (+ B (1))) (+ (* A B) A))) stmt (dist_ax6r () () (= (* (+ A (1)) B) (+ (* A B) B))) ## Adding twice mean Multiply by 2 ## right('Simplify', '2') stmt (add2mul () () (= (+ A A) (* (2) A))) ## ## redirect ../common/inequality.ghi ## ## Addition is Monotonic ## Addition is strictly monotonic in the second addend ## left('Cancel', '+') ## ## (<-> (<= A B) (<= (+ C A) (+ C B))) ##
stmt (leadd2 () () (<-> (<= A B) (<= (+ C A) (+ C B)))) ## Addition Over Inequality ## ## (<= A ] [ B ] ) ## (<= (+ A ] C) (+ [ B ] C)) ##
stmt (leadd1i () ((<= A B)) (<= (+ A C) (+ B C))) ## Addition Over Inequality ## ## (<= [ A ] [ B ) ## (<= (+ C [ A ] ) (+ C [ B )) ##
stmt (leadd2i () ((<= A B)) (<= (+ C A) (+ C B))) ## Inequality Over Addition ## ## (< A ] [ B ] ) ## (< (+ A ] C) (+ [ B ] C)) ##
stmt (ltadd1i () ((< A B)) (< (+ A C) (+ B C))) ## Inequality Over Addition ## ## (< [ A ] [ B ) ## (< (+ C [ A ] ) (+ C [ B )) ##
stmt (letraddi () ((<= A B) (<= C D)) (<= (+ A C) (+ B D))) ## ## (< A ] ] [ B ] ) ## (< [ C ] [ [ D) ## (< (+ A ] C ] ) (+ [ B [ D)) ##
stmt (lttraddi () ((< A B) (< C D)) (< (+ A C) (+ B D))) ## ## (>= A ] ] [ B ] ) ## (>= [ C ] [ [ D) ## (>= (+ A ] C ] ) (+ [ B [ D)) ##
stmt (getraddi () ((>= A B) (>= C D)) (>= (+ A C) (+ B D))) ## ## (> A ] ] [ B ] ) ## (> [ C ] [ [ D) ## (> (+ A ] C ] ) (+ [ B [ D)) ##
stmt (gttraddi () ((> A B) (> C D)) (> (+ A C) (+ B D))) ## Addition Over Inequality ## ## (> A ] [ B ] ) ## (> (+ A ] C) (+ [ B ] C)) ##
stmt (gtadd1i () ((> A B)) (> (+ A C) (+ B C))) ## Addition Over Inequality ## ## (> A ] [ B ] ) ## (> (+ A ] C) (+ [ B ] C)) ##
stmt (gtadd2i () ((> A B)) (> (+ C A) (+ C B))) ## Addition Over Inequality ## ## (>= A ] [ B ] ) ## (>= (+ A ] C) (+ [ B ] C)) ##
stmt (geadd1i () ((>= A B)) (>= (+ A C) (+ B C))) ## Addition Over Inequality ## ## (>= [ A ] [ B ) ## (>= (+ C [ A ] ) (+ C [ B )) ##
stmt (geadd2i () ((>= A B)) (>= (+ C A) (+ C B))) ## ≥ means > OR = ## right('Equivalence', '∨') left('Simplify', '≥') stmt (gegeo () () (<-> (>= A B) (\/ (> A B) (= A B)))) ## ≤ means < OR = ## right('Equivalence', '∨') left('Simplify', '≤') stmt (leleo () () (<-> (<= A B) (\/ (< A B) (= A B)))) ## Multiply by 0 ## This rederives one of the Peano axioms. stmt (mul0 () () (= (* A (0)) (0))) ## Multiply by 0 ## auto-right('Simplify','0') stmt (mul0r () () (= (* (0) A) (0))) ## Converse of ≤ ## right('Commute', '≤') left('Commute', '≥') stmt (lecon () () (<-> (<= A B) (>= B A))) ## Converse of ≤ stmt (leconi () ((<= A B)) (>= B A)) ## Converse of ≤ ## right('Commute', '≤') left('Commute', '≥') stmt (leconold () () (<-> (<= A B) (-. (< B A)))) ## Converse of < ## right('Commute', '<') left('Commute', '>') stmt (ltcon () () (<-> (< A B) (> B A))) ## Converse of < stmt (ltconi () ((< A B)) (> B A)) ## Def. Greater Than or Equal to ## right('Define', '≤') left('Simplify', '≥') stmt (df-ge () () (<-> (>= A B) (-. (< A B)))) ## Def. Greater Than ## right('Define', '<') left('Simplify', '>') stmt (df-gt () () (<-> (> A B) (-. (<= A B)))) ## Def. Greater Than or Equal ## right('Simplify', '<') stmt (notge () () (<-> (-. (>= A B)) (< A B))) ## Def. Greater Than ## right('Simplify', ' ≤') stmt (notgt () () (<-> (-. (> A B)) (<= A B))) ## Distributive Property ## right('Distribute', 'L') left('Distribute', '-L') stmt (distl () () (= (* (+ A B) C) (+ (* A C) (* B C)))) ## Distributive Property ## ## (= (* (+ A B) (+ C D)) (+ (+ (* A C) (* B C)) (+ (* A D) (* B D)))) ##
## Distribution of addition through multiplication, both arguments ## right('Distribute', 'RL') left('Distribute', 'RL') stmt (distrl () () (= (* (+ A B) (+ C D)) (+ (+ (* A C) (* B C)) (+ (* A D) (* B D))))) ## Definition of Less Than stmt (df-lt () () (<-> (< A B) (/\ (<= A B) (-. (= A B))))) ## Equivalence for < ## stmt (lteq1 () () (-> (= A C) (<-> (< A B) (< C B)))) ## Equivalence for < ## stmt (lteq2 () () (-> (= B C) (<-> (< A B) (< A C)))) ## Equivalence over Inequality ## ## (= A ] ] [ B ] ) ## (<-> (< A ] C ] ) (< [ B ] C)) ##
stmt (lteq1i () ((= A B)) (<-> (< A C) (< B C))) ## Equivalence over Inequality ## ## (= [ A ] [ [ B ] ) ## (<-> (< C [ A ] ) (< [ C [ B ] )) ##
stmt (lteq2i () ((= A B)) (<-> (< C A) (< C B))) stmt (lteq1d () ( (-> ph (= A C))) (-> ph (<-> (< A B) (< C B)))) stmt (lteq2d () ( (-> ph (= B C))) (-> ph (<-> (< A B) (< A C)))) ## Equality over Addition ## ## (= A ] [ B ] ) ## (= (+ A ] C) (+ [ B ] C)) ##
stmt (addeq1i () ((= A B)) (= (+ A C) (+ B C))) ## Equality over Addition ## ## (= [ A ] [ B ) ## (= (+ C [ A ] ) (+ C [ B)) ##
stmt (addeq2i () ((= A B)) (= (+ C A) (+ C B))) ## Equality over Multiplication ## ## (= A ] [ B ] ) ## (= (* A ] C) (* [ B ] C)) ##
stmt (muleq1i () ((= A B)) (= (* A C) (* B C))) ## Equality over Multiplication ## ## (= [ A ] [ B ) ## (= (* C [ A ] ) (* C [ B)) ##
stmt (muleq2i () ((= A B)) (= (* C A) (* C B))) ## Equivalence over Inequality ## ## (<= A ] ] ] [ C) ## (= A ] [ B ] ] ) ## (<= [ [ B ] [ C) ##
stmt (leeq1ii () ((<= A C) (= A B)) (<= B C)) ## Equivalence over Inequality ## ## (<= C [ A ] ] ) ## (= [ A ] [ B) ## (<= C [ [ [ B) ##
stmt (leeq2ii () ((<= C A) (= A B)) (<= C B)) ## Equivalence over Inequality ## ## (< A ] ] ] [ C) ## (= A ] [ B ] ] ) ## (< [ [ B ] [ C) ##
stmt (lteq1ii () ((< A C) (= A B)) (< B C)) ## Equivalence over Inequality ## ## (< C [ A ] ] ) ## (= [ A ] [ B) ## (< C [ [ [ B) ##
stmt (lteq2ii () ((< C A) (= A B)) (< C B)) ## Convert between inequalities stmt (axlttri2i () ((-. (= A B)) (<= A B)) (< A B)) ## Multiplication is Monotonic ## ## (< B ] ] ] [ C ] ] ) ## (< [ [ (0) ] [ [ [ A ) ## (< (* B ] [ A ] ) (* [ C ] [ A )) ##
stmt (ltmul2i () ((< B C) (< (0) A)) (< (* B A) (* C A))) ## A number is less, equal, or greater stmt (inequalities () () (\/ (< A B) (\/ (= A B) (> A B)))) ## Multiplication is Monotonic ## ## (> B ] ] ] [ C ] ] ) ## (> [ [ A ] [ [ [ (0) ) ## (> (+ B ] [ A ] ) (+ [ C ] [ A )) ##
stmt (gtmul2i () ((> B C) (> A (0))) (> (* B A) (* C A))) stmt (gemul1 () () (-> (/\ (>= B A) (>= C (0))) (>= (* B C) (* A C)))) ## Inequality Conversion stmt (axgrtrii () ((-. (= A B)) (>= A B)) (> A B)) ## Transitive Property ## right('Simplify', '< <') stmt (lttr () () (-> (/\ (< A B) (< B C)) (< A C))) ## Transitive law ## right('Simplify', '<') stmt (lelttr () () (-> (/\ (<= A B) (< B C)) (< A C))) ## Transitive law ## right('Simplify', '<') stmt (ltletr () () (-> (/\ (< A B) (<= B C)) (< A C))) ## Transitive Inequality ## right('Transitive', '≥') stmt (getr () () (-> (/\ (>= A B) (>= B C)) (>= A C))) ## Transitive Inequality ## right('Transitive', '>') stmt (gtgetr () () (-> (/\ (> C B) (>= B A)) (> C A))) ## Transitive Inequality ## right('Transitive', '>') stmt (gegttr () () (-> (/\ (>= C B) (> B A)) (> C A))) ## Transitive Inequality ## right('Transitive', '>') stmt (gttr () () (-> (/\ (> A B) (> B C)) (> A C))) ## Transitive Inequality ## ## (< [ B ] [ [ C ] ) ## (-> (< A [ B ] ) (< [ A [ C ] )) ##
stmt (ltTrlt () ((< B C)) (-> (< A B) (< A C))) ## Transitive Inequality ## ## (< [ B ] [ [ C ] ) ## (-> (<= A [ B ] ) (< [ A [ C ] )) ##
stmt (ltTrle () ((< B C)) (-> (<= A B) (< A C))) ## Transitive Inequality ## ## (< [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (< [ A [ C ] )) ##
stmt (ltTreq () ((< B C)) (-> (= A B) (< A C))) ## Transitive Inequality ## ## (<= [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (<= [ A [ C ] )) ##
stmt (leTreq () ((<= B C)) (-> (= A B) (<= A C))) ## Transitive Inequality ## ## (<= [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (<= [ A [ C ] )) ##
stmt (leTrlt () ((<= B C)) (-> (< A B) (< A C))) ## Transitive Inequality ## ## (<= [ B ] [ [ C ] ) ## (-> (<= A [ B ] ) (<= [ A [ C ] )) ##
stmt (leTrle () ((<= B C)) (-> (<= A B) (<= A C))) ## Transitive Inequality ## ## (-. (> [ B ] [ [ C ] )) ## (-> (> A [ B ] ) (> [ A [ C ] )) ##
stmt (gtTrgt () ((> B C)) (-> (> A B) (> A C))) ## Transitive Inequality ## ## (>= [ B ] [ [ C ] ) ## (-> (> A [ B ] ) (> [ A [ C ] )) ##
stmt (geTrgt () ((>= B C)) (-> (> A B) (> A C))) ## Transitive Inequality ## ## (>= [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (>= [ A [ C ] )) ##
stmt (geTreq () ((>= B C)) (-> (= A B) (>= A C))) ## Transitive Inequality ## ## (> [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (> [ A [ C ] )) ##
stmt (gtTreq () ((> B C)) (-> (= A B) (> A C))) ## Transitive Inequality ## ## (> [ B ] [ [ C ] ) ## (-> (>= A [ B ] )) (> [ A [ C ] )) ##
stmt (gtTrge () ((> B C)) (-> (>= C A) (> B A))) ## Transitive Inequality ## ## (>= [ B ] [ [ C ] ) ## (-> (>= A [ B ] ) (>= [ A [ C ] )) ##
stmt (geTrge () ((>= B C)) (-> (>= A B) (>= A C))) # This is identical to eqtr. So ideally we would use eqtr instead. ## Substitution ## ## (= A [ B ] ] ] ) ## (= [ B ] [ C ] ) ## (= A [ [ [ C ] ) ##
stmt (EqReplaceEq1 () ((= A B) (= B C)) (= A C)) ## Equivalence for >= stmt (geeq1 () () (-> (= A C) (<-> (>= A B) (>= C B)))) ## Equivalence for >= stmt (geeq2 () () (-> (= B C) (<-> (>= A B) (>= A C)))) ## Equivalence over Inequality ## ## (= A ] ] [ B ] ) ## (<-> (>= A ] C ] ) (>= [ B ] C)) ##
stmt (geeq1i () ( (= A C)) (<-> (>= A B) (>= C B))) ## Equivalence over Inequality ## ## (= [ A ] [ [ B ] ) ## (<-> (>= C [ A ] ) (>= [ C [ B ] )) ##
stmt (geeq2i () ((= A B)) (<-> (>= C A) (>= C B))) stmt (geeq1d () ( (-> ph (= A C))) (-> ph (<-> (>= A B) (>= C B)))) stmt (geeq2d () ( (-> ph (= B C))) (-> ph (<-> (>= A B) (>= A C)))) stmt (gteq1 () () (-> (= A C) (<-> (> A B) (> C B)))) stmt (gteq2 () () (-> (= B C) (<-> (> A B) (> A C)))) ## Equivalence over Inequality ## ## (= A ] ] [ B ] ) ## (<-> (> A ] C ] ) (> [ B ] C)) ##
stmt (gteq1i () ((= A C)) (<-> (> A B) (> C B))) ## Equivalence over Inequality ## ## (= [ A ] [ [ B ] ) ## (<-> (> C [ A ] ) (> [ C [ B ] )) ##
stmt (gteq2i () ((= B C)) (<-> (> A B) (> A C))) stmt (gteq1d () ( (-> ph (= A C))) (-> ph (<-> (> A B) (> C B)))) stmt (gteq2d () ( (-> ph (= B C))) (-> ph (<-> (> A B) (> A C)))) ## Operator Conversion ## right('Infer', '≠') stmt (ltneq () () (-> (< A B) (-. (= A B)))) ## Inequality Conversion ## right('Infer', '≤') stmt (ltle () () (-> (< A B) (<= A B))) ## Inequality Conversion ## right('Infer', '≠') stmt (gtneq () () (-> (> A B) (-. (= A B)))) ## Inequality Conversion ## right('Infer', '≥') stmt (gtge () () (-> (> A B) (>= A B))) ## Equality Conversion ## right('Infer', '≤') stmt (eqle() () (-> (= A B) (<= A B))) ## Equality Conversion ## right('Infer', '≥') stmt (eqge() () (-> (= A B) (>= A B))) ## Equality Conversion ## right('Infer', '¬<') stmt (eqnlt () () (-> (= A B) (-. (< A B)))) ## Inequality Conversion ## right('Infer', '¬<') stmt (gtnlt () () (-> (> A B) (-. (< A B)))) ## Inequality Conversion ## right('Infer', '¬≤') stmt (gtnle () () (-> (> A B) (-. (<= A B)))) ## Inequality Conversion ## right('Infer', '¬>') stmt (ltngt () () (-> (< A B) (-. (> A B)))) ## Inequality Conversion ## right('Infer', '¬≥') stmt (ltnge () () (-> (< A B) (-. (>= A B)))) ## Inequality Conversion ## right('Infer', '¬>') stmt (eqngt () () (-> (= A B) (-. (> A B)))) ## ## redirect ../common/add_multiply.ghi ## ## Add a number to both sides of an equation ## ## (-> (= A B) (= (+ A C) (+ B C))) ##