# List of theorems

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

df-naturals # <title> Def. Naturals as a Subset of the Integers </title>
(=_ (N) ({|} y (<= (0) y)))
natpos # <title> Natural Numbers are not negative </title>
(<-> (e. A (N)) (<= (0) A))
EqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (<= [ [ [ B ] C)) # </table>
(<-> ph (<= A C)) , (= A B)(<-> ph (<= B C))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
(-> (/\ (e. A (N)) (e. B (N))) (e. (+ A B) (N)))
EqReplaceImp1Le1 # <title> Substitution </title> # <table> # (-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (<= A [ [ [ C ] )) # </table>
(-> ph (<= A B)) , (= B C)(-> ph (<= A C))
EqReplaceImp1Le0 # <title> Substitution </title> # <table> # (-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (<= [ [ [ B ] C)) # </table>
(-> ph (<= A C)) , (= A B)(-> ph (<= B C))
(-> (/\ (e. A (N)) (e. B (N))) (e. (* A B) (N)))
df-n # <title> Def. Integer to Natural Conversion </title>
(n.= (n A) (n..- (head A) (tail A)))
NeqReplaceImp1Neq1 # <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))
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))
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
NeqReplaceBi0Neq1 # <title> Substitution </title> # <table> # (<-> (n.= a [ B ] ] ] ) ph) # (n.= [ B ] [ C ] ) # (<-> (n.= a [ [ [ C ] ) ph) # </table>
(<-> (n.= a b) ph) , (n.= b c)(<-> (n.= a c) ph)
natpos2 # <title> Natural numbers are not negative </title>
(<-> (e. A (N)) (n.<= (tail A) (head A)))
(-> (/\ (e. A (N)) (/\ (e. B (N)) (= A B))) (n.= (n A) (n B)))
EqReplaceBi0Eq0 # <title> Substitution </title> # <table> # (<-> (= [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (<-> (= [ [ [ B ] C) ph) # </table>
(<-> (= A C) ph) , (= A B)(<-> (= B C) ph)
NeqReplaceBi1Neq0 # <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))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
NeqReplaceImp1Eq1Op0 # <title> Substitution </title> # <table> # (-> ph (= A (<,> [ b ] ] ] d))) # (n.= [ b ] [ c ] ) # (-> ph (= A (<,> [ [ [ c ] d))) # </table>
(-> ph (= A (<,> b d))) , (n.= b c)(-> ph (= A (<,> c d)))
natAsInt # <title> Natural Number as an Integer </title> # <summary> # Express a natural number as an ordered pair representing an # integer with a negative part of 0. # </summary>
(-> (e. A (N)) (= A (<,> (n A) (n.0))))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
NeqReplaceImp1Bi1Neq0 # <title> Substitution </title> # <table> # (-> ph (<-> ps (n.= [ a ] ] ] c))) # (n.= [ a ] [ b ] ) # (-> ph (<-> ps (n.= [ [ [ b ] c))) # </table>
(-> ph (<-> ps (n.= a c))) , (n.= a b)(-> ph (<-> ps (n.= b c)))
NeqReplaceImp1Bi1Neq1 # <title> Substitution </title> # <table> # (-> ph (<-> ps (n.= a [ b ] ] ] ))) # (n.= [ b ] [ c ] ) # (-> ph (<-> ps (n.= a [ [ [ c ] ))) # </table>
(-> ph (<-> ps (n.= a b))) , (n.= b c)(-> ph (<-> ps (n.= a c)))
(-> (/\ (e. A (N)) (e. B (N))) (<-> (= A B) (n.= (n A) (n B))))
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))
0tailpos # <title> A number with no negative part is natural </title>
(e. (<,> a (n.0)) (N))
NeqReplaceNeq1 # <title> Substitution </title> # <table> # (n.= a [ b ] ] ] ) # (n.= [ b ] [ c ] ) # (n.= a [ [ [ c ] ) # </table>
(n.= a b) , (n.= b c)(n.= a c)
(n.= (n (<,> a (n.0))) a)
tail0eq # <title> Integer to Natural Equality </title>
(-> (= A (<,> b (n.0))) (n.= (n A) b))
(-> (/\ (e. A (N)) (e. B (N))) (n.= (n (+ A B)) (n.+ (n A) (n B))))
(-> (/\ (e. A (N)) (e. B (N))) (n.= (n (* A B)) (n.* (n A) (n B))))
NeqReplaceImp1Bi1Nle0 # <title> Substitution </title> # <table> # (-> ph (<-> ps (n.<= [ a ] ] ] c))) # (n.= [ a ] [ b ] ) # (-> ph (<-> ps (n.<= [ [ [ b ] c))) # </table>
(-> ph (<-> ps (n.<= a c))) , (n.= a b)(-> ph (<-> ps (n.<= b c)))
NeqReplaceImp1Bi1Nle1 # <title> Substitution </title> # <table> # (-> ph (<-> ps (n.<= a [ b ] ] ] ))) # (n.= [ b ] [ c ] ) # (-> ph (<-> ps (n.<= a [ [ [ c ] ))) # </table>
(-> ph (<-> ps (n.<= a b))) , (n.= b c)(-> ph (<-> ps (n.<= a c)))
(-> (/\ (e. A (N)) (e. B (N))) (<-> (<= A B) (n.<= (n A) (n B))))
EqReplaceEl0 # <title> Substitution </title> # <table> # (e. [ A ] ] ] S) # (= [ A ] [ B ] ) # (e. [ [ [ B ] S) # </table>
(e. A S) , (= A B)(e. B S)
0nat # <title> 0 is a Natural Number </title>
(e. (0) (N))
1nat # <title> 1 is a Natural Number </title>
(e. (1) (N))
(n.= (n (0)) (n.0))
(n.= (n (1)) (n.1))
(-> (/\ (= A B) (e. A (N))) (n.= (n A) (n B)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
(-> (= A B) (<-> (/\ (e. A (N)) (n.= (n A) a)) (/\ (e. B (N)) (n.= (n B) a))))
df-ns # <title> Def. Integer to Natural Set Conversion </title>
(n.=_ (ns S) (n.{|} Y (E. y (/\ (e. y S) (/\ (e. y (N)) (n.= (n y) Y))))))
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)
BiReplaceBi1An0 # <title> Substitution </title> # <table> # (<-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ [ [ [ ch ] th)) # </table>
(<-> ph (/\ ps th)) , (<-> ps ch)(<-> ph (/\ ch th))
BiReplaceBi1An1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps [ [ [ th ] )) # </table>
(<-> ph (/\ ps ch)) , (<-> ch th)(<-> ph (/\ ps th))
ImpReplaceBi1An1 # <title> Substitution </title> # <table> # (<-> ph (/\ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (<-> ph (/\ ps [ [ [ th ] )) # </table>
(<-> ph (/\ ps ch)) , (-> ch th)(-> ph (/\ ps th))
ImpReplaceBi1An1An1 # <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)))
BiReplaceBi1An1An1 # <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)))
BiReplaceImp1Bi1Ex1 # <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)))
(-> (/\ (e. A (N)) (C_ S (N))) (<-> (e. A S) (E. x (/\ (e. x (N)) (/\ (e. x S) (n.= (n x) (n A)))))))
(-> (/\ (e. A (N)) (C_ S (N))) (<-> (e. A S) (n.e. (n A) (ns S))))
df-n-1 # <title> Def. Natural to Integer Conversion </title>
(= (n-1 a) (<,> a (n.0)))
EqReplaceBi0Eq1 # <title> Substitution </title> # <table> # (<-> (= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (= A [ [ [ C ] ) ph) # </table>
(<-> (= A B) ph) , (= B C)(<-> (= A C) ph)
(-> (= A (n-1 a)) (n.= (n A) a))
ninv # <title> Natural conversion has an inverse </title>
(n.= (n (n-1 a)) a)
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)