# List of theorems

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

df-head # <context> # This theorem is part of a series of theorems constructing the complex numbers. # A complex number is constructed as a pair of real numbers which # represents the real and the imaginary part of the complex number. This requires # us to construct a new version of equality for complex numbers. These theorems # demonstrate that this complex equality has all the essential properties we # expect for equality. # </context>
(r.= (tail A) (r.tail A))
ReqReplaceReq0 # <title> Substitution </title> # <table> # (r.= [ A ] ] ] C) # (r.= [ A ] [ B ] ) # (r.= [ [ [ B ] C) # </table>
(r.= A C) , (r.= A B)(r.= B C)
ReqReplaceReq1 # <title> Substitution </title> # <table> # (r.= A [ B ] ] ] ) # (r.= [ B ] [ C ] ) # (r.= A [ [ [ C ] ) # </table>
(r.= A B) , (r.= B C)(r.= A C)
df-eq # <title> Definition of Complex Equality </title> # <summary> # A complex number is defined as an order pair of real numbers. The first # number in the pair represents the real part of the number, the # second number represent the imaginary part. # </summary> # <suggest> left('Simplify', '=') </suggest>
(<-> (= A B) (/\ (r.= (r.head A) (r.head B)) (r.= (r.tail A) (r.tail B))))
(<-> (= A B) (/\ (r.= (head A) (head B)) (r.= (tail A) (tail B))))
ceqeq # <title> Complex and Read Equality are equivalent </title> # <summary> # Yes, they are exactly the same, but its useful to define a new version # of equality so that we can keep the real and complex kinds separate. # </summary>
(<-> (r.= A B) (= A B))
(= A A)
(<-> (= A B) (= B A))
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
(-> (/\ (= A B) (= B C)) (= A C))
(-> (= A B) (<-> (= A C) (= B C)))
ceqeq1i # <title> Equivalence over Equality </title>
(= A B)(<-> (= A C) (= B C))
ceqeq2 # <title> Equivalence over Equality </title>
(-> (= A B) (<-> (= C A) (= C B)))
ceqeq2i # <title> Equivalence over Equality </title> # <table> # (= [ A ] [ [ B) # (<-> (= C [ A) ] [ (= C [ B)) # </table>
(= A B)(<-> (= C A) (= C B))
(= (<,> a b) (r.<,> a b))
ceqcomi # <title> Symmetric Property </title> # <table> # (= <r> A <g> B) # (= <g> B <r> A) # </table>
(= A B)(= B A)
(= A (<,> (head A) (tail A)))
eqceqi # <title> Convert Natural to Integer Equality </title>
(r.= A B)(= A B)
(r.= (<,> A B) (r.<,> A B))
(-> (r.= a b) (= (<,> a c) (<,> b c)))
(-> (r.= a b) (= (<,> c a) (<,> c b)))
(r.= A C)(= (<,> A B) (<,> C B))
(-> ph (r.= a c))(-> ph (= (<,> a b) (<,> c b)))
(r.= B C)(= (<,> A B) (<,> A C))
(-> ph (r.= B C))(-> ph (= (<,> A B) (<,> A C)))
opeq12 # <title> Equivalence for <,> </title> ##
(-> (/\ (r.= a b) (r.= c d)) (= (<,> a c) (<,> b d)))
(-> ph (r.= A B)) , (-> ph (r.= C D))(-> ph (= (<,> A C) (<,> B D)))
ReqReplaceImp1Req0 # <title> Substitution </title> # <table> # (-> ph (r.= [ a ] ] ] c)) # (r.= [ a ] [ b ] ) # (-> ph (r.= [ [ [ b ] c)) # </table>
(-> ph (r.= a c)) , (r.= a b)(-> ph (r.= b c))
ReqReplaceImp1Req1 # <title> Substitution </title> # <table> # (-> ph (r.= a [ b ] ] ] )) # (r.= [ b ] [ c ] ) # (-> ph (r.= a [ [ [ c ] )) # </table>
(-> ph (r.= a b)) , (r.= b c)(-> ph (r.= a c))
(r.= (head (<,> A B)) A)
(-> (r.= A B) (r.= (tail A) (tail B)))
(r.= (tail (<,> A B)) B)
(<-> (A. x ph) (r.A. x ph))
alnfi # <summary> Reproved for integers directly from the natural number versior. </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 versior. </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))
cexex # <title> Real and Complex Existence are the same </title>
(<-> (r.E. x ph) (E. x ph))
(E. z (= z A))