# The reals have not been constructed yet and this list is missing essential properties of the reals. 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) ##
stmt (addneq2i () ((-. (= A B))) (-. (= (+ C A) (+ C 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))) ## 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))))) ## 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))) # 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)) ## Add a number to both sides of an equation ## ## (-> (= A B) (= (+ A C) (+ B C))) ##
stmt (muleq1 () () (-> (= A B) (= (* A C) (* B C)))) ## Equality over Multiplication ## ## (-> (= A B) (= (* C A) (* C B))) ##
stmt (muleq2 () () (-> (= A B) (= (* C A) (* C B)))) ## Equality over Multiplication stmt (muleq1d () ((-> ph (= A B))) (-> ph (= (* A C) (* B C)))) stmt (muleq2d () ((-> ph (= A B))) (-> ph (= (* C A) (* C B)))) stmt (muleq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (* A C) (* B D)))) ## Equality over Multiplication stmt (muleq12i () ((= A B) (= C D)) (= (* A C) (* B D))) ## Cancellation of addition stmt (addcan2 () () (<-> (= (+ A B) (+ A C)) (= B C))) ## Rearrange Addition Terms ## ## (= (+ (+ A B) (+ C D)) (+ (+ A C) (+ B D))) ##
stmt (add4 () () (= (+ (+ A B) (+ C D)) (+ (+ A C) (+ B D)))) ## Rearrange the second and fourth terms ## ## (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ C B))) ##
stmt (add24 () () (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ C B)))) ## Rearrange Addition Terms ## ## (= (+ (+ A B) C) (+ (+ A C) B)) ##
stmt (add23 () () (= (+ (+ A B) C) (+ (+ A C) B))) ## Rearrange Addition Terms stmt (add432 () () (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ B C)))) ## Cancel Addition ## ## (= (+ A ] C ) ] (+ [ B C)) ## (= A ] ] [ B) ##
stmt (addcani () ((= (+ A C) (+ B C))) (= A B)) ## Cancel Addition ## ## (= (+ C [ A ) ] (+ C [ B )) ## (= [ A ] [ B) ##
stmt (addcan2i () ((= (+ C A) (+ C B))) (= A B)) ## Reorder Multiplication Terms stmt (mul4() () (= (* (* A B) (* C D)) (* (* A C) (* B D)))) ## Reorder Multiplication Terms stmt (mul42() () (= (* (* A B) (* C D)) (* (* A D) (* C B)))) ## Commutative Property stmt (mulcom12 () () (= (* A (* B C)) (* B (* A C)))) 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.gh ## ## Inequality Conversion ## left('Simplify', '<') stmt (axlttri2 () () (<-> (< A B) (/\ (-. (= A B)) (<= A B)))) ## Inequality Conversion ## left('Simplify', '>') stmt (axgrtri () () (<-> (> A B) (/\ (-. (= A B)) (>= A B)))) ## 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))) ## 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))) ## 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)))) ## 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)) ## Equivalence for ≤ stmt (leeq12 () () (-> (/\ (= A B) (= C D)) (<-> (<= A C) (<= B D)))) stmt (leeq12d () ( (-> ph (= A B)) (-> ph (= C D))) (-> ph (<-> (<= A C) (<= B D)))) ## 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))) ## 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))) ## 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)))) ## Equivalence over Inequality ## Equality inference for less than or equal relation ## ## (= A ] ] [ B ] ) ## (<-> (<= A ] C ] ) (<= [ B ] C)) ##
stmt (leeq1i () ((= A B)) (<-> (<= A C) (<= B C))) ## Equivalence over Inequality ## Equality inference for less than or equal relation ## ## (= [ A ] [ [ B ] ) ## (<-> (<= C [ A ] ) (<= [ C [ B ] )) ##
stmt (leeq2i () ((= A B)) (<-> (<= C A) (<= C B))) ## Inequality Equivalence ## Equality deduction for less than or equal relation stmt (leeq1d () ((-> ph (= A B))) (-> ph (<-> (<= A C) (<= B C)))) ## Inequality Equivalence ## Equality deduction for less than or equal relation ## ## (-> ph (= [ A ] [ [ B ] )) ## (-> ph (<-> (<= C [ A ] ) (<= [ C [ B ] ))) ##
stmt (leeq2d () ((-> ph (= A B))) (-> ph (<-> (<= C A) (<= C B)))) ## Inequality relation for two equal sums stmt (leadd12 () () (-> (= (+ A B) (+ C D)) (<-> (<= A C) (<= D B)))) ## 1 is more than 0 stmt (1greater0 () () (> (1) (0))) ## Definition of a Positive Number ## left('Simplify', '+') stmt (df-pos () () (<-> (pos A) (> A (0)))) stmt (poseq () () (-> (= A B) (<-> (pos A) (pos B)))) stmt (poseqi () ((= A B)) (<-> (pos A) (pos B))) stmt (1pos () () (pos (1))) ## Definition of a Negative Number ## left('Simplify', '-') stmt (df-zneg () () (<-> (zneg A) (< A (0)))) stmt (znegeq () () (-> (= A B) (<-> (zneg A) (zneg B)))) stmt (znegeqi () ((= A B)) (<-> (zneg A) (zneg B))) stmt (znegeqd () ((-> ph (= A B))) (-> ph (<-> (zneg A) (zneg B)))) ## 0 is not positive stmt (0NotPos () () (-. (pos (0)))) ## 0 is not negative stmt (0NotNeg () () (-. (zneg (0)))) ## 0 is not positive stmt (0NotPosd () () (-> (= A (0)) (-. (pos A)))) ## 0 is not positive stmt (0NotNegd () () (-> (= A (0)) (-. (zneg A)))) ## Multiply Two Positive Numbers stmt (posproduct1 () () (-> (/\ (pos A) (pos B)) (pos (* A B)))) stmt (neqlt () () (-> (-. (= A B)) (\/ (< A B) (> A B)))) stmt (ltmul0 () () (-> (/\ (< (0) A) (< (0) B)) (< (0) (* A B)))) stmt (gtmul0() () (-> (/\ (> A (0)) (> B (0))) (> (* A B) (0)))) ## Multiply Both Sides ## Multiplication is monotonic in its second argument stmt (lemul2 () () (-> (/\ (<= A B) (<= (0) C)) (<= (* C A) (* C B)))) ## Addition is Monotonic ## Addition is strictly monotonic in the first addend ## left('Cancel', '+') ## ## (<-> (<= A B) (<= (+ A C) (+ B C))) ##
stmt (leadd1 () () (<-> (<= A B) (<= (+ A C) (+ B C)))) stmt (lemul4 () () (-> (/\ (<= A B) (<= C D)) (<= (+ (* A D) (* B C)) (+ (* A C) (* B D))))) ## Multiply Nonequal Numbers stmt (ltmul1 () () (-> (/\ (< A B) (< (0) C)) (< (* A C) (* B C)))) stmt (ltmul4 () () (-> (/\ (< A B) (< C D)) (< (+ (* A D) (* B C)) (+ (* A C) (* B D))))) stmt (gtmul2 () () (-> (/\ (> A B) (> C (0))) (> (* C A) (* C B)))) stmt (gemul1 () () (-> (/\ (>= B A) (>= C (0))) (>= (* B C) (* A C)))) ## Less Than or Equal from Positive Difference stmt (exlt ((A x)(B x)) () (-> (< A B) (E. x (/\ (< (0) x) (= (+ A x) B))))) ## ## redirect ../common/mulcan.gh ## 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/ifn.gh ## ## First branch of ternary expression stmt (ifn1 () () (-> ph (= (ifn ph A B) A))) ## Second branch of ternary expression stmt (ifn2 () () (-> (-. ph) (= (ifn ph A B) B))) ## Equivalence of predicate in ifn stmt (ifnbi1 () () (-> (<-> ph ps) (= (ifn ph A B) (ifn ps A B)))) stmt (ifnbi1i () ( (<-> ph ps)) (= (ifn ph A B) (ifn ps A B))) stmt (ifnbi1d () ( (-> ch (<-> ph ps))) (-> ch (= (ifn ph A B) (ifn ps A B)))) ## Equality of first term for ifn stmt (ifneq2 () () (-> (= A B) (= (ifn ph A C) (ifn ph B C)))) stmt (ifneq2i () ( (= A B)) (= (ifn ph A C) (ifn ph B C))) stmt (ifneq2d () ( (-> ps (= A B))) (-> ps (= (ifn ph A C) (ifn ph B C)))) ## Equality of second term for ifn stmt (ifneq3 () () (-> (= A B) (= (ifn ph C A) (ifn ph C B)))) stmt (ifneq3i () ( (= A B)) (= (ifn ph C A) (ifn ph C B))) stmt (ifneq3d () ( (-> ps (= A B))) (-> ps (= (ifn ph C A) (ifn ph C B)))) stmt (ifneq13 () () (-> (/\ (<-> ph ps) (= A B)) (= (ifn ph C A) (ifn ps C B)))) ## Equivalence for ifn stmt (ifnbi123 () () (-> (/\ (<-> ph ps) (/\ (= A C) (= B D))) (= (ifn ph A B) (ifn ps C D)))) stmt (ifnbi123d () ( (-> ph (<-> ps ch)) (-> ph (= A B)) (-> ph (= C D))) (-> ph (= (ifn ps A C) (ifn ch B D)))) ## ## redirect ../common/negative.ghi ## term (nat (-n A)) ## Cancel using subtraction ## right('Simplify','-') stmt (negcan () () (= (+ A (-n A)) (0))) stmt (negeq () () (-> (= A B) (= (-n A) (-n B)))) term (nat (- A B)) ## ## (= [ A [ B) ## (= (-n [ A) (-n [ B)) ##
stmt (negeqi() ((= A B)) (= (-n A) (-n B))) stmt (negeqd () ((-> ph (= A B))) (-> ph (= (-n A) (-n B)))) stmt (negeq2() () (<-> (= A B) (= (-n A) (-n B)))) ## Negative can switch sides ## right('Equivalence', '-') left('Equivalence', '-') stmt (negeq3 () () (<-> (= A (-n B)) (= (-n A) B))) ## Double Negative ## right('Simplify', '-') stmt (doubleneg () () (= (-n (-n A)) A)) ## Negative of 0 is 0 ## right('Simplify', '0') stmt (neg0 () () (= (-n (0)) (0))) ## Negative 1 is not 0 stmt (neg1ne0 () () (-. (= (-n (1)) (0)))) ## Nonzero negatives are not zero stmt (negne0 () () (<-> (-. (= A (0))) (-. (= (-n A) (0))))) ## Cancel using subtraction ## right('Simplify','-') stmt (negcan2() () (= (+ (-n A) A) (0))) ## Definition of Subtraction ## right('Define', '-') left('Simplify', '-') stmt (df-minus () () (= (- A B) (+ A (-n B)))) ## Minus Definition Reversed stmt (df-minusr () () (= (+ A (-n B)) (- A B))) ## Subtract a number from both sides stmt (minuseq1 () () (-> (= A C) (= (- A B) (- C B)))) ## Subtract a number from both sides ## ## (= A ] ] C ] ) ## (= (- A ] B ] ) (- C ] B)) ##
stmt (minuseq1i () ((= A C)) (= (- A B) (- C B))) ## Equivalence for - ## stmt (minuseq2 () () (-> (= B C) (= (- A B) (- A C)))) stmt (minuseq1d () ((-> ph (= A C))) (-> ph (= (- A B) (- C B)))) stmt (minuseq2i () ((= B C)) (= (- A B) (- A C))) stmt (minuseq2d () ((-> ph (= B C))) (-> ph (= (- A B) (- A C)))) stmt (minuseq12 () () (-> (/\ (= A B) (= C D)) (= (- A C) (- B D)))) ## Equality over Subtraction stmt (minuseq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (- A C) (- B D)))) ## Equality over Subtraction ## ## (= A ] ] ] [ B ] ] ) ## (= [ [ C ] [ [ [ D) ## (= (- A ] [ C ] ) (- [ B ] [ D)) ##
stmt (minuseq12i () ((= A B) (= C D)) (= (- A C) (- B D))) ## Cancel using subtraction ## right('Simplify','-') stmt (minuscan () () (= (- A A) (0))) ## Addition is the inverse of Subtraction ## right('Simplify','-') stmt (minuscan2 () () (= (+ (- A B) B) A)) ## Addition is the inverse of Subtraction ## right('Simplify','-') ## ## (= (- (+ A B) B) A) ##
stmt (addcanr () () (= (- (+ A B) B) A)) ## Negative and Subtraction Cancel ## right('Simplify', '-') stmt (minusneg () () (= (- A (-n B)) (+ A B))) ## Negative Multiplication ## right('Simplify', '-') stmt (negmul () () (= (* (-n A) B) (-n (* A B)))) ## Negative Multiplication ## right('Simplify', '-') stmt (negmul2 () () (= (* A (-n B)) (-n (* A B)))) ## Multiply by Negative 1 stmt (mulneg1 () () (= (* (-n (1)) A) (-n A))) ## Multiply Two Negative Numbers ## right('Simplify', '-') stmt (doublenegmul () () (= (* (-n A) (-n B)) (* A B))) ## Distribute Multiplication over Subtraction ## ## (= (* A (- B C)) (- (* A B) (* A C))) ##
## right('Distribute', 'R') left('Distribute', '-R') stmt (minusdistr () () (= (* A (- B C)) (- (* A B) (* A C)))) ## Distribute Multiplication over Subtraction ## ## (= (* (- A B) C) (- (* A C) (* B C))) ##
## right('Distribute', 'L') left('Distribute', '-L') stmt (minusdistl () () (= (* (- A B) C) (- (* A C) (* B C)))) ## Multiply Two Negative Numbers stmt (negProduct () () (-> (/\ (zneg A) (zneg B)) (pos (* A B)))) ## Squares are not negative stmt (posSquares () () (-> (-. (= A (0))) (pos (* A A)))) ## Squares are not negative stmt (squareNotNeg () () (>= (* A A) (0))) ## Negative numbers are not positive stmt (negNotPos () () (-> (zneg A) (-. (pos A)))) ## Positive numbers are not negative stmt (posNotNeg () () (-> (pos A) (-. (zneg A)))) stmt (posProduct () () (<-> (pos (* A B)) (\/ (/\ (zneg A) (zneg B)) (/\ (pos A) (pos B))))) stmt (productPos () () (-> (pos (* A B)) (<-> (pos A) (pos B)))) ## Positive Proof by Cases stmt (posCases () () (-> (/\ (-. (zneg A)) (-. (= A (0)))) (pos A))) stmt (notPos () () (-> (-. (pos A)) (\/ (zneg A) (= A (0))))) ## Negative of a positive number stmt (negPositive () () (<-> (pos (-n A)) (zneg A))) ## Negative of Subtraction ## left('Simplify', '-') stmt (negminus () () (= (- A B) (-n (- B A)))) ## Negative of Subtraction stmt (negminus2 () () (= (+ (-n A) B) (-n (- A B)))) ## Negative of Subtraction stmt (negminus3 () () (= (- (-n A) B) (-n (+ A B)))) ## Negative distributes over addition stmt (negadd () () (= (- (-n A) B) (-n (+ A B)))) ## Subtraction Value from Addition stmt (minusValue () () (-> (= (+ A B) C) (= A (- C B)))) ## Subtract both sides ## ## (= (+ A B) C) ## (= A (- C B ) ) ##
stmt (minusValuei () ((= (+ A B) C)) (= A (- C B))) ## Subtraction from both sides ## ## (= (+ A B ) [ C) ## (= A (- (-n B ) [ C) ) ##
stmt (minusValue2i () ((= (+ A B) C)) (= A (+ (-n B) C))) ## Subtraction Value from Addition ## ## (= (+ A B) C) ## (= (- C B ) A ) ##
stmt (minusValue3i () ((= (+ A B) C)) (= (- C B) A)) ## Subtract from 0 ## right('Simplify', '-') stmt (0minus () () (= (- (0) A) (-n A))) ## Subtraction Identity ## right('Simplify', '0') stmt (minusid () () (= (- A (0)) A)) ## Add or subtract on both sides stmt (gediff () () (<-> (>= A B) (>= (- A B) (0)))) ## Add or subtract on both sides stmt (gtdiff () () (<-> (> A B) (> (- A B) (0)))) ## Positive Number Subtraction stmt (subtractPositive () () (<-> (> B (0)) (< (- A B) A))) stmt (negle () () (<-> (>= A (0)) (<= (-n A) (0)))) stmt (neglt () () (<-> (< (-n A) (0)) (> A (0)))) stmt (negge () () (<-> (>= (-n A) (0)) (<= A (0)))) stmt (neggt () () (<-> (> (-n A) (0)) (< A (0)))) term (nat (abs A)) ## Definition of Absolute Value ## right('Define', '|x|') left('Simplify', '|x|') stmt (df-abs () () (= (abs A) (ifn (>= A (0)) A (-n A)))) ## Equivalence for abs ## stmt (abseq () () (-> (= A B) (= (abs A) (abs B)))) stmt (abseqi () ( (= A B)) (= (abs A) (abs B))) stmt (abseqd () ( (-> ph (= A B))) (-> ph (= (abs A) (abs B)))) ## Def. Absolute Value for Positive Numbers stmt (dfabs1 () () (-> (>= A (0)) (= (abs A) A))) ## Def. Absolute Value for Negative Numbers stmt (dfabs2 () () (-> (< A (0)) (= (abs A) (-n A)))) ## The absolute value is not negative stmt (absNotNeg () () (>= (abs A) (0))) ## The absolute value is idempotent stmt (absidm () () (= (abs (abs A)) (abs A))) ## The absolute value is positive definite stmt (absPosDef () () (<-> (= A (0)) (= (abs A) (0)))) ## Two numbers have the same absolute value stmt (absTwoValues () () (<-> (= (abs A) B) (/\ (\/ (= A B) (= (-n A) B)) (>= B (0))))) stmt (absTwoValues2 () () (\/ (= (abs A) A) (= (abs A) (-n A)))) ## ## redirect ../common/division.ghi ## term (nat (/ A B)) stmt (diveq12 () () (-> (/\ (= A B) (= C D)) (= (/ A C) (/ B D)))) stmt (divcan () () (-> (-. (= B (0))) (= (* B (/ A B)) A))) ## Divide a number on both sides of an equation ## ## (-> (= A B) (= (/ A C) (/ B C))) ##
stmt (diveq1 () () (-> (= A B) (= (/ A C) (/ B C)))) ## Divide a number on both sides ## ## (= A ] ] [ B ] ) ## (= (/ A ] C) ] (/ [ B ] C)) ##
stmt (diveq1i () ((= A B)) (= (/ A C) (/ B C))) ## Equality over Division stmt (diveq1d () ((-> ph (= A B))) (-> ph (= (/ A C) (/ B C)))) ## Divide a number on both sides of an equation stmt (diveq2 () () (-> (= A B) (= (/ C A) (/ C B)))) ## Divide a number on both sides ## ## (= [ A ] [ [ B ) ## (= (/ C [ A ] ) [ (/ C [ B)) ##
stmt (diveq2i () ((= A B)) (= (/ C A) (/ C B))) ## Equality over Division stmt (diveq2d () ((-> ph (= A B))) (-> ph (= (/ C A) (/ C B)))) ## Equality over Division ## ## (= A ] ] ] [ B ] ] ) ## (= [ [ C ] [ [ [ D) ## (= (/ A ] [ C ] ) (/ [ B ] [ D)) ##
stmt (diveq12i () ((= A B) (= C D)) (= (/ A C) (/ B D))) ## Equality over Division stmt (diveq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (/ A C) (/ B D)))) ## Cancel with Division stmt (divcani () ((-. (= A (0)))) (= (* A (/ B A)) B)) ## Cancel with Division stmt (reciprocalcan () () (-> (-. (= A (0))) (= (* A (/ (1) A)) (1)))) ## Cancel with Division stmt (reciprocalcani () ((-. (= A (0)))) (= (* A (/ (1) A)) (1))) ## Cancel With Division stmt (divcan2 () () (-> (-. (= A (0))) (= (/ (* A B) A) B))) ## Cancel with Division ## ## (-. (= A (0))) ## (= (/ (* A B) A) B) ##
stmt (divcan2i () ((-. (= A (0)))) (= (/ (* A B) A) B)) ## Cancel with Division stmt (divcan3 () () (-> (-. (= A (0))) (= (/ (* B A) A) B))) ## Divide by 1 stmt (divid () () (= (/ A (1)) A)) ## Expand Fraction stmt (expandFrac () () (-> (-. (= B (0))) (= (/ A B) (* A (/ (1) B))))) ## Expand Fraction stmt (expandFraci () ((-. (= B (0)))) (= (/ A B) (* A (/ (1) B)))) ## Cancel using Division stmt (frac1 () () (-> (-. (= A (0))) (= (/ A A) (1)))) ## Cancel using Division stmt (frac1i () ((-. (= A (0)))) (= (/ A A) (1))) ## Division & Multiplication Ass. stmt (divmulass () () (-> (-. (= C (0))) (= (* A (/ B C)) (/ (* A B) C)))) ## Division & Multiplication Ass. stmt (divmulassi () ((-. (= C (0)))) (= (* A (/ B C)) (/ (* A B) C))) ## Division & Multiplication Ass. stmt (divmulass2i () ((-. (= C (0)))) (= (* (/ B C) A) (/ (* B A) C))) ## Zero Product Property ## ## (-. (= A ] ] ] (0))) ## (-. (= [ [ B ] (0))) ## (-. (= (* A ] [ B ] ) (0))) ##
stmt (zeroProducti () ((-. (= A (0))) (-. (= B (0)))) (-. (= (* A B) (0)))) ## Multiply Fractions stmt (fracmul () () (-> (/\ (-. (= B (0))) (-. (= D (0)))) (= (* (/ A B) (/ C D)) (/ (* A C) (* B D))))) ## Multiply Fractions stmt (fracmuli () ((-. (= B (0))) (-. (= D (0)))) (= (* (/ A B) (/ C D)) (/ (* A C) (* B D)))) ## Fraction with common factor ## Numerators and Denominators with common factors can be simplified. stmt (fracFactors () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (* A C) (* B C)) (/ A B)))) ## Fraction with common factor ## Numerators and Denominators with common factors can be simplified. stmt (fracFactorsi () ((-. (= B (0))) (-. (= C (0)))) (= (/ (* A C) (* B C)) (/ A B))) ## Distribute Division over Addition stmt (divdistr () () (-> (-. (= C (0))) (= (+ (/ A C) (/ B C)) (/ (+ A B) C)))) ## Distribute Division over Addition stmt (divdistri () ((-. (= C (0)))) (= (+ (/ A C) (/ B C)) (/ (+ A B) C))) ## Add Fractions stmt (addfrac () () (-> (/\ (-. (= B (0))) (-. (= D (0)))) (= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D))))) ## Add Fractions stmt (addfraci () ((-. (= B (0))) (-. (= D (0)))) (= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D)))) ## Negative Numerator ## A negative numerator is equivalent to a negative fraction. stmt (negNumerator () () (-> (-. (= B (0))) (= (/ (-n A) B) (-n (/ A B))))) ## Negative Numerator stmt (negNumeratori () ((-. (= B (0)))) (= (/ (-n A) B) (-n (/ A B)))) ## Negative Denominator stmt (negDenominatori () ((-. (= B (0)))) (= (/ A (-n B)) (-n (/ A B)))) stmt (negDenominator () () (-> (-. (= B (0))) (= (-n (/ A B)) (/ A (-n B))))) ## Double Negative Fraction stmt (doublenegfrac () () (-> (-. (= B (0))) (= (/ (-n A) (-n B)) (/ A B)))) ## Double Negative Fraction stmt (doublenegfraci () ((-. (= B (0)))) (= (/ (-n A) (-n B)) (/ A B))) ## Common Division in Fraction stmt (fracFactors2 () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A C) (/ B C)) (/ A B)))) ## Common Division in Fraction stmt (fracFactors2i () ((-. (= B (0))) (-. (= C (0)))) (= (/ (/ A C) (/ B C)) (/ A B))) ## Commute Division stmt (divcom () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ (/ A C) B)))) ## Distribute Division Over Subtraction stmt (divminusdistr () () (-> (-. (= C (0))) (= (- (/ A C) (/ B C)) (/ (- A B) C)))) ## Distribute Division Over Subtraction stmt (divminusdistri () ((-. (= C (0)))) (= (- (/ A C) (/ B C)) (/ (- A B) C))) ## 0 divided by anything is 0 stmt (0div () () (-> (-. (= A (0))) (= (/ (0) A) (0)))) ## 0 divided by anything is 0 stmt (0divi () ((-. (= A (0)))) (= (/ (0) A) (0))) ## Combine Two Divisions stmt (doublediv () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ A (* B C))))) ## Combine Two Divisions stmt (doubledivi () ((-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ A (* B C)))) ## A positive number has a positive reciprocal stmt (posReciprocal () () (-> (> A (0)) (> (/ (1) A) (0)))) stmt (posReciprocal2 () () (-> (-. (= A (0))) (<-> (> A (0)) (> (/ (1) A) (0))))) ## A number is its reciprocal's reciprocal stmt (doubleReciprocal () () (-> (-. (= A (0))) (= (/ (1) (/ (1) A)) A))) stmt (divDouble () () (-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ A (/ B C)) (/ (* A C) B)))) stmt (divNotZeroi () ((-. (= A (0))) (-. (= B (0)))) (-. (= (/ A B) (0)))) stmt (divNotZero () () (-> (/\ (-. (= A (0))) (-. (= B (0)))) (-. (= (/ A B) (0))))) ## ## redirect ../common/exponent.ghi ## term (nat (exp A B)) ## Equivalence for exp stmt (expeq1 () () (-> (= A B) (= (exp A C) (exp B C)))) ## Equivalence for exp stmt (expeq2 () () (-> (= B C) (= (exp A B) (exp A C)))) ## 0th power of a number is 1 ## right('Simplify', '1') stmt (exp0 () () (= (exp A (0)) (1))) ## Multiply by the base for the next power stmt (expplus1 () () (= (exp A (+ B (1))) (* A (exp A B)))) stmt (expeq1i () ( (= A B)) (= (exp A C) (exp B C))) stmt (expeq1d () ( (-> ph (= A B))) (-> ph (= (exp A C) (exp B C)))) stmt (expeq2i () ( (= A B)) (= (exp C A) (exp C B))) stmt (expeq2d () ( (-> ph (= A B))) (-> ph (= (exp C A) (exp C B)))) ## Equivalence for exp stmt (expeq12 () () (-> (/\ (= A B) (= C D)) (/\ (= (exp A C) (exp B C)) (= (exp B C) (exp B D))))) stmt (expeq12d () ( (-> ph (= A B)) (-> ph (= C D))) (-> ph (/\ (= (exp A C) (exp B C)) (= (exp B C) (exp B D))))) ## Raise to the power of 1 ## right('Simplify', '1') stmt (exp1 () () (= (exp A (1)) A)) ## Squared means multiply twice ## left('Simplify', '2') right('Equivalence', '2') stmt (exp2 () () (= (exp A (2)) (* A A))) ## Cubed means multiply thrice ## left('Simplify', '∙') stmt (exp3 () () (= (exp A (3)) (* (* A A) A))) ## Square an Addition ## left('Simplify', '2') right('Equivalence', '+') stmt (sqadd () () (= (exp (+ A B) (2)) (+ (+ (exp A (2)) (* (* (2) A) B)) (exp B (2)))))