# List of theorems

List of theorems in peano_new/arithmetic/integers/inequality_min.gh:

df-le # <context> # This theorem is part of a series of theorems constructing the integers. # <a href="/wiki/peano/arithmetic/integers">An integer is constructed</a> as a # pair of natural numbers which represents the positive and the negative part # of the integer. This requires us to construct a new version of the less than # or equal to relation for integers involving pairs of natural numbers. These theorems # demonstrate that the integers has all the essential properties of a totally # ordered set. # </context> # <title> Def. Integer Less Than or Equal To' </title>
(<-> (<= A B) (n.<= (n.+ (head A) (tail B)) (n.+ (head B) (tail A))))
NeqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (n.<= [ A ] ] ] C)) # (n.= [ A ] [ B ] ) # (<-> ph (n.<= [ [ [ B ] C)) # </table>
(<-> ph (n.<= a c)) , (n.= a b)(<-> ph (n.<= b c))
NeqReplaceBi1Le1 # <title> Substitution </title> # <table> # (<-> ph (n.<= a [ B ] ] ] )) # (n.= [ B ] [ C ] ) # (<-> ph (n.<= a [ [ [ C ] )) # </table>
(<-> ph (n.<= a b)) , (n.= b c)(<-> ph (n.<= a c))
leop # <title> Apply ≤ to ordered pair </title>
(<-> (<= (<,> a b) (<,> c d)) (n.<= (n.+ a d) (n.+ c b)))
BiReplaceImp1Bi0 # <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))
NeqReplaceImp1Neq0 # <title> Substitution </title> # <table> # (-> ph (n.= [ A ] ] ] C)) # (n.= [ A ] [ B ] ) # (-> ph (n.= [ [ [ B ] C)) # </table>
(-> ph (n.= a c)) , (n.= a b)(-> ph (n.= b c))
NeqReplaceImp1Neq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (n.= a b)) , (n.= b c)(-> ph (n.= a c))
(-> (= A B) (<-> (<= A C) (<= B C)))
(-> (= A B) (<-> (<= C A) (<= C B)))
(= A B)(<-> (<= A C) (<= B C))
(-> ph (= A B))(-> ph (<-> (<= A C) (<= B C)))
(= A B)(<-> (<= C A) (<= C B))
(-> ph (= A B))(-> ph (<-> (<= C A) (<= C B)))
leeq12 # <title> Nequivalence for >z </title> ##
(-> (/\ (= A B) (= C D)) (<-> (<= A C) (<= B D)))
lehomomorph # <title> Integer Inequality Homomorphism </title> # <summary> The <a href="df-int">int embedding</a> is a homomorphism respecting <a href="df-le">less than or equal to</a>. </summary>
(<-> (<= (int a) (int b)) (n.<= a b))
(<= A A)
EqReplaceBi0Le0 # <title> Substitution </title> # <table> # (<-> (<= [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (<-> (<= [ [ [ B ] C) ph) # </table>
(<-> (<= A C) ph) , (= A B)(<-> (<= B C) ph)
EqReplaceBi0Le1 # <title> Substitution </title> # <table> # (<-> (<= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (<= A [ [ [ C ] ) ph) # </table>
(<-> (<= A B) ph) , (= B C)(<-> (<= A C) ph)
leadd1 # <title> Addition on Both Sides of Inequality </title> # <suggest> left('Cancel', '+') </suggest>
(<-> (<= (+ A C) (+ B C)) (<= A B))
NeqReplaceNot0Neq1 # <title> Substitution </title> # <table> # (-. (n.= a [ B ] ] ] )) # (n.= [ B ] [ C ] ) # (-. (n.= a [ [ [ C ] )) # </table>
(-. (n.= a b)) , (n.= b c)(-. (n.= a c))
NeqReplaceImp1Nle0 # <title> Substitution </title> # <table> # (-> ph (n.<= [ A ] ] ] C)) # (n.= [ A ] [ B ] ) # (-> ph (n.<= [ [ [ B ] C)) # </table>
(-> ph (n.<= a c)) , (n.= a b)(-> ph (n.<= b c))
NeqReplaceImp1Nle1 # <title> Substitution </title> # <table> # (-> ph (n.<= a [ B ] ] ] )) # (n.= [ B ] [ C ] ) # (-> ph (n.<= a [ [ [ C ] )) # </table>
(-> ph (n.<= a b)) , (n.= b c)(-> ph (n.<= a c))
letr # <title> Transitive Property </title>
(-> (/\ (<= A B) (<= B C)) (<= A C))
lesym # <title> Same upper and lower bound implies equality </title>
(<-> (= A B) (/\ (<= A B) (<= B A)))
letot # <title> Integer Total Relationship </title>
(\/ (<= A B) (<= B A))
NeqReplaceImp1Nle0Nadd0 # <title> Substitution </title> # <table> # (-> ph (n.<= (n.+ [ A ] ] ] C) D)) # (n.= [ A ] [ B ] ) # (-> ph (n.<= (n.+ [ [ [ B ] C) D)) # </table>
(-> ph (n.<= (n.+ a c) d)) , (n.= a b)(-> ph (n.<= (n.+ b c) d))
NeqReplaceImp1Nle0Nadd1 # <title> Substitution </title> # <table> # (-> ph (n.<= (n.+ a [ B ] ] ] ) D)) # (n.= [ B ] [ C ] ) # (-> ph (n.<= (n.+ a [ [ [ C ] ) D)) # </table>
(-> ph (n.<= (n.+ a b) d)) , (n.= b c)(-> ph (n.<= (n.+ a c) d))
NeqReplaceImp1Nle1Nadd0 # <title> Substitution </title> # <table> # (-> ph (n.<= a (n.+ [ B ] ] ] D))) # (n.= [ B ] [ C ] ) # (-> ph (n.<= a (n.+ [ [ [ C ] D))) # </table>
(-> ph (n.<= a (n.+ b d))) , (n.= b c)(-> ph (n.<= a (n.+ c d)))
NeqReplaceImp1Nle1Nadd1 # <title> Substitution </title> # <table> # (-> ph (n.<= a (n.+ b [ C ] ] ] ))) # (n.= [ C ] [ D ] ) # (-> ph (n.<= a (n.+ b [ [ [ D ] ))) # </table>
(-> ph (n.<= a (n.+ b c))) , (n.= c d)(-> ph (n.<= a (n.+ b d)))
NeqReplaceBi1Le1Add1 # <title> Substitution </title> # <table> # (<-> ph (n.<= a (n.+ b [ C ] ] ] ))) # (n.= [ C ] [ D ] ) # (<-> ph (n.<= a (n.+ b [ [ [ D ] ))) # </table>
(<-> ph (n.<= a (n.+ b c))) , (n.= c d)(<-> ph (n.<= a (n.+ b d)))
NeqReplaceBi1Le0Add0 # <title> Substitution </title> # <table> # (<-> ph (n.<= (n.+ [ A ] ] ] C) D)) # (n.= [ A ] [ B ] ) # (<-> ph (n.<= (n.+ [ [ [ B ] C) D)) # </table>
(<-> ph (n.<= (n.+ a c) d)) , (n.= a b)(<-> ph (n.<= (n.+ b c) d))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
(<-> (<= (0) A) (n.<= (tail A) (head A)))
lemul1 # <title> Transitive Property </title>
(-> (/\ (<= A B) (<= (0) C)) (<= (* A C) (* B C)))
NeqReplaceBi1Nle0 # <title> Substitution </title> # <table> # (<-> ph (n.<= [ A ] ] ] C)) # (n.= [ A ] [ B ] ) # (<-> ph (n.<= [ [ [ B ] C)) # </table>
(<-> ph (n.<= a c)) , (n.= a b)(<-> ph (n.<= b c))
NeqReplaceBi1Nle1 # <title> Substitution </title> # <table> # (<-> ph (n.<= a [ B ] ] ] )) # (n.= [ B ] [ C ] ) # (<-> ph (n.<= a [ [ [ C ] )) # </table>
(<-> ph (n.<= a b)) , (n.= b c)(<-> ph (n.<= a c))
EqReplaceBi1Eq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (= A B)) , (= B C)(<-> ph (= A C))
0le1 # <title> One-Digit Inequality </title>
(<= (0) (1))
EqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (<= [ [ [ B ] C)) # </table>
(<-> ph (<= A C)) , (= A B)(<-> ph (<= B C))
EqReplaceBi1Eq1Add1 # <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)))
BiReplaceBi0Ex1 # <title> Substitution </title> # <table> # (<-> (E. x [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (<-> (E. x [ [ [ ps ] ) ch) # </table>
(<-> (E. x ph) ch) , (<-> ph ps)(<-> (E. x ps) ch)
BiReplaceBi0Ex1An1 # <title> Substitution </title> # <table> # (<-> (E. x (/\ ph [ ps ] ] ] )) th) # (<-> [ ps ] [ ch ] ) # (<-> (E. x (/\ ph [ [ [ ch ] )) th) # </table>
(<-> (E. x (/\ ph ps)) th) , (<-> ps ch)(<-> (E. x (/\ ph ch)) th)
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceBi1Eq0 # <title> Substitution </title> # <table> # (<-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (= [ [ [ B ] C)) # </table>
(<-> ph (= A C)) , (= A B)(<-> ph (= B C))
exle # <title> One-Digit Inequality </title>
(<-> (<= A B) (E. x (/\ (<= (0) x) (= (+ A x) B))))