# List of theorems

List of theorems in peano_new/arithmetic/common/inequality.gh:

BiReplaceImp1Bi0 tvar (set S T U V) # <context> # This theorem is part of a series of proofs on the properties of the # inequalities including <a href="/wiki/peano/arithmetic/less-than">less than</a>, # <a href="/wiki/peano/arithmetic/less-than">less than or equal</a>, greater than, # and greater than or equal to. These theorems apply generally to both natural # numbers, integers, rational, and real numbers. They do not apply to complex numbers. # </context> # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
df-lt # <title> Definition of Less Than </title>
(<-> (< A B) (/\ (<= A B) (-. (= A B))))
ltle # <title> Inequality Conversion </title> # <suggest> right('Infer', '≤') </suggest>
(-> (< A B) (<= A B))
ltlei # <title> Inequality Conversion </title>
(< A B)(<= A B)
ltneq # <title> Operator Conversion </title> # <suggest> right('Infer', '≠') </suggest>
(-> (< A B) (-. (= A B)))
ltneqi # <title> Inequality Conversion </title>
(< A B)(-. (= A B))
(= A B) , (-. (= B C))(-. (= A C))
(-> ph (= A B))(-> ph (<-> (<= A C) (<= B C)))
(-> ph (= A B))(-> ph (<-> (<= C A) (<= C B)))
leeq12 # <title> Equivalence for ≤ </title>
(-> (/\ (= A B) (= C D)) (<-> (<= A C) (<= B D)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (<= A C) (<= B D)))
leeq1i # <title> Equivalence over Inequality </title> # <summary> Equality inference for less than or equal relation </summary> # <table> # (= A ] ] [ B ] ) # (<-> (<= A ] C ] ) (<= [ B ] C)) # </table>
(= A B)(<-> (<= A C) (<= B C))
leeq2i # <title> Equivalence over Inequality </title> # <summary> Equality inference for less than or equal relation </summary> # <table> # (= [ A ] [ [ B ] ) # (<-> (<= C [ A ] ) (<= [ C [ B ] )) # </table>
(= A B)(<-> (<= C A) (<= C B))
leeq1ii # <title> Equivalence over Inequality </title> # <summary> Equality inference for less than or equal relation </summary> # <table> # (<= A ] ] ] [ C) # (= A ] [ B ] ] ) # (<= [ [ B ] [ C) # </table>
(<= A C) , (= A B)(<= B C)
leeq2ii # <title> Equivalence over Inequality </title> # <summary> Equality inference for less than or equal relation </summary> # <table> # (<= C [ A ] ] ) # (= [ A ] [ B) # (<= C [ [ [ B) # </table>
(<= C A) , (= A B)(<= C B)
(rwff x (<= x A))
(rwff x (<= A x))
BiReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (<-> ps ch)(<-> ph (E. x ch))
BiReplaceBi1Ex1An1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (E. x (/\ ps [ [ [ th ] ))) # </table>
(<-> ph (E. x (/\ ps ch))) , (<-> ch th)(<-> ph (E. x (/\ ps th)))
EqReplaceBi1Ex1An1Eq0 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps (= [ A ] ] ] C)))) # (= [ A ] [ B ] ) # (<-> ph (E. x (/\ ps (= [ [ [ B ] C)))) # </table>
(<-> ph (E. x (/\ ps (= A C)))) , (= A B)(<-> ph (E. x (/\ ps (= B C))))
leadd1 # <title> Addition is Monotonic </title> # <summary> Addition is strictly monotonic in the first addend </summary> # <suggest> left('Cancel', '+') </suggest> # <table> # (<-> (<= A B) (<= (+ A <g> C) (+ B <g> C))) # </table>
(<-> (<= A B) (<= (+ A C) (+ B C)))
leadd2 # <title> Addition is Monotonic </title> # <summary> Addition is strictly monotonic in the second addend </summary> # <suggest> left('Cancel', '+') </suggest> # <table> # (<-> (<= A B) (<= (+ <g> C A) (+ <g> C B))) # </table>
(<-> (<= A B) (<= (+ C A) (+ C B)))
leadd1i # <title> Addition Over Inequality </title> # <table> # (<= A ] ] [ B ] ) # (<= (+ A ] C) ] (+ [ B ] C)) # </table>
(<= A B)(<= (+ A C) (+ B C))
leadd2i # <title> Addition Over Inequality </title> # <table> # (<= [ A ] [ B ) # (<= (+ C [ A ] ) (+ C [ B )) # </table>
(<= A B)(<= (+ C A) (+ C B))
leadd12 # <title> Inequality relation for two equal sums </title>
(-> (= (+ A B) (+ C D)) (<-> (<= A C) (<= D B)))
ltadd1 # <title> Addition is Monotonic </title> # <suggest> left('Cancel', '+') </suggest>
(<-> (< A B) (< (+ A C) (+ B C)))
ltadd2 # <title> Addition is Monotonic </title> # <suggest> left('Cancel', '+') </suggest>
(<-> (< A B) (< (+ C A) (+ C B)))
lteq1 # <title> Equivalence for < </title> ##
(-> (= A C) (<-> (< A B) (< C B)))
(= A C)(<-> (< A B) (< C B))
lteq2 # <title> Equivalence for < </title> ##
(-> (= B C) (<-> (< A B) (< A C)))
(-> ph (= A C))(-> ph (<-> (< A B) (< C B)))
(= B C)(<-> (< A B) (< A C))
(-> ph (= B C))(-> ph (<-> (< A B) (< A C)))
lteq2ii # <title> Equivalence over Inequality </title> # <table> # (< C [ A ] ] ) # (= [ A ] [ B) # (< C [ [ [ B) # </table>
(< C A) , (= A B)(< C B)
lteq1ii # <title> Equivalence over Inequality </title> # <summary> Equality deduction for less than relation </summary> # <table> # (< A ] ] ] [ C) # (= A ] [ B ] ] ) # (< [ [ B ] [ C) # </table>
(< A C) , (= A B)(< B C)
lteq12 # <title> Equivalence for < </title> ##
(-> (/\ (= A B) (= C D)) (<-> (< A C) (< B D)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (< A C) (< B D)))
EqReplaceLt1 # <title> Substitution </title> # <table> # (< A [ B ] ] ] ) # (= [ B ] [ C ] ) # (< A [ [ [ C ] ) # </table>
(< A B) , (= B C)(< A C)
EqReplaceLt0 # <title> Substitution </title> # <table> # (< [ A ] ] ] C) # (= [ A ] [ B ] ) # (< [ [ [ B ] C) # </table>
(< A C) , (= A B)(< B C)
EqReplaceImp1Imp1Lt1 # <title> Substitution </title> # <table> # (-> ph (-> ps (< A [ B ] ] ] ))) # (= [ B ] [ C ] ) # (-> ph (-> ps (< A [ [ [ C ] ))) # </table>
(-> ph (-> ps (< A B))) , (= B C)(-> ph (-> ps (< A C)))
EqReplaceImp1Lt1 # <title> Substitution </title> # <table> # (-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (< A [ [ [ C ] )) # </table>
(-> ph (< A B)) , (= B C)(-> ph (< A C))
df-ge # <title> Def. Greater Than or Equal to </title> # <suggest> right('Define', '≤') left('Simplify', '≥') </suggest>
(<-> (>= A B) (-. (< A B)))
df-gt # <title> Def. Greater Than </title> # <suggest> right('Define', '<') left('Simplify', '>') </suggest>
(<-> (> A B) (-. (<= A B)))
gteq1 # <title> Equivalence for > </title> ##
(-> (= A C) (<-> (> A B) (> C B)))
(= A C)(<-> (> A B) (> C B))
gteq2 # <title> Equivalence for > </title> ##
(-> (= B C) (<-> (> A B) (> A C)))
(-> ph (= A C))(-> ph (<-> (> A B) (> C B)))
(= B C)(<-> (> A B) (> A C))
gteq12 # <title> Equivalence for > </title> ##
(-> (/\ (= A B) (= C D)) (<-> (> A C) (> B D)))
(-> ph (= B C))(-> ph (<-> (> A B) (> A C)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (> A C) (> B D)))
geeq1 # <title> Equivalence for >= </title> ##
(-> (= A C) (<-> (>= A B) (>= C B)))
(= A C)(<-> (>= A B) (>= C B))
geeq2 # <title> Equivalence for >= </title> ##
(-> (= B C) (<-> (>= A B) (>= A C)))
(-> ph (= A C))(-> ph (<-> (>= A B) (>= C B)))
(= B C)(<-> (>= A B) (>= A C))
geeq12 # <title> Equivalence for >= </title> ##
(-> (/\ (= A B) (= C D)) (<-> (>= A C) (>= B D)))
(-> ph (= B C))(-> ph (<-> (>= A B) (>= A C)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (>= A C) (>= B D)))
notge # <title> Def. Greater Than or Equal </title> # <suggest> right('Simplify', '<') </suggest>
(<-> (-. (>= A B)) (< A B))
notgt # <title> Def. Greater Than </title> # <suggest> right('Simplify', ' ≤') </suggest>
(<-> (-. (> A B)) (<= A B))
gtadd1i # <title> Addition Over Inequality </title> # <table> # (> A ] [ B ] ) # (> (+ A ] C) (+ [ B ] C)) # </table>
(> A B)(> (+ A C) (+ B C))
gtadd2i # <title> Addition Over Inequality </title> # <table> # (> A ] [ B ] ) # (> (+ A ] C) (+ [ B ] C)) # </table>
(> A B)(> (+ C A) (+ C B))
geadd1i # <title> Addition Over Inequality </title> # <table> # (>= A ] [ B ] ) # (>= (+ A ] C) (+ [ B ] C)) # </table>
(>= A B)(>= (+ A C) (+ B C))
geadd2i # <title> Addition Over Inequality </title> # <table> # (>= [ A ] [ B ) # (>= (+ C [ A ] ) (+ C [ B )) # </table>
(>= A B)(>= (+ C A) (+ C B))
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
ImpReplaceEx1 # <title> Substitution </title> # <table> # (E. x [ ph ] ] ] ) # (-> [ ph ] [ ps ] ) # (E. x [ [ [ ps ] ) # </table>
(E. x ph) , (-> ph ps)(E. x ps)
ImpReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
ImpReplaceImp1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y [ ps ] ] ] ))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y [ [ [ ch ] ))) # </table>
(-> ph (E. x (E. y ps))) , (-> ps ch)(-> ph (E. x (E. y ch)))
ImpReplaceImp1Ex1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (/\ [ ps ] ] ] th)))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (/\ [ [ [ ch ] th)))) # </table>
(-> ph (E. x (E. y (/\ ps th)))) , (-> ps ch)(-> ph (E. x (E. y (/\ ch th))))
EqReplaceImp0Eq0 # <title> Substitution </title> # <table> # (-> (= [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (-> (= [ [ [ B ] C) ph) # </table>
(-> (= A C) ph) , (= A B)(-> (= B C) ph)
eqle # <title> Equality Conversion </title> # <suggest> right('Infer', '≤') </suggest>
(-> (= A B) (<= A B))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
BiReplaceBi1Or0 # <title> Substitution </title> # <table> # (<-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (\/ [ [ [ ch ] th)) # </table>
(<-> ph (\/ ps th)) , (<-> ps ch)(<-> ph (\/ ch th))
BiReplaceBi1Or1 # <title> Substitution </title> # <table> # (<-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (\/ ps [ [ [ th ] )) # </table>
(<-> ph (\/ ps ch)) , (<-> ch th)(<-> ph (\/ ps th))
gttot # <title> Total Relation for > </title>
(\/ (= A B) (\/ (> A B) (> B A)))
ltcon.1 # <title> Converse of < Lemma </title>
(-> (> A B) (< B A))
(-> (< A B) (> B A))
ltcon # <title> Converse of < </title> # <suggest> right('Commute', '<') left('Commute', '>') </suggest>
(<-> (< B A) (> A B))
BiReplaceBi1Not0An0 # <title> Substitution </title> # <table> # (<-> ph (-. (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (/\ [ [ [ ch ] th))) # </table>
(<-> ph (-. (/\ ps th))) , (<-> ps ch)(<-> ph (-. (/\ ch th)))
BiReplaceBi1Not0An1 # <title> Substitution </title> # <table> # (<-> ph (-. (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (/\ ps [ [ [ th ] ))) # </table>
(<-> ph (-. (/\ ps ch))) , (<-> ch th)(<-> ph (-. (/\ ps th)))
BiReplaceBi1Not0An1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. (/\ ps (-. [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (/\ ps (-. [ [ [ th ] )))) # </table>
(<-> ph (-. (/\ ps (-. ch)))) , (<-> ch th)(<-> ph (-. (/\ ps (-. th))))
lecon # <title> Converse of ≤ </title> # <suggest> right('Commute', '≤') left('Commute', '≥') </suggest>
(<-> (<= A B) (>= B A))
(<-> (<= A B) (-. (< B A)))
ltadd12 # <title> Inequality relation for two equal sums </title>
(-> (= (+ A B) (+ C D)) (<-> (< A C) (< D B)))
(rwff x (= x A))
(rwff x (= A x))
(rwff x (< x A))
(rwff x (< A x))
BiReplaceBi1An0 # <title> Substitution </title> # <table> # (<-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ [ [ [ ch ] th)) # </table>
(<-> ph (/\ ps th)) , (<-> ps ch)(<-> ph (/\ ch th))
notltge # <title> Impossible Inequality
(-. (/\ (< A B) (<= B A)))
notlegt # <title> Impossible Inequality
(-. (/\ (<= A B) (< B A)))
lelttr.1 # <title> Transitive Not Equal </title> # <suggest> right('Simplify', '<') </suggest>
(-> (/\ (<= A B) (< B C)) (-. (= A C)))
lelttr # <title> Transitive law </title> # <suggest> right('Simplify', '<') </suggest>
(-> (/\ (<= A B) (< B C)) (< A C))
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
ltletr.1 # <title> Transitive Not Equal </title> # <suggest> right('Simplify', '<') </suggest>
(-> (/\ (< A B) (<= B C)) (-. (= A C)))
ltletr # <title> Transitive law </title> # <suggest> right('Simplify', '<') </suggest>
(-> (/\ (< A B) (<= B C)) (< A C))
axlttri # <title> Inequality Conversion </title> # <suggest> left('Simplify', '<') </suggest>
(<-> (< A B) (-. (\/ (= A B) (< B A))))
leleo # <title> ≤ means < OR = </title> # <summary> Less than or equal to expressed in terms of less than or equals </summary> # <suggest> right('Equivalence', '∨') left('Simplify', '≤') </suggest>
(<-> (<= A B) (\/ (< A B) (= A B)))
ltconi # <title> Commute Inequality </title>
(< A B)(> B A)
leconi # <title> Commute Inequality </title>
(<= A B)(>= B A)
gegeo # <title> ≥ means > OR = </title> # <summary> Greater than or equal to expressed in terms of greater than or equals </summary> # <suggest> right('Equivalence', '∨') left('Simplify', '≥') </suggest>
(<-> (>= A B) (\/ (> A B) (= A B)))
(<-> (> B A) (> (+ B C) (+ A C)))
(<-> (> B A) (> (+ C B) (+ C A)))
(<-> (>= A B) (>= (+ A C) (+ B C)))
(<-> (>= A B) (>= (+ C A) (+ C B)))
BiReplaceBi1An1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps [ [ [ th ] )) # </table>
(<-> ph (/\ ps ch)) , (<-> ch th)(<-> ph (/\ ps th))
(< A B) , (< B C)(< A C)
replaceBi1An1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps [ [ [ th ] )) # </table>
(<-> ph (/\ ps ch)) , (<-> ch th)(<-> ph (/\ ps th))
BiReplaceBi1Or1Not0 # <title> Substitution </title> # <table> # (<-> ph (\/ ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (\/ ps (-. [ [ [ th ] ))) # </table>
(<-> ph (\/ ps (-. ch))) , (<-> ch th)(<-> ph (\/ ps (-. th)))
BiReplaceBi1Or1Ex1Not0 # <title> Substitution </title> # <table> # (<-> ph (\/ ps (E. x (-. [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (<-> ph (\/ ps (E. x (-. [ [ [ th ] )))) # </table>
(<-> ph (\/ ps (E. x (-. ch)))) , (<-> ch th)(<-> ph (\/ ps (E. x (-. th))))
BiReplaceBi1Or1Ex1 # <title> Substitution </title> # <table> # (<-> ph (\/ ps (E. x [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (\/ ps (E. x [ [ [ th ] ))) # </table>
(<-> ph (\/ ps (E. x ch))) , (<-> ch th)(<-> ph (\/ ps (E. x th)))
ImpReplaceImp1Imp1An1 # <title> Substitution </title> # <table> # (-> ph (-> ps (/\ ch [ th ] ] ] ))) # (-> [ th ] [ ta ] ) # (-> ph (-> ps (/\ ch [ [ [ ta ] ))) # </table>
(-> ph (-> ps (/\ ch th))) , (-> th ta)(-> ph (-> ps (/\ ch ta)))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
BiReplaceImp1Imp1Ex1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (E. x [ [ [ th ] ))) # </table>
(-> ph (-> ps (E. x ch))) , (<-> ch th)(-> ph (-> ps (E. x th)))
BiReplaceImp1Imp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (/\ ch [ th ] ] ] )))) # (<-> [ th ] [ ta ] ) # (-> ph (-> ps (E. x (/\ ch [ [ [ ta ] )))) # </table>
(-> ph (-> ps (E. x (/\ ch th)))) , (<-> th ta)(-> ph (-> ps (E. x (/\ ch ta))))
axlttri2 # <title> Inequality Conversion </title> # <suggest> left('Simplify', '<') </suggest>
(<-> (< A B) (/\ (-. (= A B)) (<= A B)))
axlttri2i # <title> Convert between inequalities </title>
(-. (= A B)) , (<= A B)(< A B)
eqge # <title> Equality Conversion </title> # <suggest> right('Infer', '≥') </suggest>
(-> (= A B) (>= A B))
eqnlt # <title> Equality Conversion </title> # <suggest> right('Infer', '¬<') </suggest>
(-> (= A B) (-. (< A B)))
gtnlt # <title> Inequality Conversion </title> # <suggest> right('Infer', '¬<') </suggest>
(-> (> A B) (-. (< A B)))
gtnle # <title> Inequality Conversion </title> # <suggest> right('Infer', '¬≤') </suggest>
(-> (> A B) (-. (<= A B)))
replaceBi1An0Not0 # <title> Substitution </title> # <table> # (<-> ph (/\ (-. [ ps ] ] ] ) th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ (-. [ [ [ ch ] ) th)) # </table>
(<-> ph (/\ (-. ps) th)) , (<-> ps ch)(<-> ph (/\ (-. ch) th))
BiReplaceBi0An0 # <title> Substitution </title> # <table> # (<-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (<-> (/\ [ [ [ ps ] ch) th) # </table>
(<-> (/\ ph ch) th) , (<-> ph ps)(<-> (/\ ps ch) th)
axgrtri # <title> Inequality Conversion </title> # <suggest> left('Simplify', '>') </suggest>
(<-> (> A B) (/\ (-. (= A B)) (>= A B)))
axgrtrii # <title> Inequality Conversion </title>
(-. (= A B)) , (>= A B)(> A B)
gtneq # <title> Inequality Conversion </title> # <suggest> right('Infer', '≠') </suggest>
(-> (> A B) (-. (= A B)))
ltngt # <title> Inequality Conversion </title> # <suggest> right('Infer', '¬>') </suggest>
(-> (< A B) (-. (> A B)))
ltnge # <title> Inequality Conversion </title> # <suggest> right('Infer', '¬≥') </suggest>
(-> (< A B) (-. (>= A B)))
eqngt # <title> Inequality Conversion </title> # <suggest> right('Infer', '¬>') </suggest>
(-> (= A B) (-. (> A B)))
gtge # <title> Inequality Conversion </title> # <suggest> right('Infer', '≥') </suggest>
(-> (> A B) (>= A B))
gtneqi # <title> Inequality Conversion </title>
(> A B)(-. (= A B))
gtgei # <title> Inequality Conversion </title>
(> A B)(>= A B)
ltadd1i # <title> Inequality Over Addition </title> # <table> # (< A ] [ B ] ) # (< (+ A ] C) (+ [ B ] C)) # </table>
(< A B)(< (+ A C) (+ B C))
ltadd2i # <title> Inequality Over Addition </title> # <table> # (< [ A ] [ B ) # (< (+ C [ A ] ) (+ C [ B )) # </table>
(< A B)(< (+ C A) (+ C B))
EqReplaceBi0Lt1 # <title> Substitution </title> # <table> # (<-> (< A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (< A [ [ [ C ] ) ph) # </table>
(<-> (< A B) ph) , (= B C)(<-> (< A C) ph)
EqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (<= [ [ [ B ] C)) # </table>
(<-> ph (<= A C)) , (= A B)(<-> ph (<= B C))
EqReplaceBi1Ex1Eq0 # <title> Substitution </title> # <table> # (<-> ph (E. x (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (<-> ph (E. x (= [ [ [ B ] C))) # </table>
(<-> ph (E. x (= A C))) , (= A B)(<-> ph (E. x (= B C)))
EqReplaceImp1Le0 # <title> Substitution </title> # <table> # (-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (<= [ [ [ B ] C)) # </table>
(-> ph (<= A C)) , (= A B)(-> ph (<= B C))
EqReplaceImp1Le1 # <title> Substitution </title> # <table> # (-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (<= A [ [ [ C ] )) # </table>
(-> ph (<= A B)) , (= B C)(-> ph (<= A C))
lemul2 # <title> Multiply Both Sides </title> # <summary> Multiplication is monotonic in its second argument </summary>
(-> (/\ (<= A B) (<= (0) C)) (<= (* C A) (* C B)))
EqReplaceImp1Bi1Eq0 # <title> Substitution </title> # <table> # (-> ph (<-> ps (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (<-> ps (= [ [ [ B ] C))) # </table>
(-> ph (<-> ps (= A C))) , (= A B)(-> ph (<-> ps (= B C)))
exeq # <title> Equality Equivalent to Adding Zero </title>
(<-> (= A B) (E. x (/\ (= x (0)) (= (+ A x) B))))
BiReplaceBi1An0Not0 # <title> Substitution </title> # <table> # (<-> ph (/\ (-. [ ps ] ] ] ) th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ (-. [ [ [ ch ] ) th)) # </table>
(<-> ph (/\ (-. ps) th)) , (<-> ps ch)(<-> ph (/\ (-. ch) th))
BiReplaceBi1Al1 # <title> Substitution </title> # <table> # (<-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x [ [ [ ch ] )) # </table>
(<-> ph (A. x ps)) , (<-> ps ch)(<-> ph (A. x ch))
BiReplaceBi1Al1Not0 # <title> Substitution </title> # <table> # (<-> ph (A. x (-. [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (<-> ph (A. x (-. [ [ [ ch ] ))) # </table>
(<-> ph (A. x (-. ps))) , (<-> ps ch)(<-> ph (A. x (-. ch)))
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (<-> ps ch)(-> ph (E. x ch))
BiReplaceImp1Ex1Or1 # <title> Substitution </title> # <table> # (-> ph (E. x (\/ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (E. x (\/ ps [ [ [ th ] ))) # </table>
(-> ph (E. x (\/ ps ch))) , (<-> ch th)(-> ph (E. x (\/ ps th)))
BiReplaceBi1An0An0 # <title> Substitution </title> # <table> # (<-> ph (/\ (/\ [ ps ] ] ] th) ta)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ (/\ [ [ [ ch ] th) ta)) # </table>
(<-> ph (/\ (/\ ps th) ta)) , (<-> ps ch)(<-> ph (/\ (/\ ch th) ta))
BiReplaceBi1An0An0Not0 # <title> Substitution </title> # <table> # (<-> ph (/\ (/\ (-. [ ps ] ] ] ) th) ta)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ (/\ (-. [ [ [ ch ] ) th) ta)) # </table>
(<-> ph (/\ (/\ (-. ps) th) ta)) , (<-> ps ch)(<-> ph (/\ (/\ (-. ch) th) ta))
exlt # <title> Less Than or Equal from Positive Difference </title>
(-> (< A B) (E. x (/\ (< (0) x) (= (+ A x) B))))
EqReplaceImp1Imp1Lt0 # <title> Substitution </title> # <table> # (-> ph (-> ps (< [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (-> ps (< [ [ [ B ] C))) # </table>
(-> ph (-> ps (< A C))) , (= A B)(-> ph (-> ps (< B C)))
BiReplaceImp1Imp0 # <title> Substitution </title> # <table> # (-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (-> [ [ [ ch ] th)) # </table>
(-> ph (-> ps th)) , (<-> ps ch)(-> ph (-> ch th))
BiReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
EqReplaceImp1Imp1Not0Le0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. (<= [ A ] ] ] C)))) # (= [ A ] [ B ] ) # (-> ph (-> ps (-. (<= [ [ [ B ] C)))) # </table>
(-> ph (-> ps (-. (<= A C)))) , (= A B)(-> ph (-> ps (-. (<= B C))))
EqReplaceImp1Imp1Not0Le1 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. (<= A [ B ] ] ] )))) # (= [ B ] [ C ] ) # (-> ph (-> ps (-. (<= A [ [ [ C ] )))) # </table>
(-> ph (-> ps (-. (<= A B)))) , (= B C)(-> ph (-> ps (-. (<= A C))))
EqReplaceImp1Imp1Gt0 # <title> Substitution </title> # <table> # (-> ph (-> ps (> [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (-> ps (> [ [ [ B ] C))) # </table>
(-> ph (-> ps (> A C))) , (= A B)(-> ph (-> ps (> B C)))
EqReplaceImp1Imp1Gt1 # <title> Substitution </title> # <table> # (-> ph (-> ps (> A [ B ] ] ] ))) # (= [ B ] [ C ] ) # (-> ph (-> ps (> A [ [ [ C ] ))) # </table>
(-> ph (-> ps (> A B))) , (= B C)(-> ph (-> ps (> A C)))
EqReplaceImp1Gt0 # <title> Substitution </title> # <table> # (-> ph (> [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (> [ [ [ B ] C)) # </table>
(-> ph (> A C)) , (= A B)(-> ph (> B C))
EqReplaceImp1Gt1 # <title> Substitution </title> # <table> # (-> ph (> A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (> A [ [ [ C ] )) # </table>
(-> ph (> A B)) , (= B C)(-> ph (> A C))
BiReplaceImp0An0Not0 # <title> Substitution </title> # <table> # (-> (/\ (-. [ ph ] ] ] ) ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ (-. [ [ [ ps ] ) ch) th) # </table>
(-> (/\ (-. ph) ch) th) , (<-> ph ps)(-> (/\ (-. ps) ch) th)
BiReplaceImp0An1Not0 # <title> Substitution </title> # <table> # (-> (/\ ph (-. [ ps ] ] ] )) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph (-. [ [ [ ch ] )) th) # </table>
(-> (/\ ph (-. ps)) th) , (<-> ps ch)(-> (/\ ph (-. ch)) th)
BiReplaceOr1Or0 # <title> Substitution </title> # <table> # (\/ ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (\/ ph (\/ [ [ [ ch ] th)) # </table>
(\/ ph (\/ ps th)) , (<-> ps ch)(\/ ph (\/ ch th))
BiReplaceOr1Or1 # <title> Substitution </title> # <table> # (\/ ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (\/ ph (\/ ps [ [ [ th ] )) # </table>
(\/ ph (\/ ps ch)) , (<-> ch th)(\/ ph (\/ ps th))
inequalities # <title> A number is less, equal, or greater </title>
(\/ (< A B) (\/ (= A B) (> A B)))
neqLtGt # <title> A nonequal number is smaller or larger </title> # <suggest> left('Simplify', '≠') </suggest>
(<-> (-. (= A B)) (\/ (< A B) (> A B)))
neqLtGt2 # <title> A nonequal number is smaller or larger </title> # <suggest> left('Simplify', '≠') </suggest>
(<-> (-. (= A B)) (\/ (< A B) (< B A)))
(-> (-. (= A B)) (\/ (< A B) (> A B)))
BiReplaceImp1Imp1Not0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (-. [ [ [ th ] ))) # </table>
(-> ph (-> ps (-. ch))) , (<-> ch th)(-> ph (-> ps (-. th)))
(-> (/\ (< (0) A) (< (0) B)) (< (0) (* A B)))
(-> (/\ (> A (0)) (> B (0))) (> (* A B) (0)))
BiReplaceBi1An0Or0 # <title> Substitution </title> # <table> # (<-> ph (/\ (\/ [ ps ] ] ] th) ta)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ (\/ [ [ [ ch ] th) ta)) # </table>
(<-> ph (/\ (\/ ps th) ta)) , (<-> ps ch)(<-> ph (/\ (\/ ch th) ta))
BiReplaceBi1An0Or1 # <title> Substitution </title> # <table> # (<-> ph (/\ (\/ ps [ ch ] ] ] ) ta)) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ (\/ ps [ [ [ th ] ) ta)) # </table>
(<-> ph (/\ (\/ ps ch) ta)) , (<-> ch th)(<-> ph (/\ (\/ ps th) ta))
BiReplaceBi1Or1Or1 # <title> Substitution </title> # <table> # (<-> ph (\/ ps (\/ ch [ th ] ] ] ))) # (<-> [ th ] [ ta ] ) # (<-> ph (\/ ps (\/ ch [ [ [ ta ] ))) # </table>
(<-> ph (\/ ps (\/ ch th))) , (<-> th ta)(<-> ph (\/ ps (\/ ch ta)))
ImpReplaceBi1Or1Or0An1 # <title> Substitution </title> # <table> # (<-> ph (\/ ps (\/ (/\ ch [ th ] ] ] ) et))) # (-> [ th ] [ ta ] ) # (<-> ph (\/ ps (\/ (/\ ch [ [ [ ta ] ) et))) # </table>
(<-> ph (\/ ps (\/ (/\ ch th) et))) , (-> th ta)(-> ph (\/ ps (\/ (/\ ch ta) et)))
BiReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (<-> ps ch)(-> ph (\/ ch th))
ImpReplaceImp1Or0Or1An0 # <title> Substitution </title> # <table> # (-> ph (\/ (\/ ps (/\ [ ch ] ] ] ta)) et)) # (-> [ ch ] [ th ] ) # (-> ph (\/ (\/ ps (/\ [ [ [ th ] ta)) et)) # </table>
(-> ph (\/ (\/ ps (/\ ch ta)) et)) , (-> ch th)(-> ph (\/ (\/ ps (/\ th ta)) et))
BiReplaceImp1Or0Or1 # <title> Substitution </title> # <table> # (-> ph (\/ (\/ ps [ ch ] ] ] ) ta)) # (<-> [ ch ] [ th ] ) # (-> ph (\/ (\/ ps [ [ [ th ] ) ta)) # </table>
(-> ph (\/ (\/ ps ch) ta)) , (<-> ch th)(-> ph (\/ (\/ ps th) ta))
ImpReplaceImp1Or0An1 # <title> Substitution </title> # <table> # (-> ph (\/ (/\ ps [ ch ] ] ] ) ta)) # (-> [ ch ] [ th ] ) # (-> ph (\/ (/\ ps [ [ [ th ] ) ta)) # </table>
(-> ph (\/ (/\ ps ch) ta)) , (-> ch th)(-> ph (\/ (/\ ps th) ta))
BiReplaceBi0Imp1 # <title> Substitution </title> # <table> # (<-> (-> ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (<-> (-> ph [ [ [ ch ] ) th) # </table>
(<-> (-> ph ps) th) , (<-> ps ch)(<-> (-> ph ch) th)
BiReplaceBi0Imp1Or0 # <title> Substitution </title> # <table> # (<-> (-> ph (\/ [ ps ] ] ] th)) ta) # (<-> [ ps ] [ ch ] ) # (<-> (-> ph (\/ [ [ [ ch ] th)) ta) # </table>
(<-> (-> ph (\/ ps th)) ta) , (<-> ps ch)(<-> (-> ph (\/ ch th)) ta)
BiReplaceBi0Imp1Or0An1 # <title> Substitution </title> # <table> # (<-> (-> ph (\/ (/\ ps [ ch ] ] ] ) ta)) et) # (<-> [ ch ] [ th ] ) # (<-> (-> ph (\/ (/\ ps [ [ [ th ] ) ta)) et) # </table>
(<-> (-> ph (\/ (/\ ps ch) ta)) et) , (<-> ch th)(<-> (-> ph (\/ (/\ ps th) ta)) et)
BiReplaceImp1An0Not0 # <title> Substitution </title> # <table> # (-> ph (/\ (-. [ ps ] ] ] ) th)) # (<-> [ ps ] [ ch ] ) # (-> ph (/\ (-. [ [ [ ch ] ) th)) # </table>
(-> ph (/\ (-. ps) th)) , (<-> ps ch)(-> ph (/\ (-. ch) th))
BiReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (<-> ps ch)(-> ph (/\ ch th))
BiReplaceNot0An1 # <title> Substitution </title> # <table> # (-. (/\ ph [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-. (/\ ph [ [ [ ch ] )) # </table>
(-. (/\ ph ps)) , (<-> ps ch)(-. (/\ ph ch))
BiReplaceNot0Not0 # <title> Substitution </title> # <table> # (-. (-. [ ph ] ] ] )) # (<-> [ ph ] [ ps ] ) # (-. (-. [ [ [ ps ] )) # </table>
(-. (-. ph)) , (<-> ph ps)(-. (-. ps))
ImpReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
nalexi number 2.5
(-. (A. x (-. ph)))(E. x ph)
impexpi2 # <title> Import-Export Theorem </title> # <table> # (-> (/\ ph [ ps ] ) [ ch) # (-> ph (-> [ ps ] [ ch)) # </table>
(-> (/\ ph ps) ch)(-> ph (-> ps ch))
lttr number 11.0 # <title> Transitive Property </title> # <suggest> right('Simplify', '< <') </suggest>
(-> (/\ (< A B) (< B C)) (< A C))
letradd # <title> Combine Inequalities </title> # <table> # (-> (/\ (<= <c> A <b> B) (<= <m> C <r> D)) (<= (+ <c> A <m> C) (+ <b> B <r> D))) # </table>
(-> (/\ (<= A B) (<= C D)) (<= (+ A C) (+ B D)))
lttradd # <title> Combine Inequalities </title>
(-> (/\ (< A B) (< C D)) (< (+ A C) (+ B D)))
lelttradd # <title> Combine Inequalities </title>
(-> (/\ (<= A B) (< C D)) (< (+ A C) (+ B D)))
(-> (/\ (>= A B) (>= C D)) (>= (+ A C) (+ B D)))
(-> (/\ (> A B) (> C D)) (> (+ A C) (+ B D)))
(-> (/\ (>= B A) (> D C)) (> (+ B D) (+ A C)))
letraddi # <table> # (<= A ] ] [ B ] ) # (<= [ C ] [ [ D) # (<= (+ A ] C ] ) (+ [ B [ D)) # </table>
(<= A B) , (<= C D)(<= (+ A C) (+ B D))
lttraddi # <table> # (< A ] ] [ B ] ) # (< [ C ] [ [ D) # (< (+ A ] C ] ) (+ [ B [ D)) # </table>
(< A B) , (< C D)(< (+ A C) (+ B D))
getraddi # <table> # (>= A ] ] [ B ] ) # (>= [ C ] [ [ D) # (>= (+ A ] C ] ) (+ [ B [ D)) # </table>
(>= A B) , (>= C D)(>= (+ A C) (+ B D))
gttraddi # <table> # (> A ] ] [ B ] ) # (> [ C ] [ [ D) # (> (+ A ] C ] ) (+ [ B [ D)) # </table>
(> A B) , (> C D)(> (+ A C) (+ B D))
(= A (+ B (+ C D)))(= A (+ (+ B C) D))
ltTrlti thm (ltmul () () ( -> (/\ (< A B) (< C D)) (< (* A C) (* B D))) A B nnltp1let C D nnltp1let anbi12i (+ A (1)) B (+ C (1)) D lemul3 sylbi (* A C) (+ (* (1) C) (* A (1))) addge01t (* A C) (* (1) C) (* A (1)) addass (* A C) leeq2i mpbir (* A C) (+ (+ (* A C) (* (1) C)) (* A (1))) (1) leadd1 mpbi A (1) C (1) distrl addassrli (1) mulid (+ (+ (* A C) (* (1) C)) (* A (1))) addeq2i eqtri (+ (* A C) (1)) leeq2i mpbir jctil (+ (* A C) (1)) (* (+ A (1)) (+ C (1))) (* B D) letr syl (* A C) (* B D) nnltp1let sylibr) thm (gtmul () () (-> (/\ (> A B) (> C D)) (> (* A C) (* B D))) B A D C ltmul ## <d 'Converse of < '> B A ltcon BiReplaceImp0An0 ## </d 'Converse of < '> ## <d 'Converse of < '> D C ltcon BiReplaceImp0An1 ## </d 'Converse of < '> ## <d 'Converse of < '> (* B D) (* A C) ltcon sylib ## </d 'Converse of < '> ) # <title> Transitive Inequality </title>
(< A B)(-> (< B C) (< A C))
leTreti # <title> Transitive Inequality </title>
(<= A B)(-> (<= B C) (<= A C))
getr # <title> Transitive Inequality </title> # <suggest> right('Transitive', '≥') </suggest>
(-> (/\ (>= A B) (>= B C)) (>= A C))
gttr # <title> Transitive Inequality </title> # <suggest> right('Transitive', '>') </suggest>
(-> (/\ (> A B) (> B C)) (> A C))
gtgetr # <title> Transitive Inequality </title> # <suggest> right('Transitive', '>') </suggest>
(-> (/\ (> C B) (>= B A)) (> C A))
gegttr # <title> Transitive Inequality </title> # <suggest> right('Transitive', '>') </suggest>
(-> (/\ (>= C B) (> B A)) (> C A))
ltTrlt # <title> Transitive Inequality </title> # <table> # (< [ B ] [ [ C ] ) # (-> (< A [ B ] ) (< [ A [ C ] )) # </table>
(< B C)(-> (< A B) (< A C))
ltTrle # <title> Transitive Inequality </title> # <table> # (< [ B ] [ [ C ] ) # (-> (<= A [ B ] ) (< [ A [ C ] )) # </table>
(< B C)(-> (<= A B) (< A C))
ltTreq # <title> Transitive Inequality </title> # <table> # (< [ B ] [ [ C ] ) # (-> (= A [ B ] ) (< [ A [ C ] )) # </table>
(< B C)(-> (= A B) (< A C))
leTreq # <title> Transitive Inequality </title> # <table> # (<= [ B ] [ [ C ] ) # (-> (= A [ B ] ) (<= [ A [ C ] )) # </table>
(<= B C)(-> (= A B) (<= A C))
leTrlt # <title> Transitive Inequality </title> # <table> # (<= [ B ] [ [ C ] ) # (-> (= A [ B ] ) (<= [ A [ C ] )) # </table>
(<= B C)(-> (< A B) (< A C))
leTrle # <title> Transitive Inequality </title> # <table> # (<= [ B ] [ [ C ] ) # (-> (<= A [ B ] ) (<= [ A [ C ] )) # </table>
(<= B C)(-> (<= A B) (<= A C))
gtTrgt # <title> Transitive Inequality </title> # <table> # (-. (> [ B ] [ [ C ] )) # (-> (> A [ B ] ) (> [ A [ C ] )) # </table>
(> B C)(-> (> A B) (> A C))
geTrgt # <title> Transitive Inequality </title> # <table> # (>= [ B ] [ [ C ] ) # (-> (> A [ B ] ) (> [ A [ C ] )) # </table>
(>= B C)(-> (> A B) (> A C))
geTreq # <title> Transitive Inequality </title> # <table> # (>= [ B ] [ [ C ] ) # (-> (= A [ B ] ) (>= [ A [ C ] )) # </table>
(>= B C)(-> (= A B) (>= A C))
gtTreq # <title> Transitive Inequality </title> # <table> # (> [ B ] [ [ C ] ) # (-> (= A [ B ] ) (> [ A [ C ] )) # </table>
(> B C)(-> (= A B) (> A C))
gtTrge # <title> Transitive Inequality </title> # <table> # (> [ B ] [ [ C ] ) # (-> (>= A [ B ] )) (> [ A [ C ] )) # </table>
(> B C)(-> (>= C A) (> B A))
geTrge # <title> Transitive Inequality </title> # <table> # (>= [ B ] [ [ C ] ) # (-> (>= A [ B ] ) (>= [ A [ C ] )) # </table>
(>= B C)(-> (>= A B) (>= A C))
ImpReplaceBi0 # <title> Substitution </title> # <table> # (<-> [ ph ] ] ] ch) # (-> [ ph ] [ ps ] ) # (<-> [ [ [ ps ] ch) # </table>
(<-> ph ch) , (-> ph ps)(-> ch ps)
ImpReplaceBi0Ex1 # <title> Substitution </title>
(<-> (E. x ph) ch) , (-> ph ps)(-> ch (E. x ps))
ImpReplaceBi0Ex1An0 # <title> Substitution </title>
(<-> (E. x (/\ ph ch)) th) , (-> ph ps)(-> th (E. x (/\ ps ch)))
GtReplaceBi0Ex1An0Eq1 # <title> Substitution </title>
(<-> (E. x (/\ (= A B) ph)) ps) , (> B C)(-> ps (E. x (/\ (> A C) ph)))
1notEqual0 # <title> One-Digit Inequality </title>
(-. (= (1) (0)))
0less1 # <title> One-Digit Inequality </title>
(< (0) (1))
1greater0 # <title> 1 is more than 0 </title>
(> (1) (0))
BiReplaceBi1Ex1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x (E. y [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x (E. y [ [ [ ch ] ))) # </table>
(<-> ph (E. x (E. y ps))) , (<-> ps ch)(<-> ph (E. x (E. y ch)))
BiReplaceBi1Ex1Ex1An1 # <title> Substitution </title> # <table> # (<-> ph (E. x (E. y (/\ ps [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (<-> ph (E. x (E. y (/\ ps [ [ [ th ] )))) # </table>
(<-> ph (E. x (E. y (/\ ps ch)))) , (<-> ch th)(<-> ph (E. x (E. y (/\ ps th))))
BiReplaceBi1Ex1Ex1An0 # <title> Substitution </title> # <table> # (<-> ph (E. x (E. y (/\ [ ps ] ] ] th)))) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x (E. y (/\ [ [ [ ch ] th)))) # </table>
(<-> ph (E. x (E. y (/\ ps th)))) , (<-> ps ch)(<-> ph (E. x (E. y (/\ ch th))))
ImpReplaceBi1Ex1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x (E. y [ ps ] ] ] ))) # (-> [ ps ] [ ch ] ) # (<-> ph (E. x (E. y [ [ [ ch ] ))) # </table>
(<-> ph (E. x (E. y ps))) , (-> ps ch)(-> ph (E. x (E. y ch)))
EqReplaceBi1Ge1 # <title> Substitution </title> # <table> # (<-> ph (>= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (>= A [ [ [ C ] )) # </table>
(<-> ph (>= A B)) , (= B C)(<-> ph (>= A C))
EqReplaceImp1Ex1Eq0 # <title> Substitution </title> # <table> # (-> ph (E. x (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (-> ph (E. x (= [ [ [ B ] C))) # </table>
(-> ph (E. x (= A C))) , (= A B)(-> ph (E. x (= B C)))
EqReplaceBi1Lt0 # <title> Substitution </title> # <table> # (<-> ph (< [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (< [ [ [ B ] C)) # </table>
(<-> ph (< A C)) , (= A B)(<-> ph (< B C))
df-pos # <title> Definition of a Positive Number </title> # <suggest> left('Simplify', '+') </suggest>
(<-> (pos A) (> A (0)))
(-> (= A B) (<-> (pos A) (pos B)))
(= A B)(<-> (pos A) (pos B))
(-> ph (= A B))(-> ph (<-> (pos A) (pos B)))
df-zneg # <title> Definition of a Negative Integer </title> # <suggest> left('Simplify', '-') </suggest>
(<-> (zneg A) (< A (0)))
(-> (= A B) (<-> (zneg A) (zneg B)))
(= A B)(<-> (zneg A) (zneg B))
(-> ph (= A B))(-> ph (<-> (zneg A) (zneg B)))
gtNotSym # <title> Greater Than is Not Symmetric </title>
(-. (> A A))
ltNotSym # <title> Less Than is Not Symmetric </title>
(-. (< A A))
0NotPos # <title> 0 is not positive </title>
(-. (pos (0)))
0NotNeg # <title> 0 is not negative </title>
(-. (zneg (0)))
0NotPosd # <title> 0 is not positive </title>
(-> (= A (0)) (-. (pos A)))
0NotNegd # <title> 0 is not positive </title>
(-> (= A (0)) (-. (zneg A)))
posproduct1 # <title> Multiply Two Positive Numbers </title>
(-> (/\ (pos A) (pos B)) (pos (* A B)))
EqReplaceBi1Le1 # <title> Substitution </title> # <table> # (<-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (<= A [ [ [ C ] )) # </table>
(<-> ph (<= A B)) , (= B C)(<-> ph (<= A C))
LeReplaceLe1 # <title> Substitution </title> # <table> # (<= A [ B ] ] ] ) # (<= [ B ] [ C ] ) # (<= A [ [ [ C ] ) # </table>
(<= A B) , (<= B C)(<= A C)
LeReplaceLt1 # <title> Substitution </title> # <table> # (< A [ B ] ] ] ) # (<= [ B ] [ C ] ) # (< A [ [ [ C ] ) # </table>
(< A B) , (<= B C)(< A C)
(> (+ (1) (1)) (1))
1pos # <title> 1 is positive </title>
(pos (1))
BiReplaceImp1Ex1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y [ [ [ ch ] ))) # </table>
(-> ph (E. x (E. y ps))) , (<-> ps ch)(-> ph (E. x (E. y ch)))
BiReplaceImp1Ex1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (/\ [ ps ] ] ] th)))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (/\ [ [ [ ch ] th)))) # </table>
(-> ph (E. x (E. y (/\ ps th)))) , (<-> ps ch)(-> ph (E. x (E. y (/\ ch th))))
ImpReplaceImp1Ex1Ex1An0An1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (/\ (/\ ps [ ch ] ] ] ) ta)))) # (-> [ ch ] [ th ] ) # (-> ph (E. x (E. y (/\ (/\ ps [ [ [ th ] ) ta)))) # </table>
(-> ph (E. x (E. y (/\ (/\ ps ch) ta)))) , (-> ch th)(-> ph (E. x (E. y (/\ (/\ ps th) ta))))
EqReplaceBi1Le0Add0 # <title> Substitution </title> # <table> # (<-> ph (<= (+ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (<-> ph (<= (+ [ [ [ B ] C) D)) # </table>
(<-> ph (<= (+ A C) D)) , (= A B)(<-> ph (<= (+ B C) D))
EqReplaceBi1Le1Add1 # <title> Substitution </title> # <table> # (<-> ph (<= A (+ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (<-> ph (<= A (+ B [ [ [ D ] ))) # </table>
(<-> ph (<= A (+ B C))) , (= C D)(<-> ph (<= A (+ B D)))
ImpReplaceImp1Ex1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (/\ ps [ ch ] ] ] )))) # (-> [ ch ] [ th ] ) # (-> ph (E. x (E. y (/\ ps [ [ [ th ] )))) # </table>
(-> ph (E. x (E. y (/\ ps ch)))) , (-> ch th)(-> ph (E. x (E. y (/\ ps th))))
BiReplaceImp1Ex1Ex1An0An0 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (/\ (/\ [ ps ] ] ] th) ta)))) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x (E. y (/\ (/\ [ [ [ ch ] th) ta)))) # </table>
(-> ph (E. x (E. y (/\ (/\ ps th) ta)))) , (<-> ps ch)(-> ph (E. x (E. y (/\ (/\ ch th) ta))))
BiReplaceImp1Ex1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (E. x (E. y (/\ ps [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (-> ph (E. x (E. y (/\ ps [ [ [ th ] )))) # </table>
(-> ph (E. x (E. y (/\ ps ch)))) , (<-> ch th)(-> ph (E. x (E. y (/\ ps th))))
(-> (/\ (<= A B) (<= C D)) (<= (+ (* A D) (* B C)) (+ (* A C) (* B D))))
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
ltmul1 # <title> Multiply Nonequal Numbers </title>
(-> (/\ (< A B) (< (0) C)) (< (* A C) (* B C)))
ltmul2i # <title> Multiplication is Monotonic </title> # <table> # (< B ] ] ] [ C ] ] ) # (< [ [ (0) ] [ [ [ A ) # (< (* B ] [ A ] ) (* [ C ] [ A )) # </table>
(< B C) , (< (0) A)(< (* B A) (* C A))
EqReplaceGt0 # <title> Substitution </title> # <table> # (> [ A ] ] ] C) # (= [ A ] [ B ] ) # (> [ [ [ B ] C) # </table>
(> A C) , (= A B)(> B C)
EqReplaceBi1Lt1 # <title> Substitution </title> # <table> # (<-> ph (< A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (< A [ [ [ C ] )) # </table>
(<-> ph (< A B)) , (= B C)(<-> ph (< A C))
(-> (/\ (> A B) (> C (0))) (> (* C A) (* C B)))
gtmul2i # <title> Multiplication is Monotonic </title> # <table> # (> B ] ] ] [ C ] ] ) # (> [ [ A ] [ [ [ (0) ) # (> (+ B ] [ A ] ) (+ [ C ] [ A )) # </table>
(> B C) , (> A (0))(> (* B A) (* C A))
EqReplaceBi1Lt0Add0 # <title> Substitution </title> # <table> # (<-> ph (< (+ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (<-> ph (< (+ [ [ [ B ] C) D)) # </table>
(<-> ph (< (+ A C) D)) , (= A B)(<-> ph (< (+ B C) D))
EqReplaceBi1Lt1Add1 # <title> Substitution </title> # <table> # (<-> ph (< A (+ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (<-> ph (< A (+ B [ [ [ D ] ))) # </table>
(<-> ph (< A (+ B C))) , (= C D)(<-> ph (< A (+ B D)))
(-> (/\ (< A B) (< C D)) (< (+ (* A D) (* B C)) (+ (* A C) (* B D))))
(-> (/\ (>= B A) (>= C (0))) (>= (* B C) (* A C)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)