## redirect inequality.gh # This file contains theorems related to natural number aristmtetic. 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) "") param (ADD_MULTIPLY_MIN add_multiply_min.ghi (PROP PREDICATE_EQ) "") param (INEQUALITY_MIN inequality_min.ghi (PROP PREDICATE_EQ ADD_MULTIPLY_MIN) "") 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)) ## 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)))) stmt (geeq1d () ( (-> ph (= A C))) (-> ph (<-> (>= A B) (>= C B)))) stmt (geeq2d () ( (-> ph (= B C))) (-> ph (<-> (>= 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 (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)))) stmt (0less1 () () (< (0) (1))) ## 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)))) ## Less Than or Equal from Positive Difference stmt (exlt ((A x)(B x)) () (-> (< A B) (E. x (/\ (< (0) x) (= (+ A x) B))))) stmt (gemul1 () () (-> (/\ (>= B A) (>= C (0))) (>= (* B C) (* A C))))