# List of theorems

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

df-eqn # <context> # This theorem is part of a series of theorems that take theorems that are valid only # for natural numbers and export them into more general contexts. Lower case numbers # are assumed to be natural numbers. Upper case numbers are in a more general context # where you must specify that each number is part of the set of natural numbers. This # allowed us to export theorems proved in the natural numbers directory and use them # with integer, rational, real, and complex numbers. # </context> # <title> Def. nat to n.nat equality </title> # <summary> # The normal equality = involves two nats. The natural equality involves two n.nats. # This equality involves a nat on the left and a n.nat on the right. # </summary>
(<-> (=n A a) (/\ (e. A (N)) (n.= (n A) a)))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
dfeqn1 # <title> Partial Def. of Equality </title> # <summary> Just use the first half of the definition of =n. </summary>
(-> (=n A a) (e. A (N)))
dfeqn2 # <title> Partial Def. of Equality </title> # <summary> Just use the second half of the definition of =n. </summary>
(-> (=n A a) (n.= (n A) a))
(<-> (e. A (N)) (=n A (n A)))
eqn # <title> Identity </title>
(-> (e. A (N)) (=n A (n A)))
eqntr # <title> Transitive Property </title>
(-> (/\ (=n A (n B)) (=n B a)) (=n A a))
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (n.= (n.+ (n A) (n B)) (n.+ a b)))
natAdd1 # <table> # (-> ph (=n A ] ] ] [ a ] ] )) # (-> ph (=n [ [ B ] [ [ [ b)) # (-> ph (=n (+ A ] [ B ] ) (n.+ [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (=n (+ A B) (n.+ a b)))
natAdd2 # <table> # (-> ph ] ] ] (=n A ] ] ] [ a ] ] )) # (-> [ [ ps ] (=n [ [ B ] [ [ [ b)) # (-> (/\ ph ] [ ps ] ) (=n (+ A ] [ B ] ) (n.+ [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ps (=n B b))(-> (/\ ph ps) (=n (+ A B) (n.+ a b)))
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (n.= (n.* (n A) (n B)) (n.* a b)))
natMul1 # <table> # (-> ph (=n A ] ] ] [ a ] ] )) # (-> ph (=n [ [ B ] [ [ [ b)) # (-> ph (=n (* A ] [ B ] ) (n.* [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (=n (* A B) (n.* a b)))
natMul2 # <table> # (-> ph ] ] ] (=n A ] ] ] [ a ] ] )) # (-> [ [ ps ] (=n [ [ B ] [ [ [ b)) # (-> (/\ ph ] [ ps ] ) (=n (* A ] [ B ] ) (n.* [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ps (=n B b))(-> (/\ ph ps) (=n (* A B) (n.* a b)))
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (<-> (n.<= (n A) (n B)) (n.<= a b)))
natLe1 # <table> # (-> ph (=n A ] ] ] [ a ] ] )) # (-> ph (=n [ [ B ] [ [ [ b)) # (-> ph (<-> (<= A ] [ B ] ) (n.<= [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (<-> (<= A B) (n.<= a b)))
natLe2 # <table> # (-> ph ] ] ] (=n A ] ] ] [ a ] ] )) # (-> [ [ ps ] (=n [ [ B ] [ [ [ b)) # (-> (/\ ph ] [ ps ] ) (<-> (<= A ] [ B ] ) (n.<= [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ps (=n B b))(-> (/\ ph ps) (<-> (<= A B) (n.<= a b)))
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (<-> (n.= (n A) (n B)) (n.= a b)))
natEq1 # <table> # (-> ph (=n A ] ] ] [ a ] ] )) # (-> ph (=n [ [ B ] [ [ [ b)) # (-> ph (<-> (<= A ] [ B ] ) (n.<= [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ph (=n B b))(-> ph (<-> (= A B) (n.= a b)))
natEq2 # <table> # (-> ph ] ] ] (=n A ] ] ] [ a ] ] )) # (-> [ [ ps ] (=n [ [ B ] [ [ [ b)) # (-> (/\ ph ] [ ps ] ) (<-> (= A ] [ B ] ) (n.= [ a ] [ b))) # </table>
(-> ph (=n A a)) , (-> ps (=n B b))(-> (/\ ph ps) (<-> (= A B) (n.= a b)))
(=n (0) (n.0))
(=n (1) (n.1))
(-> (e. A (N)) (<= (0) A))
(-> (/\ (e. A (N)) (e. B (N))) (<= A (+ A B)))
EqReplaceImp1Le1 # <title> Substitution </title> # <table> # (-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (<= A [ [ [ C ] )) # </table>
(-> ph (<= A B)) , (= B C)(-> ph (<= A C))
(-> (/\ (e. A (N)) (e. B (N))) (<= A (+ B A)))
(-> (/\ (e. A (N)) (/\ (e. B (N)) (e. C (N)))) (-> (= (+ A B) C) (<= A C)))
(-> (/\ (e. A (N)) (e. B (N))) (<-> (<= A B) (\/ (= A B) (<= (+ A (1)) B))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)