# List of theorems

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

df-le-just # <context> # This theorem is part of a series of theorems that derive the # most basic properties of the less than or equal to relation from the # <a href="/wiki/peano/arithmetic/axioms">Peano axiom</a>. # It is assumed that every number in this theorem is a natural number. # These theorems demonstrate that the natural numbers have all the essential # properties of a totally ordered set. # </context>
(<-> (E. x (= (+ A x) B)) (E. y (= (+ A y) B)))
df-le # <title> Definition of Less Than or Equal to </title> # <suggest> right('Define', '≤') left('Simplify', '≤') </suggest>
(<-> (<= A B) (E. x (= (+ A x) B)))
df-lt # <title> Definition of Less Than </title>
(<-> (< A B) (/\ (<= A B) (-. (= A B))))
leeq1d # <title> Inequality Equivalence </title> # <summary> Equality deduction for less than or equal relation </summary>
(-> ph (= A B))(-> ph (<-> (<= A C) (<= B C)))
leeq2d # <title> Inequality Equivalence </title> # <summary> Equality deduction for less than or equal relation </summary> # <table> # (-> ph (= [ A ] [ [ B ] )) # (-> ph (<-> (<= C [ A ] ) (<= [ C [ B ] ))) # </table>
(-> ph (= A B))(-> ph (<-> (<= C A) (<= C B)))
leeq1 # <title> Inequality Equivalence </title>
(-> (= A B) (<-> (<= A C) (<= B C)))
leeq2 # <title> Inequality Equivalence </title>
(-> (= A B) (<-> (<= C A) (<= C B)))
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))
leadd1 # <title> Addition is Monotonic </title> # <summary> Addition is strictly monotonic in the first addend </summary> # <suggest> left('Cancel', '+') </suggest>
(<-> (<= 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)))
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))
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)))
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)))
gteq2 # <title> Equivalence for > </title> ##
(-> (= B C) (<-> (> A B) (> A C)))
(= B C)(<-> (> A B) (> A C))
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))
EqReplaceNot0Eq0 # <title> Substitution </title> # <table> # (-. (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-. (= [ [ [ B ] C)) # </table>
(-. (= A C)) , (= A B)(-. (= B C))
1nle0 # <title> Basic Inequality </title>
(> (1) (0))
(<= A (+ A B))
(<= A (+ B A))
leid # <title> Reflexive Property </title> # <summary> Less than or equal is a reflexive relation </summary>
(<= A A)
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
(> (+ A (1)) A)
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))
provele # <title> Addition implies ≤ </title>
(-> (= (+ A B) C) (<= A C))
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)
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
letr # <title> Transitive Property </title> # <suggest> right('Simplify', '≤ ≤') </suggest>
(-> (/\ (<= A B) (<= B C)) (<= A C))
(\/ (= A (0)) (E. z (= (+ (1) z) A)))
(<-> (<= A B) (\/ (= A B) (<= (+ A (1)) B)))
(<-> (< A B) (<= (+ A (1)) B))
lePlus1 # <title> Convert between ≤ and < </title> # <summary> This proves that natural numbers are whole numbers. </summary> # <suggest> right('Equivalence', '≤-1') left('Equivalence', '<') </suggest>
(<-> (< A (+ B (1))) (<= A B))
ge0 # <title> No Natural Numbers Below Zero </title>
(>= A (0))
lecon # <title> Converse of ≤ </title> # <suggest> right('Commute', '≤') left('Commute', '≥') </suggest>
(<-> (<= A B) (>= B A))
0le # <title> No Natural Numbers Below Zero </title>
(<= (0) A)
lesym # <title> Same upper and lower bound implies equality </title> # <summary> Trichotomy law (may be a poor choice of name) </summary> # <suggest> left('Simplify', '=') </suggest>
(<-> (= A B) (/\ (<= A B) (<= B A)))
letot # <title> Total Relationship </title> # <summary> Less than or equal is a total relationship </summary>
(\/ (<= A B) (<= B A))
lemul2nat # <title> Multiply Both Sides </title> # <summary> Multiplication is monotonic in its second argument </summary>
(-> (<= A B) (<= (* C A) (* C B)))
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))
lemul1n # <title> Inequality Multiplication </title>
(-> (<= A B) (<= (* A C) (* B C)))
lemul1 # <title> Inequality Multiplication </title> # <summary> # This theorem takes <a href="lemuln">lemuln</a> and adds and extra restriction # that C ≥ 0. From <a href="0le">0le</a> we know that this is true for all natural # numbers, but this theorem is used in an interface where the numbers may not be # natural numbers. # </summary>
(-> (/\ (<= A B) (<= (0) C)) (<= (* A C) (* B C)))
0le1 # <title> 0 is less than or equal to 1 </title> # <summary> # This theorem applies the <a href="0le">0le</a> theorem that all natural numbers # are greater than or equal to 0. This theorem is used in an interface where the numbers # are be negative and <a href="0le">0le</a> does not apply. # </summary>
(<= (0) (1))
axlttri # <title> Inequality Conversion </title> # <suggest> left('Simplify', '<') </suggest>
(<-> (< A B) (-. (\/ (= A B) (< B A))))
exle # <title> Less Than or Equal from Nonnegative Difference </title>
(<-> (<= A B) (E. x (/\ (<= (0) x) (= (+ A x) B))))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
(-> (<= (* A (+ C (1))) (* B (+ C (1)))) (<= A B))
lemul5 # <summary> Multiplication is strictly monotonic with nonzero multiplicand </summary>
(<-> (<= (* A (+ C (1))) (* B (+ C (1)))) (<= A B))
eq0le0 # <summary> For naturals, equal to zero is equivalent to less than or equal to zero </summary>
(<-> (= A (0)) (<= A (0)))
sindlem1 number 58.0
(-> ch (-> ps (\/ (-> th ph) ta))) , (-> si (/\ th (-> ta ph)))(-> si (-> ch (-> ps ph)))
BiReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (<-> ch th)(-> ph (\/ ps th))
ImpReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (-> ch th)(-> ph (-> ps th))
sind # <title> Strong Induction </title>
(-> (= x (0)) (<-> ph ps)) , (-> (= x (+ y (1))) (<-> ph th)) , (-> (= x A) (<-> ph ta)) , ps , (-> (A. x (-> (<= x y) ph)) th)ta
0orpos number 40.0 # <title> Natural Number </title>
(\/ (= A (0)) (<= (1) A))