# List of theorems

List of theorems in peano_new/arithmetic/rationals/division_min.gh:

df-al # <context> # This theorem is part of a series of proofs related to the # <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. This is the second part # in that process. The first part constructed the rationals from an ordered pair of integers. # However, it allows for the existence of NaN (not-a-number) which breaks several of the basic rules. # Now a new version of addition, multiplication, and equality are introduced which merges the number 0 # and the symbol NaN together, but the merging is done so that this number retains all the properties # of 0 and none of the properties of NaN. # </context> Briefly Add Back Predicate Calculus # <summary> # To be able to bind q.nat and nat we cannot import predicate because that would reintroduce nat. # So we have to prove everything in predicate_min from q. Here we redefine q.A. as A. # </summary>
(<-> (A. x ph) (q.A. x ph))
alnfi # <summary> Reproved for integers directly from the natural number versioq. </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 versioq. </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))
qexex # <title> Natural and Integer Existence are the same </title>
(<-> (q.E. x ph) (E. x ph))
df-r # <title> Definition of Remove NaN </title> # <summary> # This maps NaN to 0 and leaves everything else unchanged. # </summary> # <suggest> left('Simplify', '/') right('Define', '/') </suggest>
(q.= (r A) (q.ifn (q.= A (q.NaN)) (q.0) A))
(-> (q.= A B) (q.= (r A) (r B)))
(q.= A B)(q.= (r A) (r B))
(-> ph (q.= A B))(-> ph (q.= (r A) (r B)))
(-> (q.= A (q.NaN)) (q.= (r A) (q.0)))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
(-> (-. (q.= A (q.NaN))) (q.= (r A) A))
(-. (q.= (r A) (q.NaN)))
(q.= (r (q.0)) (q.0))
(q.= (r (q.1)) (q.1))
(<-> (= A B) (q.= (r A) (r B)))
eqid # <title> Reflexive Property </title>
(= A A)
eqcom # <title> Symmetric Property </title>
(<-> (= 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))
(E. x (= x A))
(-> (q.= A B) (= A B))
eqeqqi # <title> Convert Natural to Rational Equality </title>
(q.= A B)(= A B)
eqeqqd # <title> Convert Natural to Rational Equality </title>
(-> ph (q.= A B))(-> ph (= A B))
(q.= (r (r A)) (r A))
df-add # <title> Definition of Rational Addition </title> # <suggest> left('Simplify', '+') right('Define', '+') </suggest>
(q.= (+ A B) (q.+ (r A) (r B)))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
(-> (= A B) (= (+ A C) (+ B C)))
(-> (= A B) (= (+ C A) (+ C B)))
(= A B)(= (+ A C) (+ B C))
(-> ph (= A B))(-> ph (= (+ A C) (+ B C)))
(= A B)(= (+ C A) (+ C B))
addeq12 # <title> Equivalence for +q </title> ##
(-> (/\ (= A B) (= C D)) (= (+ A C) (+ B D)))
addeq12i # <table> # (= A ] ] ] [ B ] ] ) # (= [ [ C ] [ [ [ D) # (= (+ A ] [ C ] ) (+ [ B ] [ D)) # </table>
(= A B) , (= C D)(= (+ A C) (+ B D))
(-> ph (= A B))(-> ph (= (+ C A) (+ C B)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (+ A C) (+ B D)))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq1 # <title> Substitution </title> # <table> # (= A [ B ] ] ] ) # (= [ B ] [ C ] ) # (= A [ [ [ C ] ) # </table>
(= A B) , (= B C)(= A C)
(-> (/\ (-. (q.= A (q.NaN))) (-. (q.= B (q.NaN)))) (q.= (q.+ (r A) (r B)) (q.+ A B)))
QeqReplaceNot0Qeq0 # <title> Substitution </title> # <table> # (-. (q.= [ A ] ] ] C)) # (q.= [ A ] [ B ] ) # (-. (q.= [ [ [ B ] C)) # </table>
(-. (q.= A C)) , (q.= A B)(-. (q.= B C))
(-. (q.= (+ A B) (q.NaN)))
(q.= (r (+ A B)) (+ A B))
(q.= (r (+ B C)) (q.+ (r B) (r C)))
(= (+ A B) (+ B A))
(= (+ (+ A B) C) (+ A (+ B C)))
df-0 # <title> Definition of 0 </title>
(q.= (0) (q.0))
(q.= (r (0)) (0))
(= (+ A (0)) A)
df-1 # <title> Definition of 1 </title>
(q.= (1) (q.1))
(q.= (r (1)) (1))
df-mul # <title> Definition of Rational Multiplication </title>
(q.= (* A B) (q.* (r A) (r B)))
(-> (= A B) (= (* A C) (* B C)))
(-> (= A B) (= (* C A) (* C B)))
(= A B)(= (* A C) (* B C))
(-> ph (= A B))(-> ph (= (* A C) (* B C)))
(= A B)(= (* C A) (* C B))
(-> ph (= A B))(-> ph (= (* C A) (* C B)))
muleq12 # <title> Equivalence for *q </title> ##
(-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (* A C) (* B D)))
(-. (q.= (* A B) (q.NaN)))
(q.= (r (* A B)) (* A B))
(q.= (r (* B C)) (q.* (r B) (r C)))
(= (* A B) (* B A))
(= (* (* A B) C) (* A (* B C)))
(= (* A (1)) A)
(= (* A (+ B C)) (+ (* A B) (* A C)))
df-le # <title> Def. Less Than or Equal </title>
(<-> (<= A B) (q.<= (r A) (r B)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
(-> (= A B) (<-> (<= A C) (<= B C)))
(-> (= A B) (<-> (<= C A) (<= C B)))
(= A C)(<-> (<= A B) (<= C B))
(-> ph (= A C))(-> ph (<-> (<= A B) (<= C B)))
(= B C)(<-> (<= A B) (<= A C))
leeq12 # <title> Equivalence for <=q </title> ##
(-> (/\ (= A B) (= C D)) (<-> (<= A C) (<= B D)))
(-> ph (= B C))(-> ph (<-> (<= A B) (<= A C)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (<= A C) (<= B D)))
(<= A A)
QeqReplaceNot0Qeq1 # <title> Substitution </title> # <table> # (-. (q.= A [ B ] ] ] )) # (q.= [ B ] [ C ] ) # (-. (q.= A [ [ [ C ] )) # </table>
(-. (q.= A B)) , (q.= B C)(-. (q.= A C))
(-. (= (0) (1)))
QeqReplaceQle0 # <title> Substitution </title> # <table> # (q.<= [ A ] ] ] C) # (q.= [ A ] [ B ] ) # (q.<= [ [ [ B ] C) # </table>
(q.<= A C) , (q.= A B)(q.<= B C)
QeqReplaceQle1 # <title> Substitution </title> # <table> # (q.<= A [ B ] ] ] ) # (q.= [ B ] [ C ] ) # (q.<= A [ [ [ C ] ) # </table>
(q.<= A B) , (q.= B C)(q.<= A C)
(<= (0) (1))
QeqReplaceBi0Qeq0 # <title> Substitution </title> # <table> # (<-> (q.= [ A ] ] ] C) ph) # (q.= [ A ] [ B ] ) # (<-> (q.= [ [ [ B ] C) ph) # </table>
(<-> (q.= A C) ph) , (q.= A B)(<-> (q.= B C) ph)
QeqReplaceBi0Qeq1 # <title> Substitution </title> # <table> # (<-> (q.= A [ B ] ] ] ) ph) # (q.= [ B ] [ C ] ) # (<-> (q.= A [ [ [ C ] ) ph) # </table>
(<-> (q.= A B) ph) , (q.= B C)(<-> (q.= A C) ph)
(<-> (= (+ B A) (+ C A)) (= B C))
QeqReplaceImp1Bi0Qeq0 # <title> Substitution </title> # <table> # (-> ph (<-> (q.= [ A ] ] ] C) ps)) # (q.= [ A ] [ B ] ) # (-> ph (<-> (q.= [ [ [ B ] C) ps)) # </table>
(-> ph (<-> (q.= A C) ps)) , (q.= A B)(-> ph (<-> (q.= B C) ps))
QeqReplaceImp1Bi0Qeq1 # <title> Substitution </title> # <table> # (-> ph (<-> (q.= A [ B ] ] ] ) ps)) # (q.= [ B ] [ C ] ) # (-> ph (<-> (q.= A [ [ [ C ] ) ps)) # </table>
(-> ph (<-> (q.= A B) ps)) , (q.= B C)(-> ph (<-> (q.= A C) ps))
BiReplaceImp0An0Not0 # <title> Substitution </title> # <table> # (-> (/\ (-. [ ph ] ] ] ) ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ (-. [ [ [ ps ] ) ch) th) # </table>
(-> (/\ (-. ph) ch) th) , (<-> ph ps)(-> (/\ (-. ps) ch) th)
QeqReplaceImp0An0Not0Qeq1 # <title> Substitution </title> # <table> # (-> (/\ (-. (q.= A [ B ] ] ] )) ph) ps) # (q.= [ B ] [ C ] ) # (-> (/\ (-. (q.= A [ [ [ C ] )) ph) ps) # </table>
(-> (/\ (-. (q.= A B)) ph) ps) , (q.= B C)(-> (/\ (-. (q.= A C)) ph) ps)
QeqReplaceQeq0 # <title> Substitution </title> # <table> # (q.= [ A ] ] ] C) # (q.= [ A ] [ B ] ) # (q.= [ [ [ B ] C) # </table>
(q.= A C) , (q.= A B)(q.= B C)
QeqReplaceBi1Qeq1 # <title> Substitution </title> # <table> # (<-> ph (q.= A [ B ] ] ] )) # (q.= [ B ] [ C ] ) # (<-> ph (q.= A [ [ [ C ] )) # </table>
(<-> ph (q.= A B)) , (q.= B C)(<-> ph (q.= A C))
(-> (-. (= C (0))) (<-> (= (* A C) (* B C)) (= A B)))
df-neg # <title> Definition of Rational Negative </title> # <suggest> left('Simplify', '-') right('Define', '-') </suggest>
(q.= (-n A) (q.-n (r A)))
(-> (= A B) (= (-n A) (-n B)))
(-. (q.= (-n A) (q.NaN)))
(q.= (r (-n A)) (-n A))
QeqReplaceImp1Qeq0 # <title> Substitution </title> # <table> # (-> ph (q.= [ A ] ] ] C)) # (q.= [ A ] [ B ] ) # (-> ph (q.= [ [ [ B ] C)) # </table>
(-> ph (q.= A C)) , (q.= A B)(-> ph (q.= B C))
QeqReplaceImp1Qeq0Q.+1 # <title> Substitution </title> # <table> # (-> ph (q.= (q.+ A [ B ] ] ] ) D)) # (q.= [ B ] [ C ] ) # (-> ph (q.= (q.+ A [ [ [ C ] ) D)) # </table>
(-> ph (q.= (q.+ A B) D)) , (q.= B C)(-> ph (q.= (q.+ A C) D))
QeqReplaceQeq1 # <title> Substitution </title> # <table> # (q.= A [ B ] ] ] ) # (q.= [ B ] [ C ] ) # (q.= A [ [ [ C ] ) # </table>
(q.= A B) , (q.= B C)(q.= A C)
(= (+ A (-n A)) (0))
df-div # <title> Definition of Rational Division </title>
(q.= (/ A B) (q./ (r A) (r B)))
(-> (= A B) (= (/ A C) (/ B C)))
(-> (= A B) (= (/ C A) (/ C B)))
QeqReplaceImp0Not0Qeq1 # <title> Substitution </title> # <table> # (-> (-. (q.= A [ B ] ] ] )) ph) # (q.= [ B ] [ C ] ) # (-> (-. (q.= A [ [ [ C ] )) ph) # </table>
(-> (-. (q.= A B)) ph) , (q.= B C)(-> (-. (q.= A C)) ph)
QeqReplaceImp1Not0Qeq0 # <title> Substitution </title> # <table> # (-> ph (-. (q.= [ A ] ] ] C))) # (q.= [ A ] [ B ] ) # (-> ph (-. (q.= [ [ [ B ] C))) # </table>
(-> ph (-. (q.= A C))) , (q.= A B)(-> ph (-. (q.= B C)))
(-> (-. (= B (0))) (-. (q.= (/ A B) (q.NaN))))
(-> (-. (= B (0))) (q.= (r (/ A B)) (/ A B)))
(-> (-. (= B (0))) (q.= (r (/ A B)) (q./ (r A) (r B))))
QeqReplaceImp1Qeq0Q.*1 # <title> Substitution </title> # <table> # (-> ph (q.= (q.* A [ B ] ] ] ) D)) # (q.= [ B ] [ C ] ) # (-> ph (q.= (q.* A [ [ [ C ] ) D)) # </table>
(-> ph (q.= (q.* A B) D)) , (q.= B C)(-> ph (q.= (q.* A C) D))
QeqReplaceImp1Qeq1 # <title> Substitution </title> # <table> # (-> ph (q.= A [ B ] ] ] )) # (q.= [ B ] [ C ] ) # (-> ph (q.= A [ [ [ C ] )) # </table>
(-> ph (q.= A B)) , (q.= B C)(-> ph (q.= A C))
BiReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (<-> ch th)(-> ph (/\ ps th))
QeqReplaceImp1Qeq0R0 # <title> Substitution </title> # <table> # (-> ph (q.= (r [ A ] ] ] ) C)) # (q.= [ A ] [ B ] ) # (-> ph (q.= (r [ [ [ B ] ) C)) # </table>
(-> ph (q.= (r A) C)) , (q.= A B)(-> ph (q.= (r B) C))
(-> (-. (= B (0))) (= (* B (/ A B)) A))
diveq12 # <title> Equivalence for / </title> ##
(-> (/\ (= A B) (= C D)) (= (/ A C) (/ B D)))
(T)