# List of theorems

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

df-head # <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 equality # for integers involving pairs of natural numbers. These theorems # demonstrate that this integer equality has all the essential properties we # expect for equality. # </context>
(n.= (tail A) (n.tail A))
NeqReplaceNeq0 # <title> Substitution </title> # <table> # (n.= [ A ] ] ] C) # (n.= [ A ] [ B ] ) # (n.= [ [ [ B ] C) # </table>
(n.= A C) , (n.= A B)(n.= B C)
NeqReplaceNeq1 # <title> Substitution </title> # <table> # (n.= A [ B ] ] ] ) # (n.= [ B ] [ C ] ) # (n.= A [ [ [ C ] ) # </table>
(n.= A B) , (n.= B C)(n.= A C)
df-eq # <title> Definition of Integer Equality </title> # <summary> # An integer is defined as an order pair of natural numbers. The first # number in the pair represents the positive part of the number, the # second number represent the negative part of the number. Thus (0,0), # (1,1), (2,2) are all equivalent to the integer 0, since their negative # and positive parts are equal. (A, 0) presents +A. (0, A) represents -A. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. # </summary> # <suggest> left('Simplify', '=') </suggest>
(<-> (= A B) (n.= (n.+ (head A) (tail B)) (n.+ (head B) (tail A))))
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))
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))
(-> (n.= A B) (n.= (tail A) (tail B)))
eqzeq # <title> Convert Natural to Integer Equality </title> # <suggest> right('Infer', '=z') </suggest>
(-> (n.= A B) (= A B))
eqzeqi # <title> Convert Natural to Integer Equality </title>
(n.= A B)(= A B)
eqzeqd # <title> Convert Natural to Integer Equality </title>
(-> ph (n.= A B))(-> ph (= A B))
NeqReplaceBi1Neq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (n.= A B)) , (n.= B C)(<-> ph (n.= A C))
eqid # <title> Reflexive Property </title> # <summary> Integer equality is reflexive. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. #</summary>
(= A A)
eqcom # <title> Symmetric Property </title> # <summary> Integer equality is symmetric. # For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. # </summary> # <suggest> right('Commute', '=') </suggest>
(<-> (= A B) (= B A))
zeqcomi # <title> Symmetric Property </title> # <table> # (= <r> A <g> B) # (= <g> B <r> A) # </table>
(= A B)(= B A)
NeqReplaceImp1Neq1Add0 # <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)))
eqtr # <title> Transitive Property </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/integers">construction of the integers</a>. </summary> # <suggest> right('Simplify', '=') </suggest>
(-> (/\ (= A B) (= B C)) (= A C))
(-> (= A B) (<-> (= A C) (= B C)))
zeqeq1i # <title> Equivalence over Equality </title>
(= A B)(<-> (= A C) (= B C))
zeqeq2 # <title> Equivalence over Equality </title>
(-> (= A B) (<-> (= C A) (= C B)))
zeqeq2i # <title> Equivalence over Equality </title> # <table> # (= [ A ] [ [ B) # (<-> (= C [ A) ] [ (= C [ B)) # </table>
(= A B)(<-> (= C A) (= C B))
(n.= (<,> a b) (n.<,> a b))
(= (<,> a b) (n.<,> a b))
(= A (<,> (head A) (tail A)))
(n.= a b)(= (<,> a c) (<,> b c))
(n.= a b)(= (<,> c a) (<,> c b))
(-> (/\ (n.= a b) (n.= c d)) (= (<,> a c) (<,> b d)))
(n.= (head (<,> A B)) A)
(n.= (tail (<,> A B)) B)
(<-> (A. x ph) (n.A. x ph))
alnfi # <summary> Reproved for integers directly from the natural number version. </title>
(-> ph (A. x ph))
gen # <title> Generalization Axiom </title> # <table> # [ ph ] # (A. x [ ph ] ) # </table> # <summary> Reproved for integers directly from the natural number version. </title>
ph(A. x ph)
ax-4 roughly Margaris A5, but without the subst # <title> Axiom 4: Specialization </title> # <suggest> right('Remove', '∀') </suggest>
(-> (A. x ph) ph)
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))
ax-alim # <title> Axiom 5: Quantified Implication </title>
(-> (A. x (-> ph ps)) (-> (A. x ph) (A. x ps)))
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
ax-6 # <title> Axiom 6: Quantified Negation </title>
(-> (-. (A. x ph)) (A. x (-. (A. x ph))))
ax-7 # <title> Axiom 7: Quantifier Commutation </title>
(-> (A. x (A. y ph)) (A. y (A. x ph)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
nexex # <title> Natural and Integer Existence are the same </title>
(<-> (n.E. x ph) (E. x ph))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
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))
ImpReplaceEx1 # <title> Substitution </title> # <table> # (E. x [ ph ] ] ] ) # (-> [ ph ] [ ps ] ) # (E. x [ [ [ ps ] ) # </table>
(E. x ph) , (-> ph ps)(E. x ps)
EqReplaceEx1Eq1 # <title> Substitution </title> # <table> # (E. x (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (E. x (= A [ [ [ C ] )) # </table>
(E. x (= A B)) , (= B C)(E. x (= A C))
tyex # <title> One-Digit Inequality </title>
(E. z (= z A))
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))
NeqReplaceBi1Neq0Add0 # <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))
NeqReplaceBi1Neq0Add1 # <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))
NeqReplaceBi1Neq1Add0 # <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)))
NeqReplaceBi1Neq1Add1 # <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)))
opzeq # <title> Natural-Integer Equality Conversion </title> # <suggest> right('Equivalence', '=N') left('Equivalence', '=z') </suggest>
(<-> (= (<,> a b) (<,> c d)) (n.= (n.+ a d) (n.+ c b)))
zeqexpand # <title> Expand Integer Equality </title>
(-> (= A B) (n.= (n.+ (head A) (tail B)) (n.+ (head B) (tail A))))
df-int # <title> Def. Natural to Integer Mapping </title> # <summary> # Defines a mapping between a natural number to an ordered pair # that represents the same number as an integer. Subsequent # theorems show that this mapping is a homomorphism respecting # <a href="addhomomorph">addition</a>, <a href="df-mul">multiplication</a>, # and <a href="lehomomorph">inequality</a>. # </summary> # <suggest> left('Simplify', 'int') </suggest>
(= (int a) (<,> a (n.0)))