# List of theorems

List of theorems in peano_new/arithmetic/rationals/NaN_construction/equality_min.gh:

df-al # <context> # This theorem is part of a series of theorems # <a href="/wiki/peano/arithmetic/rationals">constructing rational number</a>. # A rational number is constructed as a # pair of natural numbers which represents the numerator and the denominator part # of a fraction. This requires us to construct a new version of equality # for fractions involving pairs of integers. These theorems # demonstrate that this rational equality has all the essential properties we # expect for equality. # </context> Briefly Add Back Predicate Calculus # <summary> # To be able to bind z.nat and nat we cannot import predicate because that would reintroduce nat. # So we have to prove everything in predicate_min from z. Here we redefine z.A. as A. # </summary>
(<-> (A. x ph) (z.A. x ph))
alnfi # <summary> Reproved for integers directly from the natural number versioz. </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 versioz. </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))
zexex # <title> Rational and Integer Existence are the same </title>
(<-> (z.E. x ph) (E. x ph))
ZeqReplaceImp1Zeq0 # <title> Substitution </title> # <table> # (-> ph (z.= [ A ] ] ] C)) # (z.= [ A ] [ B ] ) # (-> ph (z.= [ [ [ B ] C)) # </table>
(-> ph (z.= A C)) , (z.= A B)(-> ph (z.= B C))
ZeqReplaceImp1Zeq1 # <title> Substitution </title> # <table> # (-> ph (z.= A [ B ] ] ] )) # (z.= [ B ] [ C ] ) # (-> ph (z.= A [ [ [ C ] )) # </table>
(-> ph (z.= A B)) , (z.= B C)(-> ph (z.= A C))
df-top # <title> Definition of numerator </title> # <summary> # The numerator or top of a rational number. This is the same as the head of an # ordered pair. This definition is just a way of explaining that the head # of the ordered pair is the numerator. The head of the ordered pair is expected # to be in the format of an integer. This is only used in the construction of the rationals. It is # ambiguous since the number 1/2, could be represented as 1/2, 2/4, or 6/12 and the bottom value # would be different in each case. Thus all the theorems in the construction of the rationals # assume that we do not know the value of bottom, we only know the ratio between the top and bottom # values. # </summary>
topeq # <title> Equivalence for numerator </title>
(-> (z.= A B) (z.= (top A) (top B)))
df-bottom # <title> Definition of denominator </title> # <summary> # The numerator or bottom of a rational number. This is the same as the tail of an # ordered pair. This definition is just a way of explaining that the tail # of the ordered pair is the denominator. The tail of the ordered pair is expected # to be in the format of an integer. This is only used in the construction of the rationals. It is # ambiguous since the number 1/2, could be represented as 1/2, 2/4, or 6/12 and the bottom value # would be different in each case. Thus all the theorems in the construction of the rationals # assume that we do not know the value of bottom, we only know the ratio between the top and bottom # values. # </summary>
(z.= (bottom A) (z.tail A))
bottomeq # <title> Equivalence for denominator </title>
(-> (z.= A B) (z.= (bottom A) (bottom B)))
(-> ph (z.= A B))(-> ph (z.= (bottom A) (bottom B)))
NeqReplaceNeq0 # <title> Substitution </title> # <table> # (z.= [ A ] ] ] C) # (z.= [ A ] [ B ] ) # (z.= [ [ [ B ] C) # </table>
(z.= A C) , (z.= A B)(z.= B C)
NeqReplaceNeq1 # <title> Substitution </title> # <table> # (z.= A [ B ] ] ] ) # (z.= [ B ] [ C ] ) # (z.= A [ [ [ C ] ) # </table>
(z.= A B) , (z.= B C)(z.= A C)
df-eq # <title> Definition of Rational Equality </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. </summary> # <suggest> left('Simplify', '=') </suggest>
(<-> (= A B) (/\ (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0)))))
dfeq1 # <title> Part of the Rational Equality Definition </title>
(-> (= A B) (z.= (z.* (top A) (bottom B)) (z.* (top B) (bottom A))))
dfeq2 # <title> Part of the Rational Equality Definition </title>
(-> (= A B) (<-> (z.= (bottom A) (z.0)) (z.= (bottom B) (z.0))))
eqid # <title> Reflexive Property </title>
(= A A)
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))
eqcom # <title> Symmetric Property </title> # <summary> Rational equality is symmetric. # For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. </summary> # <suggest> right('Commute', '=') </suggest>
(<-> (= A B) (= B A))
BiReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (<-> ch th)(-> ph (/\ ps th))
ImpReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (-> ch th)(-> ph (/\ ps th))
(-> (/\ (= A B) (= B C)) (<-> (z.= (bottom A) (z.0)) (z.= (bottom C) (z.0))))
eqtr.1 # <title> First Part of Transitivity Proof </title>
(-> (= A B) (-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (z.= (top A) (z.0))))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
ZeqReplaceImp1Imp1Zeq1 # <title> Substitution </title> # <table> # (-> ph (-> ps (z.= A [ B ] ] ] ))) # (z.= [ B ] [ C ] ) # (-> ph (-> ps (z.= A [ [ [ C ] ))) # </table>
(-> ph (-> ps (z.= a b))) , (z.= b c)(-> ph (-> ps (z.= a c)))
BiReplaceImp1Imp0An1 # <title> Substitution </title> # <table> # (-> ph (-> (/\ ps [ ch ] ] ] ) ta)) # (<-> [ ch ] [ th ] ) # (-> ph (-> (/\ ps [ [ [ th ] ) ta)) # </table>
(-> ph (-> (/\ ps ch) ta)) , (<-> ch th)(-> ph (-> (/\ ps th) ta))
(-> (/\ (z.= (top B) (z.0)) (-. (z.= (bottom B) (z.0)))) (-> (/\ (= A B) (= B C)) (= A C)))
(-> (/\ (z.= (bottom B) (z.0)) (= A B)) (z.= (bottom A) (z.0)))
BiReplaceImp0An1 # <title> Substitution </title> # <table> # (-> (/\ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph [ [ [ ch ] ) th) # </table>
(-> (/\ ph ps) th) , (<-> ps ch)(-> (/\ ph ch) th)
ZeqReplaceBi1An0Zeq0 # <title> Substitution </title> # <table> # (<-> ph (/\ (z.= [ A ] ] ] C) ps)) # (z.= [ A ] [ B ] ) # (<-> ph (/\ (z.= [ [ [ B ] C) ps)) # </table>
(<-> ph (/\ (z.= A C) ps)) , (z.= A B)(<-> ph (/\ (z.= B C) ps))
(-> (z.= (bottom B) (z.0)) (-> (/\ (= A B) (= B C)) (= A C)))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
ZeqReplaceImp1Not0Zeq0 # <title> Substitution </title> # <table> # (-> ph (-. (z.= [ A ] ] ] C))) # (z.= [ A ] [ B ] ) # (-> ph (-. (z.= [ [ [ B ] C))) # </table>
(-> ph (-. (z.= A C))) , (z.= A B)(-> ph (-. (z.= B C)))
(-> (/\ (-. (z.= (bottom B) (z.0))) (-. (z.= (top B) (z.0)))) (-> (/\ (= A B) (= B C)) (= A C)))
eqtr # <title> Transitive Property </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. </summary> # <suggest> right('Transitive', '=') </suggest>
(-> (/\ (= A B) (= B C)) (= A C))
(-> (= A B) (<-> (= A C) (= B C)))
eqqeqq2 # <title> Equivalence over Equality </title>
(-> (= A B) (<-> (= C A) (= C B)))
(= A B)(<-> (= C A) (= C B))
ZeqReplaceBi1Not0Zeq0 # <title> Substitution </title> # <table> # (<-> ph (-. (z.= [ A ] ] ] C))) # (z.= [ A ] [ B ] ) # (<-> ph (-. (z.= [ [ [ B ] C))) # </table>
(<-> ph (-. (z.= A C))) , (z.= A B)(<-> ph (-. (z.= B C)))
df-fraction # <title> Definition of Fraction </title> # <summary> # A fraction is just an ordered pair of integers. This definition signals to the # typesetter that the number should be displayed as a fraction and not an ordered pair. # </summary> # <title> Definition of Fraction </title>
(z.= (</> A B) (z.<,> A B))
topfrac # <title> Grab the top of a fraction </title> # <suggest> right('Simplify', 'Top') </suggest>
(z.= (top (</> a b)) a)
bottomfrac # <title> Grab the bottom of a fraction </title> # <suggest> right('Simplify', 'Bt') </suggest>
(z.= (bottom (</> a b)) b)
ZeqReplaceBi1Zeq1 # <title> Substitution </title> # <table> # (<-> ph (z.= A [ B ] ] ] )) # (z.= [ B ] [ C ] ) # (<-> ph (z.= A [ [ [ C ] )) # </table>
(<-> ph (z.= A B)) , (z.= B C)(<-> ph (z.= A C))
ZeqReplaceBi1Zeq0 # <title> Substitution </title> # <table> # (<-> ph (z.= [ A ] ] ] C)) # (z.= [ A ] [ B ] ) # (<-> ph (z.= [ [ [ B ] C)) # </table>
(<-> ph (z.= A C)) , (z.= A B)(<-> ph (z.= B C))
ZeqReplaceBi1Zeq0Mul1 # <title> Substitution </title> # <table> # (<-> ph (z.= (z.* A [ B ] ] ] ) D)) # (z.= [ B ] [ C ] ) # (<-> ph (z.= (z.* A [ [ [ C ] ) D)) # </table>
(<-> ph (z.= (z.* A B) D)) , (z.= B C)(<-> ph (z.= (z.* A C) D))
ZeqReplaceEq1Op0 # <title> Substitution </title> # <table> # (z.= A (z.<,> [ B ] ] ] D)) # (z.= [ B ] [ C ] ) # (z.= A (z.<,> [ [ [ C ] D)) # </table>
(z.= A (z.<,> B D)) , (z.= B C)(z.= A (z.<,> C D))
ZeqReplaceBi1An0Zeq1 # <title> Substitution </title> # <table> # (<-> ph (/\ (z.= A [ B ] ] ] ) ps)) # (z.= [ B ] [ C ] ) # (<-> ph (/\ (z.= A [ [ [ C ] ) ps)) # </table>
(<-> ph (/\ (z.= A B) ps)) , (z.= B C)(<-> ph (/\ (z.= A C) ps))
ZeqReplaceBi1An0Zeq1Mul1 # <title> Substitution </title> # <table> # (<-> ph (/\ (z.= A (z.* B [ C ] ] ] )) ps)) # (z.= [ C ] [ D ] ) # (<-> ph (/\ (z.= A (z.* B [ [ [ D ] )) ps)) # </table>
(<-> ph (/\ (z.= A (z.* B C)) ps)) , (z.= C D)(<-> ph (/\ (z.= A (z.* B D)) ps))
BiReplaceBi1An1Bi0 # <title> Substitution </title> # <table> # (<-> ph (/\ ps (<-> [ ch ] ] ] ta))) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps (<-> [ [ [ th ] ta))) # </table>
(<-> ph (/\ ps (<-> ch ta))) , (<-> ch th)(<-> ph (/\ ps (<-> th ta)))
ZeqReplaceBi1An1Bi0Zeq0 # <title> Substitution </title> # <table> # (<-> ph (/\ ps (<-> (z.= [ A ] ] ] C) ch))) # (z.= [ A ] [ B ] ) # (<-> ph (/\ ps (<-> (z.= [ [ [ B ] C) ch))) # </table>
(<-> ph (/\ ps (<-> (z.= A C) ch))) , (z.= A B)(<-> ph (/\ ps (<-> (z.= B C) ch)))
ZeqReplaceBi1An0Zeq0Mul0 # <title> Substitution </title> # <table> # (<-> ph (/\ (z.= (z.* [ A ] ] ] C) D) ps)) # (z.= [ A ] [ B ] ) # (<-> ph (/\ (z.= (z.* [ [ [ B ] C) D) ps)) # </table>
(<-> ph (/\ (z.= (z.* A C) D) ps)) , (z.= A B)(<-> ph (/\ (z.= (z.* B C) D) ps))
ZeqReplaceBi1An0Zeq0Mul1 # <title> Substitution </title> # <table> # (<-> ph (/\ (z.= (z.* A [ B ] ] ] ) D) ps)) # (z.= [ B ] [ C ] ) # (<-> ph (/\ (z.= (z.* A [ [ [ C ] ) D) ps)) # </table>
(<-> ph (/\ (z.= (z.* A B) D) ps)) , (z.= B C)(<-> ph (/\ (z.= (z.* A C) D) ps))
ZeqReplaceBi1An0Zeq1Mul0 # <title> Substitution </title> # <table> # (<-> ph (/\ (z.= A (z.* [ B ] ] ] D)) ps)) # (z.= [ B ] [ C ] ) # (<-> ph (/\ (z.= A (z.* [ [ [ C ] D)) ps)) # </table>
(<-> ph (/\ (z.= A (z.* B D)) ps)) , (z.= B C)(<-> ph (/\ (z.= A (z.* C D)) ps))
BiReplaceBi1An1Not0 # <title> Substitution </title> # <table> # (<-> ph (/\ ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (/\ ps (-. [ [ [ th ] ))) # </table>
(<-> ph (/\ ps (-. ch))) , (<-> ch th)(<-> ph (/\ ps (-. th)))
ZeqReplaceBi1An1Not0Zeq0 # <title> Substitution </title> # <table> # (<-> ph (/\ ps (-. (z.= [ A ] ] ] C)))) # (z.= [ A ] [ B ] ) # (<-> ph (/\ ps (-. (z.= [ [ [ B ] C)))) # </table>
(<-> ph (/\ ps (-. (z.= A C)))) , (z.= A B)(<-> ph (/\ ps (-. (z.= B C))))
BiReplaceBi1An1Bi1 # <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)))
ZeqReplaceBi1An1Bi1Zeq0 # <title> Substitution </title> # <table> # (<-> ph (/\ ps (<-> ch (z.= [ A ] ] ] C)))) # (z.= [ A ] [ B ] ) # (<-> ph (/\ ps (<-> ch (z.= [ [ [ B ] C)))) # </table>
(<-> ph (/\ ps (<-> ch (z.= A C)))) , (z.= A B)(<-> ph (/\ ps (<-> ch (z.= B C))))
fraceq # <title> Fraction Equality Formula </title>
(<-> (= (</> A B) (</> C D)) (/\ (z.= (z.* A D) (z.* C B)) (<-> (z.= B (z.0)) (z.= D (z.0)))))
(-> (z.= A B) (= (</> A C) (</> B C)))
(-> (z.= A B) (= (</> C A) (</> C B)))
(z.= A B)(= (</> A C) (</> B C))
(-> ph (z.= A B))(-> ph (= (</> A C) (</> B C)))
(z.= A B)(= (</> C A) (</> C B))
(-> ph (z.= A B))(-> ph (= (</> C A) (</> C B)))
fraczeq12 # <title> Equivalence for </> </title> ##
(-> (/\ (z.= A B) (z.= C D)) (= (</> A C) (</> B D)))
(z.= A (</> (top A) (bottom A)))
fracExpand # <suggest> left('Simplify', '/') </suggest>
(= A (</> (top A) (bottom A)))
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))
eqeqq # <title> Convert from Natural to Rational Equality </title>
(-> (z.= A B) (= A B))
eqeqqi # <title> Convert Natural to Rational Equality </title>
(z.= A B)(= A B)
eqeqqd # <title> Convert Natural to Rational Equality </title>
(-> ph (z.= A B))(-> ph (= A B))
tyex # <title> One-Digit Inequality </title>
(E. z (= z A))