# List of theorems

List of theorems in peano/rationals.gh:

ZeqReplaceImp1Zeq0 # <context> # This theorem is part of a series of theorems that construct the rational numbers using # integers. We are in the process of reorganizing the theorems and grouping them into # smaller files that concern one specific topic. This theorem should have been moved into # the peano_new/arithmetic/rationals directory. # </context> # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (=z A C)) , (=z A B)(-> ph (=z B C))
ZeqReplaceImp1Zeq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= 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>
topop # <title> Apply top to ordered pair </title> # <summary> # The top operation grabs the first number in an ordered pair, just like # head. # </summary>
(=z (top (<,> A B)) A)
topeq # <title> Equivalence for numerator </title>
(-> (= A B) (=z (top A) (top B)))
(= A B)(=z (top A) (top B))
(-> ph (= A B))(-> ph (=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>
(= (bottom A) (tail A))
bottomop # <title> Apply bottom to ordered pair </title> # <summary> # The bottom operation grabs the second number in an ordered pair, just like # tail. # </summary>
(=z (bottom (<,> A B)) B)
bottomeq # <title> Equivalence for denominator </title>
(-> (= A B) (=z (bottom A) (bottom B)))
(= A B)(=z (bottom A) (bottom B))
(-> ph (= A B))(-> ph (=z (bottom A) (bottom B)))
(=_ ({|} x (-. (=z (bottom x) (0z)))) ({|} y (-. (=z (bottom y) (0z)))))
df-rationals # <title> Set of Rational Numbers Definition </title> # <summary> # Rationals Numbers can never divide by 0. Otherwise, a rational # number is an ordered pair with the second number as the # denominator. # </summary>
(=_ (rationals) ({|} y (-. (=z (bottom y) (0z)))))
SeqReplaceBi0El1 # <title> Substitution </title> # <table> # (<-> (e. A [ S ] ] ] ) ph) # (=_ [ S ] [ T ] ) # (<-> (e. A [ [ [ T ] ) ph) # </table>
(<-> (e. A S) ph) , (=_ S T)(<-> (e. A T) ph)
bottomNot0 # <title> The denominator is never 0 </title>
(<-> (e. A (rationals)) (-. (=z (bottom A) (0z))))
df-eqq # <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>
(<-> (=q A B) (/\ (=z (*z (top A) (bottom B)) (*z (top B) (bottom A))) (<-> (=z (bottom A) (0z)) (=z (bottom B) (0z)))))
dfeqq1 # <title> Part of the Rational Equality Definition </title>
(-> (=q A B) (=z (*z (top A) (bottom B)) (*z (top B) (bottom A))))
dfeqq2 # <title> Part of the Rational Equality Definition </title>
(-> (=q A B) (<-> (=z (bottom A) (0z)) (=z (bottom B) (0z))))
eqqid # <title> Reflexive Property </title>
(=q 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))
eqqcom # <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>
(<-> (=q A B) (=q B A))
eqqcomi # <title> Symmetric Property </title> # <table> # (=z <r> A <g> B) # (=z <g> B <r> A) # </table>
(=q A B)(=q 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))
(-> (/\ (=q A B) (=q B C)) (<-> (=z (bottom A) (0z)) (=z (bottom C) (0z))))
eqqtr.1 # <title> First Part of Transitivity Proof </title>
(-> (=q A B) (-> (/\ (=z (top B) (0z)) (-. (=z (bottom B) (0z)))) (=z (top A) (0z))))
BiReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
BiReplaceImp1Imp0 # <title> Substitution </title> # <table> # (-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (-> [ [ [ ch ] th)) # </table>
(-> ph (-> ps th)) , (<-> ps ch)(-> ph (-> ch 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) (0z)) (-. (=z (bottom B) (0z)))) (-> (/\ (=q A B) (=q B C)) (=q A C)))
(-> (/\ (=z (bottom B) (0z)) (=q A B)) (=z (bottom A) (0z)))
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) (0z)) (-> (/\ (=q A B) (=q B C)) (=q 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) (0z))) (-. (=z (top B) (0z)))) (-> (/\ (=q A B) (=q B C)) (=q A C)))
eqqtr # <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>
(-> (/\ (=q A B) (=q B C)) (=q A C))
(-> (=q A B) (<-> (=q A C) (=q B C)))
eqqeqq2 # <title> Equivalence over Equality </title>
(-> (=q A B) (<-> (=q C A) (=q C B)))
(=q A B)(<-> (=q A C) (=q B C))
(-> ph (=q A B))(-> ph (<-> (=q A C) (=q B C)))
(=q A B)(<-> (=q C A) (=q C B))
(-> ph (=q A B))(-> ph (<-> (=q C A) (=q C B)))
eqqeqq12d # <title> Transitive Property </title>
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (<-> (=q A C) (=q B D)))
eqqtrd # <title> Transitive Property </title>
(-> ph (=q A B)) , (-> ph (=q B C))(-> ph (=q A C))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
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>
(= (</> A B) (<,> 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))
ZeqReplaceBi1Zeq0Zmul1 # <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))
EqReplaceEq1Op0 # <title> Substitution </title> # <table> # (= A (<,> [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (<,> [ [ [ C ] D)) # </table>
(= A (<,> B D)) , (= B C)(= A (<,> 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))
ZeqReplaceBi1An0Zeq1Zmul1 # <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)))
ZeqReplaceBi1An0Zeq0Zmul0 # <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))
ZeqReplaceBi1An0Zeq0Zmul1 # <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))
ZeqReplaceBi1An0Zeq1Zmul0 # <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))))
fraceqq # <title> Fraction Equality Formula </title>
(<-> (=q (</> A B) (</> C D)) (/\ (=z (*z A D) (*z C B)) (<-> (=z B (0z)) (=z D (0z)))))
(-> (=z A B) (=q (</> A C) (</> B C)))
(-> (=z A B) (=q (</> C A) (</> C B)))
(=z A B)(=q (</> A C) (</> B C))
(-> ph (=z A B))(-> ph (=q (</> A C) (</> B C)))
(=z A B)(=q (</> C A) (</> C B))
(-> ph (=z A B))(-> ph (=q (</> C A) (</> C B)))
fraczeq12 # <title> Equivalence for </> </title> ##
(-> (/\ (=z A B) (=z C D)) (=q (</> A C) (</> B D)))
(= A (</> (top A) (bottom A)))
fracExpand # <suggest> left('Simplify', '/') </suggest>
(=q A (</> (top A) (bottom A)))
df-0q # <title> Definition of 0 as a Fraction </title>
(=q (0q) (</> (0z) (1z)))
df-1q # <title> Definition of 1 as a Fraction </title>
(=q (1q) (</> (1z) (1z)))
ZeqReplaceZeq1 # <title> Substitution </title> # <table> # (=z A [ B ] ] ] ) # (=z [ B ] [ C ] ) # (=z A [ [ [ C ] ) # </table>
(=z A B) , (=z B C)(=z A C)
ZeqReplaceZeq1Zmul0 # <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))
ZeqReplaceBi1Zeq1Zmul0 # <title> Substitution </title> # <table> # (<-> ph (=z A (*z [ B ] ] ] D))) # (=z [ B ] [ C ] ) # (<-> ph (=z A (*z [ [ [ C ] D))) # </table>
(<-> ph (=z A (*z B D))) , (=z B C)(<-> ph (=z A (*z C D)))
top0 # <title> Numerator of 0 is 0 </title>
(=z (top (0q)) (0z))
ZeqReplaceImp1Bi1Zeq0 # <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)))
proveRational # <title> Rational has a nonzero denominator </title>
(-> (/\ (=q A (</> B C)) (-. (=z C (0z)))) (e. A (rationals)))
0rational # <title> 0 is rational </title>
(e. (0q) (rationals))
1rational # <title> 1 is rational </title>
(e. (1q) (rationals))
(=q (</> (0z) (0z)) (</> A (0z)))
df-NaN # <title> Definition of Not a Number </title> # <summary> # Definition of Not a Number which is the result when you divide any # number by 0. # </summary>
(=q (NaN) (</> x (0z)))
QeqReplaceQeq1 # <title> Substitution </title> # <table> # (=q A [ B ] ] ] ) # (=q [ B ] [ C ] ) # (=q A [ [ [ C ] ) # </table>
(=q A B) , (=q B C)(=q A C)
dfNaN # <title> Definition of Not a Number </title> # <summary> Definition of Not a Number # The difference between this theorem and the <a href="df-NaN">original definition</a> # is that this theorem uses an arbitrary variable A, not a binding variable x. # </summary>
(=q (NaN) (</> A (0z)))
bottomNaN # <title> Denominator of NaN is 0 </title>
(=z (bottom (NaN)) (0z))
QeqReplaceImp0Qeq1 # <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)
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))
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))
bottomNaN2 # <title> Denominator of NaN is 0 </title>
(<-> (=z (bottom A) (0z)) (=q A (NaN)))
irrationalNaN # <title> A non-number is not Rational </title>
(-. (e. (NaN) (rationals)))
irrationalNaN2 # <title> A non-number is not Rational </title>
(<-> (-. (e. A (rationals))) (=q A (NaN)))
df-qmul # <title> Definition of Rational Multiplication </title> # <suggest> left('Simplify', '∙') right('Define', '∙') </suggest> # <summary> # See <a href="qmulfrac">qmulfrac</a> for a restatement of # integer multiplication using ordered pairs and integer equality. # </summary>
(=q (*q A B) (</> (*z (top A) (top B)) (*z (bottom A) (bottom B))))
qmulcom # <title> Commutative Property of Multiplication </title> # <table> (=z (*z <r> A <g> B) (*z <g> B <r> A)) </table> # <suggest> right('Commute', '∙') </suggest> # <summary> # Rational number multiplication is defined using integer multiplication. # Use the commutative property of integer multiplication to show that # rational number multiplication has the same property. # For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. # </summary>
(=q (*q A B) (*q B A))
ZeqReplaceQeq1Frac0 # <title> Substitution </title> # <table> # (=q A (</> [ B ] ] ] D)) # (=z [ B ] [ C ] ) # (=q A (</> [ [ [ C ] D)) # </table>
(=q A (</> B D)) , (=z B C)(=q A (</> C D))
ZeqReplaceQeq1Frac0Zmul0 # <title> Substitution </title> # <table> # (=q A (</> (*z [ B ] ] ] D) A')) # (=z [ B ] [ C ] ) # (=q A (</> (*z [ [ [ C ] D) A')) # </table>
(=q A (</> (*z B D) A')) , (=z B C)(=q A (</> (*z C D) A'))
ZeqReplaceQeq1Frac0Zmul1 # <title> Substitution </title> # <table> # (=q A (</> (*z B [ C ] ] ] ) A')) # (=z [ C ] [ D ] ) # (=q A (</> (*z B [ [ [ D ] ) A')) # </table>
(=q A (</> (*z B C) A')) , (=z C D)(=q A (</> (*z B D) A'))
ZeqReplaceQeq1Frac1 # <title> Substitution </title> # <table> # (=q A (</> B [ C ] ] ] )) # (=z [ C ] [ D ] ) # (=q A (</> B [ [ [ D ] )) # </table>
(=q A (</> B C)) , (=z C D)(=q A (</> B D))
ZeqReplaceQeq1Frac1Zmul0 # <title> Substitution </title> # <table> # (=q A (</> B (*z [ C ] ] ] A'))) # (=z [ C ] [ D ] ) # (=q A (</> B (*z [ [ [ D ] A'))) # </table>
(=q A (</> B (*z C A'))) , (=z C D)(=q A (</> B (*z D A')))
ZeqReplaceQeq1Frac1Zmul1 # <title> Substitution </title> # <table> # (=q A (</> B (*z C [ D ] ] ] ))) # (=z [ D ] [ A' ] ) # (=q A (</> B (*z C [ [ [ A' ] ))) # </table>
(=q A (</> B (*z C D))) , (=z D A')(=q A (</> B (*z C A')))
qmulfrac # <title> Multiply Fractions </title> # <suggest> right('Equivalence', '∙') </suggest>
(=q (*q (</> A B) (</> C D)) (</> (*z A C) (*z B D)))
bottomQmul # <title> Multiplication Denominator Formula </title>
(<-> (=z (bottom (*q A B)) (0z)) (=z (*z (bottom A) (bottom B)) (0z)))
bottomZeroProduct # <title> Denominator Zero Product Property </title>
(<-> (-. (=z (*z (bottom A) (bottom B)) (0z))) (/\ (e. A (rationals)) (e. B (rationals))))
qmulClosure # <title> Closure of rationals under multiplication </title>
(<-> (e. (*q A B) (rationals)) (/\ (e. A (rationals)) (e. B (rationals))))
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)
(<-> (=q (*q A B) (*q C B)) (/\ (=z (*z (*z (top A) (top B)) (*z (bottom C) (bottom B))) (*z (*z (top C) (top B)) (*z (bottom A) (bottom B)))) (<-> (=z (*z (bottom A) (bottom B)) (0z)) (=z (*z (bottom C) (bottom B)) (0z)))))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
BiReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (<-> ps ch)(-> ph (/\ ch th))
ZeqReplaceImp1An0Zeq0 # <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))
ZeqReplaceImp1An0Zeq0Zmul0 # <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))
ZeqReplaceImp1An0Zeq1 # <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))
ZeqReplaceImp1An0Zeq1Zmul0 # <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))
(-> (=q A C) (=q (*q A B) (*q C B)))
(-> (=q A B) (=q (*q C A) (*q C B)))
(=q A B)(=q (*q A C) (*q B C))
(-> ph (=q A B))(-> ph (=q (*q A C) (*q B C)))
(=q A B)(=q (*q C A) (*q C B))
(-> ph (=q A B))(-> ph (=q (*q C A) (*q C B)))
qmuleqq12 # <title> Equivalence for *q </title> ##
(-> (/\ (=q A B) (=q C D)) (=q (*q A C) (*q B D)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (=q (*q A C) (*q B D)))
qmulNaN # <title> Multiplying Not a Number </title>
(=q (*q A (NaN)) (NaN))
QeqReplaceQeq0 # <title> Substitution </title> # <table> # (=q [ A ] ] ] C) # (=q [ A ] [ B ] ) # (=q [ [ [ B ] C) # </table>
(=q A C) , (=q A B)(=q B C)
(=q (*q (NaN) A) (NaN))
qmuleqq12i # <title> Equality over Multiplication </title> # <table> # (=q A ] ] ] [ B ] ] ) # (=q [ [ C ] [ [ [ D) # (=q (*q A ] [ C ] ) (*q [ B ] [ D)) # </table>
(=q A B) , (=q C D)(=q (*q A C) (*q B D))
QeqReplaceQeq1Qmul0 # <title> Substitution </title> # <table> # (=q A (*q [ B ] ] ] D)) # (=q [ B ] [ C ] ) # (=q A (*q [ [ [ C ] D)) # </table>
(=q A (*q B D)) , (=q B C)(=q A (*q C D))
QeqReplaceQeq1Qmul1 # <title> Substitution </title> # <table> # (=q A (*q B [ C ] ] ] )) # (=q [ C ] [ D ] ) # (=q A (*q B [ [ [ D ] )) # </table>
(=q A (*q B C)) , (=q C D)(=q A (*q B D))
QeqReplaceQeq1Qmul1Qmul0 # <title> Substitution </title> # <table> # (=q A (*q B (*q [ C ] ] ] A'))) # (=q [ C ] [ D ] ) # (=q A (*q B (*q [ [ [ D ] A'))) # </table>
(=q A (*q B (*q C A'))) , (=q C D)(=q A (*q B (*q D A')))
QeqReplaceQeq1Qmul1Qmul1 # <title> Substitution </title> # <table> # (=q A (*q B (*q C [ D ] ] ] ))) # (=q [ D ] [ A' ] ) # (=q A (*q B (*q C [ [ [ A' ] ))) # </table>
(=q A (*q B (*q C D))) , (=q D A')(=q A (*q B (*q C A')))
qmulass # <title> Associative Property of Rational Multiplication </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=q (*q (*q A B) C) (*q A (*q B C)))
qmulid # <title> Rational Multiplication Identity </title> # <summary> 1 is the identity for rational multiplication. </summary> # <suggest> right('Simplify','1') </suggest>
(=q (*q A (1q)) A)
qmulidr # <title> Rational Multiplication Identity </title> # <summary> 1 is the identity for rational multiplication. </summary> # <suggest> right('Simplify','1') </suggest>
(=q (*q (1q) A) A)
df-qadd # <title> Definition of Rational Multiplication </title> # <suggest> left('Simplify', '+') right('Define', '+') </suggest> # <summary> # See <a href="qaddfrac">qaddfrac</a> for a restatement of # integer multiplication using ordered pairs and integer equality. # </summary>
(=q (+q A B) (</> (+z (*z (top A) (bottom B)) (*z (top B) (bottom A))) (*z (bottom A) (bottom B))))
ZeqReplaceQeq1Frac0Zadd0 # <title> Substitution </title> # <table> # (=q A (</> (+z [ B ] ] ] D) A')) # (=z [ B ] [ C ] ) # (=q A (</> (+z [ [ [ C ] D) A')) # </table>
(=q A (</> (+z B D) A')) , (=z B C)(=q A (</> (+z C D) A'))
ZeqReplaceQeq1Frac0Zadd0Zmul0 # <title> Substitution </title> # <table> # (=q A (</> (+z (*z [ B ] ] ] D) A') B')) # (=z [ B ] [ C ] ) # (=q A (</> (+z (*z [ [ [ C ] D) A') B')) # </table>
(=q A (</> (+z (*z B D) A') B')) , (=z B C)(=q A (</> (+z (*z C D) A') B'))
ZeqReplaceQeq1Frac0Zadd0Zmul1 # <title> Substitution </title> # <table> # (=q A (</> (+z (*z B [ C ] ] ] ) A') B')) # (=z [ C ] [ D ] ) # (=q A (</> (+z (*z B [ [ [ D ] ) A') B')) # </table>
(=q A (</> (+z (*z B C) A') B')) , (=z C D)(=q A (</> (+z (*z B D) A') B'))
ZeqReplaceQeq1Frac0Zadd1 # <title> Substitution </title> # <table> # (=q A (</> (+z B [ C ] ] ] ) A')) # (=z [ C ] [ D ] ) # (=q A (</> (+z B [ [ [ D ] ) A')) # </table>
(=q A (</> (+z B C) A')) , (=z C D)(=q A (</> (+z B D) A'))
ZeqReplaceQeq1Frac0Zadd1Zmul0 # <title> Substitution </title> # <table> # (=q A (</> (+z B (*z [ C ] ] ] A')) B')) # (=z [ C ] [ D ] ) # (=q A (</> (+z B (*z [ [ [ D ] A')) B')) # </table>
(=q A (</> (+z B (*z C A')) B')) , (=z C D)(=q A (</> (+z B (*z D A')) B'))
ZeqReplaceQeq1Frac0Zadd1Zmul1 # <title> Substitution </title> # <table> # (=q A (</> (+z B (*z C [ D ] ] ] )) B')) # (=z [ D ] [ A' ] ) # (=q A (</> (+z B (*z C [ [ [ A' ] )) B')) # </table>
(=q A (</> (+z B (*z C D)) B')) , (=z D A')(=q A (</> (+z B (*z C A')) B'))
qaddfrac # <suggest> right('Equivalence', '+') </suggest>
(=q (+q (</> A B) (</> C D)) (</> (+z (*z A D) (*z C B)) (*z B D)))
qaddcom # <title> Commutative Property of Rational Addition </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. </summary> # <table> (=q (+q <r> A <g> B) (+q <g> B <r> A)) </table> # <suggest> right('Commute', '+') </suggest>
(=q (+q A B) (+q B A))
(<-> (=q (+q A B) (+q C B)) (/\ (=z (*z (+z (*z (top A) (bottom B)) (*z (top B) (bottom A))) (*z (bottom C) (bottom B))) (*z (+z (*z (top C) (bottom B)) (*z (top B) (bottom C))) (*z (bottom A) (bottom B)))) (<-> (=z (*z (bottom A) (bottom B)) (0z)) (=z (*z (bottom C) (bottom B)) (0z)))))
(-> (=q A C) (=q (+q A B) (+q C B)))
(-> (=q A B) (=q (+q C A) (+q C B)))
(=q A B)(=q (+q A C) (+q B C))
(-> ph (=q A B))(-> ph (=q (+q A C) (+q B C)))
(=q A B)(=q (+q C A) (+q C B))
qaddeqq12 # <title> Equivalence for +q </title> ##
(-> (/\ (=q A B) (=q C D)) (=q (+q A C) (+q B D)))
qaddeqq12i # <table> # (=q A ] ] ] [ B ] ] ) # (=q [ [ C ] [ [ [ D) # (=q (+q A ] [ C ] ) (+q [ B ] [ D)) # </table>
(=q A B) , (=q C D)(=q (+q A C) (+q B D))
(-> ph (=q A B))(-> ph (=q (+q C A) (+q C B)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (=q (+q A C) (+q B D)))
(=q (+q A (NaN)) (NaN))
(=q (+q (NaN) A) (NaN))
(<-> (=z (bottom (+q A B)) (0z)) (=z (*z (bottom A) (bottom B)) (0z)))
(<-> (e. (+q A B) (rationals)) (/\ (e. A (rationals)) (e. B (rationals))))
QeqReplaceQeq1Qadd0 # <title> Substitution </title> # <table> # (=q A (+q [ B ] ] ] D)) # (=q [ B ] [ C ] ) # (=q A (+q [ [ [ C ] D)) # </table>
(=q A (+q B D)) , (=q B C)(=q A (+q C D))
QeqReplaceQeq1Qadd1 # <title> Substitution </title> # <table> # (=q A (+q B [ C ] ] ] )) # (=q [ C ] [ D ] ) # (=q A (+q B [ [ [ D ] )) # </table>
(=q A (+q B C)) , (=q C D)(=q A (+q B D))
ZeqReplaceQeq1Frac0Zadd0Zadd0 # <title> Substitution </title> # <table> # (=q A (</> (+z (+z [ B ] ] ] D) A') B')) # (=z [ B ] [ C ] ) # (=q A (</> (+z (+z [ [ [ C ] D) A') B')) # </table>
(=q A (</> (+z (+z B D) A') B')) , (=z B C)(=q A (</> (+z (+z C D) A') B'))
ZeqReplaceZeq1Zmul1 # <title> Substitution </title> # <table> # (=z A (*z B [ C ] ] ] )) # (=z [ C ] [ D ] ) # (=z A (*z B [ [ [ D ] )) # </table>
(=z A (*z B C)) , (=z C D)(=z A (*z B D))
ZeqReplaceQeq1Frac0Zadd0Zadd1 # <title> Substitution </title> # <table> # (=q A (</> (+z (+z B [ C ] ] ] ) A') B')) # (=z [ C ] [ D ] ) # (=q A (</> (+z (+z B [ [ [ D ] ) A') B')) # </table>
(=q A (</> (+z (+z B C) A') B')) , (=z C D)(=q A (</> (+z (+z B D) A') B'))
qaddass # <title> Associative Property of Rational Addition </title> # <summary> For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=q (+q (+q A B) C) (+q A (+q B C)))
(=q (+q A (0q)) A)
qequivalence # <title> Rational Number Equivalence Class </title>
(-> (-. (=z A (0z))) (=q (</> (*z A B) (*z A C)) (</> B C)))
ZeqReplaceImp1Qeq1Frac0 # <title> Substitution </title> # <table> # (-> ph (=q A (</> [ B ] ] ] D))) # (=z [ B ] [ C ] ) # (-> ph (=q A (</> [ [ [ C ] D))) # </table>
(-> ph (=q A (</> B D))) , (=z B C)(-> ph (=q A (</> C D)))
ZeqReplaceImp1Qeq1Frac0Zadd0 # <title> Substitution </title> # <table> # (-> ph (=q A (</> (+z [ B ] ] ] D) A'))) # (=z [ B ] [ C ] ) # (-> ph (=q A (</> (+z [ [ [ C ] D) A'))) # </table>
(-> ph (=q A (</> (+z B D) A'))) , (=z B C)(-> ph (=q A (</> (+z C D) A')))
ZeqReplaceImp1Qeq1Frac0Zadd1 # <title> Substitution </title> # <table> # (-> ph (=q A (</> (+z B [ C ] ] ] ) A'))) # (=z [ C ] [ D ] ) # (-> ph (=q A (</> (+z B [ [ [ D ] ) A'))) # </table>
(-> ph (=q A (</> (+z B C) A'))) , (=z C D)(-> ph (=q A (</> (+z B D) A')))
ZeqReplaceImp1Qeq1Frac1 # <title> Substitution </title> # <table> # (-> ph (=q A (</> B [ C ] ] ] ))) # (=z [ C ] [ D ] ) # (-> ph (=q A (</> B [ [ [ D ] ))) # </table>
(-> ph (=q A (</> B C))) , (=z C D)(-> ph (=q A (</> B D)))
qdistrNaN # <title> Distributive Property for NaN </title> # <summary> # The distributive property hold for not-a-number (NaN) because multiplying # and adding by NaN results in NaN in both cases. # </summary>
(-> (-. (e. A (rationals))) (=q (+q (*q A B) (*q A C)) (*q A (+q B C))))
qdistr # <title> Distributive Property </title> # <summary> # Distribution of rational addition through multiplication. # See <a href="qdistl">qdistl</a> for distribution in the opposite direction. # For more information see the <a href="/wiki/peano/arithmetic/rationals">construction of the rationals</a>. # </summary> # <table> # (=z (+z (*z <c> A B) (*z <c> A C)) (*z <c> A (+z B C))) # </table> # <suggest> right('Distribute', '-R') left('Distribute', 'R') </suggest>
(=q (+q (*q A B) (*q A C)) (*q A (+q B C)))
QeqReplaceQeq0Qadd0 # <title> Substitution </title> # <table> # (=q (+q [ A ] ] ] C) D) # (=q [ A ] [ B ] ) # (=q (+q [ [ [ B ] C) D) # </table>
(=q (+q A C) D) , (=q A B)(=q (+q B C) D)
QeqReplaceQeq0Qadd1 # <title> Substitution </title> # <table> # (=q (+q A [ B ] ] ] ) D) # (=q [ B ] [ C ] ) # (=q (+q A [ [ [ C ] ) D) # </table>
(=q (+q A B) D) , (=q B C)(=q (+q A C) D)
qdistl # <title> Distributive Property </title> # <summary> # Distribution of rational addition through multiplication. # See <a href="qdistr">qdistr</a> for distribution in the opposite direction. # </summary> # <table> # (=z (+z (*z B <c> A) (*z C <c> A)) (*z (+z B C) <c> A)) # </table> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(=q (+q (*q B A) (*q C A)) (*q (+q B C) A))
df-qneg # <title> Definition of Negative </title> # <summary> # This is the unary negative sign for rational numbers, not to be confused with # binary <a href="df-minus">subtraction</a> which is defined using the negative sign. # The negative is defined by negating the numerator. See # <a href="/peano/integers.gh/df-neg">df-neg</a> for the integer version. # </summary>
(=q (-qn A) (</> (-n (top A)) (bottom A)))
(<-> (=q (-qn A) (-qn B)) (=q A B))
(-> (=q A B) (=q (-qn A) (-qn B)))
(=q A B)(=q (-qn A) (-qn B))
(-> ph (=q A B))(-> ph (=q (-qn A) (-qn B)))
ZeqReplaceQeq1Frac0Neg0 # <title> Substitution </title> # <table> # (=q A (</> (-n [ B ] ] ] ) D)) # (=z [ B ] [ C ] ) # (=q A (</> (-n [ [ [ C ] ) D)) # </table>
(=q A (</> (-n B) D)) , (=z B C)(=q A (</> (-n C) D))
negfrac # <title> Negative Applied to a Fraction </title>
(=q (-qn (</> A B)) (</> (-n A) B))
doubleqneg # <title> Double Negative </title>
(=q (-qn (-qn A)) A)
QeqReplaceQeq0Qneg0 # <title> Substitution </title> # <table> # (=q (-qn [ A ] ] ] ) C) # (=q [ A ] [ B ] ) # (=q (-qn [ [ [ B ] ) C) # </table>
(=q (-qn A) C) , (=q A B)(=q (-qn B) C)
qneg0 # <title> Negative of 0 is 0 </title> # <suggest> right('Simplify', '-') </suggest>
(=q (-qn (0q)) (0q))
ZeqReplaceImp1Qeq0Frac0 # <title> Substitution </title> # <table> # (-> ph (=q (</> [ A ] ] ] C) D)) # (=z [ A ] [ B ] ) # (-> ph (=q (</> [ [ [ B ] C) D)) # </table>
(-> ph (=q (</> A C) D)) , (=z A B)(-> ph (=q (</> B C) D))
ZeqReplaceImp1Qeq0Frac1 # <title> Substitution </title> # <table> # (-> ph (=q (</> A [ B ] ] ] ) D)) # (=z [ B ] [ C ] ) # (-> ph (=q (</> A [ [ [ C ] ) D)) # </table>
(-> ph (=q (</> A B) D)) , (=z B C)(-> ph (=q (</> A C) D))
qnegClosure # <title> Closure of rationals under negation </title>
(<-> (e. (-qn A) (rationals)) (e. A (rationals)))
qequivalence0 # <title> 0 equals any number with 0 in numerator </title>
(-> (-. (=z A (0z))) (=q (</> (0z) A) (0q)))
qequivalence1 # <title> Equivalence Class for 1 </title>
(-> (-. (=z A (0z))) (=q (</> A A) (1q)))
(<-> (=q A (0q)) (/\ (=z (top A) (0z)) (-. (=z (bottom A) (0z)))))
df-qminus # <title> Definition of Subtraction </title> # <summary> # This is the binary subtraction operation, not to be confused with the # unary <a href="df-qneg">negative sign</a> which is used in the definition. # </summary> # <suggest> left('Simplify', '-') right('Define', '-') </suggest>
(=q (-q A B) (+q A (-qn B)))
qminuseqq1 # <title> Equivalence for -q </title> ##
(-> (=q A C) (=q (-q A B) (-q C B)))
(=q A C)(=q (-q A B) (-q C B))
qminuseqq2 # <title> Equivalence for -q </title> ##
(-> (=q B C) (=q (-q A B) (-q A C)))
(-> ph (=q A C))(-> ph (=q (-q A B) (-q C B)))
(=q B C)(=q (-q A B) (-q A C))
qminuseqq12 # <title> Equivalence for -q </title> ##
(-> (/\ (=q A B) (=q C D)) (=q (-q A C) (-q B D)))
(-> ph (=q B C))(-> ph (=q (-q A B) (-q A C)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (=q (-q A C) (-q B D)))
(=q (-q (</> A B) (</> C D)) (</> (- (*z A D) (*z C B)) (*z B D)))
QeqReplaceQeq0Qminus0 # <title> Substitution </title> # <table> # (=q (-q [ A ] ] ] C) D) # (=q [ A ] [ B ] ) # (=q (-q [ [ [ B ] C) D) # </table>
(=q (-q A C) D) , (=q A B)(=q (-q B C) D)
QeqReplaceQeq0Qminus1 # <title> Substitution </title> # <table> # (=q (-q A [ B ] ] ] ) D) # (=q [ B ] [ C ] ) # (=q (-q A [ [ [ C ] ) D) # </table>
(=q (-q A B) D) , (=q B C)(=q (-q A C) D)
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
qaddcan # <title> Cancel using Subtraction </title>
(-> (e. A (rationals)) (=q (-q A A) (0q)))
qaddcan2 # <title> Cancel using Subtraction </title>
(-> (/\ (=q A B) (e. B (rationals))) (=q (-q A B) (0q)))
qminusid # <title> Subtraction Identity </title> # <suggest> right('Simplify', '-') </suggest>
(=q (-q A (0q)) A)
qmulhomomorph # <summary> # Division by 1 is a homomorphism respecting <a href="df-qmul">multiplication</a>. # </summary>
(=q (*q (</> A (1z)) (</> B (1z))) (</> (*z A B) (1z)))
(=q (+q (</> A (1z)) (</> B (1z))) (</> (+z A B) (1z)))
eqeqq # <title> Convert from Natural to Rational Equality </title>
(-> (= A B) (=q A B))
eqeqqi # <title> Convert Natural to Rational Equality </title>
(= A B)(=q A B)
eqeqqd # <title> Convert Natural to Rational Equality </title>
(-> ph (= A B))(-> ph (=q A B))
(-> (=q A C) (=q (ifn ph A B) (ifn ph C B)))
(-> (=q A C) (=q (ifn ph B A) (ifn ph B C)))
df-qdiv # <title> Definition of Division </title> # <summary> # Division is defined by multiplying a number with its numerator and denominator reversed. # NaN needs to be treated as a special case since it represents x/0 for any arbitrary value of x. # Reversing the numerator and denominator in this case might result in the number 0 when x is nonzero # or in the number 0/0 when x is zero. For division to be well-defined we treat NaN as a special # case that always returns NaN. # </summary> # <suggest> left('Simplify', '/') right('Define', '/') </suggest>
(=q (/ A B) (ifn (e. B (rationals)) (*q A (</> (bottom B) (top B))) (NaN)))
(-> (=q A C) (=q (/ A B) (/ C B)))
BiReplaceImp0An1Not0 # <title> Substitution </title> # <table> # (-> (/\ ph (-. [ ps ] ] ] )) th) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph (-. [ [ [ ch ] )) th) # </table>
(-> (/\ ph (-. ps)) th) , (<-> ps ch)(-> (/\ ph (-. ch)) th)
BiReplaceImp0An0 # <title> Substitution </title> # <table> # (-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ [ [ [ ps ] ch) th) # </table>
(-> (/\ ph ch) th) , (<-> ph ps)(-> (/\ ps ch) th)
BiReplaceImp0An0Not0 # <title> Substitution </title> # <table> # (-> (/\ (-. [ ph ] ] ] ) ch) th) # (<-> [ ph ] [ ps ] ) # (-> (/\ (-. [ [ [ ps ] ) ch) th) # </table>
(-> (/\ (-. ph) ch) th) , (<-> ph ps)(-> (/\ (-. ps) ch) th)
BiReplaceImp0An1An0 # <title> Substitution </title> # <table> # (-> (/\ ph (/\ [ ps ] ] ] th)) ta) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph (/\ [ [ [ ch ] th)) ta) # </table>
(-> (/\ ph (/\ ps th)) ta) , (<-> ps ch)(-> (/\ ph (/\ ch th)) ta)
BiReplaceImp0An1An0Not0 # <title> Substitution </title> # <table> # (-> (/\ ph (/\ (-. [ ps ] ] ] ) th)) ta) # (<-> [ ps ] [ ch ] ) # (-> (/\ ph (/\ (-. [ [ [ ch ] ) th)) ta) # </table>
(-> (/\ ph (/\ (-. ps) th)) ta) , (<-> ps ch)(-> (/\ ph (/\ (-. ch) th)) ta)
BiReplaceImp1Imp0Not0 # <title> Substitution </title> # <table> # (-> ph (-> (-. [ ps ] ] ] ) th)) # (<-> [ ps ] [ ch ] ) # (-> ph (-> (-. [ [ [ ch ] ) th)) # </table>
(-> ph (-> (-. ps) th)) , (<-> ps ch)(-> ph (-> (-. ch) th))
(-> (=q A B) (-> (e. A (rationals)) (<-> (=z (top A) (0z)) (=z (top B) (0z)))))
(-> (=q A B) (-> (e. A (rationals)) (=q (</> (bottom A) (top A)) (</> (bottom B) (top B)))))
BiReplaceImp1Bi0An0 # <title> Substitution </title> # <table> # (-> ph (<-> (/\ [ ps ] ] ] th) ta)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> (/\ [ [ [ ch ] th) ta)) # </table>
(-> ph (<-> (/\ ps th) ta)) , (<-> ps ch)(-> ph (<-> (/\ ch th) ta))
BiReplaceImp1Bi0An0Not0 # <title> Substitution </title> # <table> # (-> ph (<-> (/\ (-. [ ps ] ] ] ) th) ta)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> (/\ (-. [ [ [ ch ] ) th) ta)) # </table>
(-> ph (<-> (/\ (-. ps) th) ta)) , (<-> ps ch)(-> ph (<-> (/\ (-. ch) th) ta))
BiReplaceImp1Bi0An1 # <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))
BiReplaceImp1Bi0An1Not0 # <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))
BiReplaceImp1Bi1Not0 # <title> Substitution </title> # <table> # (-> ph (<-> ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps (-. [ [ [ th ] ))) # </table>
(-> ph (<-> ps (-. ch))) , (<-> ch th)(-> ph (<-> ps (-. th)))
(-> (=q A B) (<-> (/\ (e. A (rationals)) (e. B (rationals))) (e. A (rationals))))
qminusClosure # <title> Closure of rationals under subtraction </title>
(-> (/\ (e. A (rationals)) (e. B (rationals))) (e. (-q A B) (rationals)))
(-> (<-> ph ps) (=q (ifn ph A B) (ifn ps A B)))
(-> (/\ (e. A (rationals)) (=q A C)) (=q (/ B C) (/ B A)))
BiReplaceImp1Imp1Not0 # <title> Substitution </title> # <table> # (-> ph (-> ps (-. [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (-. [ [ [ th ] ))) # </table>
(-> ph (-> ps (-. ch))) , (<-> ch th)(-> ph (-> ps (-. th)))
ImpReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (-> ps ch)(-> ph (/\ ch th))
(-> (=q A C) (=q (/ B A) (/ B C)))
(=q A B)(=q (/ A C) (/ B C))
(-> ph (=q A B))(-> ph (=q (/ A C) (/ B C)))
(=q A C)(=q (/ B A) (/ B C))
qdiveqq12 # <title> Equivalence for / </title> ##
(-> (/\ (=q A B) (=q C D)) (=q (/ A C) (/ B D)))
(-> ph (=q A C))(-> ph (=q (/ B A) (/ B C)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (=q (/ A C) (/ B D)))
df-qdivrat # <title> Rational Definition of Division </title>
(-> (e. B (rationals)) (=q (/ A B) (*q A (</> (bottom B) (top B)))))
df-qdivNaN # <title> Definition of Division for NaN </title>
(-> (-. (e. B (rationals))) (=q (/ A B) (NaN)))
qdivNaN # <title> Divide by NaN </title>
(=q (/ A (NaN)) (NaN))
divideBy0 # <title> Divide by 0 </title> # <summary> Division by 0 gives Not a Number.
(=q (/ A (0q)) (NaN))
QeqReplaceImp1Qeq1Qmul1 # <title> Substitution </title> # <table> # (-> ph (=q A (*q B [ C ] ] ] ))) # (=q [ C ] [ D ] ) # (-> ph (=q A (*q B [ [ [ D ] ))) # </table>
(-> ph (=q A (*q B C))) , (=q C D)(-> ph (=q A (*q B D)))
ZeqReplaceImp1Qeq1Qmul1Frac0 # <title> Substitution </title> # <table> # (-> ph (=q A (*q B (</> [ C ] ] ] A')))) # (=z [ C ] [ D ] ) # (-> ph (=q A (*q B (</> [ [ [ D ] A')))) # </table>
(-> ph (=q A (*q B (</> C A')))) , (=z C D)(-> ph (=q A (*q B (</> D A'))))
ZeqReplaceImp1Qeq1Qmul1Frac1 # <title> Substitution </title> # <table> # (-> ph (=q A (*q B (</> C [ D ] ] ] )))) # (=z [ D ] [ A' ] ) # (-> ph (=q A (*q B (</> C [ [ [ A' ] )))) # </table>
(-> ph (=q A (*q B (</> C D)))) , (=z D A')(-> ph (=q A (*q B (</> C A'))))
qdivfrac # <title> Divide Fractions </title>
(-> (-. (=z D (0z))) (=q (/ (</> A B) (</> C D)) (</> (*z A D) (*z B C))))
BiReplaceBi1Not0Or1 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (\/ ps [ [ [ th ] ))) # </table>
(<-> ph (-. (\/ ps ch))) , (<-> ch th)(<-> ph (-. (\/ ps th)))
(<-> (/\ (-. (=q A (0q))) (e. A (rationals))) (/\ (-. (=z (top A) (0z))) (-. (=z (bottom A) (0z)))))
QeqReplaceImp1Qeq0Qdiv0 # <title> Substitution </title> # <table> # (-> ph (=q (/ [ A ] ] ] C) D)) # (=q [ A ] [ B ] ) # (-> ph (=q (/ [ [ [ B ] C) D)) # </table>
(-> ph (=q (/ A C) D)) , (=q A B)(-> ph (=q (/ B C) D))
QeqReplaceImp1Qeq0Qdiv1 # <title> Substitution </title> # <table> # (-> ph (=q (/ A [ B ] ] ] ) D)) # (=q [ B ] [ C ] ) # (-> ph (=q (/ A [ [ [ C ] ) D)) # </table>
(-> ph (=q (/ A B) D)) , (=q B C)(-> ph (=q (/ A C) D))
qdivcan # <title> Cancel using Division </title> # <suggest> right('Simplify', '1') </suggest>
(-> (/\ (-. (=q A (0q))) (e. A (rationals))) (=q (/ A A) (1q)))
QeqReplaceQeq0Qdiv1 # <title> Substitution </title> # <table> # (=q (/ A [ B ] ] ] ) D) # (=q [ B ] [ C ] ) # (=q (/ A [ [ [ C ] ) D) # </table>
(=q (/ A B) D) , (=q B C)(=q (/ A C) D)
QeqReplaceQeq0Qdiv0 # <title> Substitution </title> # <table> # (=q (/ [ A ] ] ] C) D) # (=q [ A ] [ B ] ) # (=q (/ [ [ [ B ] C) D) # </table>
(=q (/ A C) D) , (=q A B)(=q (/ B C) D)
qdivid # <title> Division Identity </title> # <suggest> right('Simplify', '1') </suggest> # <summary> Division by 1 has no effect. </summary>
(=q (/ A (1q)) A)
ZeqReplaceImp1Zeq0Zmul1 # <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))
ZeqReplaceImp1Zeq1Zmul0 # <title> Substitution </title> # <table> # (-> ph (=z A (*z [ B ] ] ] D))) # (=z [ B ] [ C ] ) # (-> ph (=z A (*z [ [ [ C ] D))) # </table>
(-> ph (=z A (*z B D))) , (=z B C)(-> ph (=z A (*z C D)))
(<-> (=q A (0q)) (/\ (=z (top A) (0z)) (-. (=z (bottom A) (0z)))))
qmul0 # <title> Multiply by 0 </title>
(-> (e. A (rationals)) (=q (*q A (0q)) (0q)))
QeqReplaceQeq0Qdiv0Qmul0 # <title> Substitution </title> # <table> # (=q (/ (*q [ A ] ] ] C) D) A') # (=q [ A ] [ B ] ) # (=q (/ (*q [ [ [ B ] C) D) A') # </table>
(=q (/ (*q A C) D) A') , (=q A B)(=q (/ (*q B C) D) A')
QeqReplaceQeq0Qdiv0Qmul1 # <title> Substitution </title> # <table> # (=q (/ (*q A [ B ] ] ] ) D) A') # (=q [ B ] [ C ] ) # (=q (/ (*q A [ [ [ C ] ) D) A') # </table>
(=q (/ (*q A B) D) A') , (=q B C)(=q (/ (*q A C) D) A')
QeqReplaceImp1Qeq0Qmul0 # <title> Substitution </title> # <table> # (-> ph (=q (*q [ A ] ] ] C) D)) # (=q [ A ] [ B ] ) # (-> ph (=q (*q [ [ [ B ] C) D)) # </table>
(-> ph (=q (*q A C) D)) , (=q A B)(-> ph (=q (*q B C) D))
qdivmulass # <title> Ass. Multiply & Divide </title> # <summary> Reorder multiplication and division. </summary> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(=q (/ (*q A B) C) (*q A (/ B C)))
qdivReciprocal # <title> Division is multiplying by reciprocal </title> # <summary> # Division is identical to multiplying by the reciprocal of # a number. # </summary> # <suggest> left('Simplify', '/') </suggest>
(=q (/ A B) (*q A (/ (1q) B)))
qdivdist # <title> Distributive Property </title> # <summary> Distribute division over addition </title>
(=q (/ (+q A B) C) (+q (/ A C) (/ B C)))
qdivcan2 # <title> Cancel using Division </title>
(-> (/\ (-. (=q A (0q))) (e. A (rationals))) (=q (/ (*q B A) A) B))
qdivcan3 # <title> Cancel using Division </title>
(-> (/\ (-. (=q A (0q))) (e. A (rationals))) (=q (/ (*q A B) A) B))
df-qpos # <title> Definition of a Positive Rational </title> # <summary> # This definition is used to construct the <a href="df-zlt">definition of less than </a>. # Once less than is defined <a href="qltpos">the usual definition</a> holds. # </summary> # <suggest> left('Simplify', '+') </suggest>
(<-> (qpos A) (zpos (*z (top A) (bottom A))))
(-> (=z (top A) (0z)) (-. (qpos A)))
(-> (=z (bottom A) (0z)) (-. (qpos A)))
(-> (=q A B) (-> (\/ (=z (bottom A) (0z)) (=z (top A) (0z))) (<-> (qpos A) (qpos B))))
ZeqReplaceImp1Zeq1Zmul0Zmul1 # <title> Substitution </title> # <table> # (-> ph (=z A (*z (*z B [ C ] ] ] ) A'))) # (=z [ C ] [ D ] ) # (-> ph (=z A (*z (*z B [ [ [ D ] ) A'))) # </table>
(-> ph (=z A (*z (*z B C) A'))) , (=z C D)(-> ph (=z A (*z (*z B D) A')))
BiReplaceImp1Imp1Bi0 # <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)))
BiReplaceImp1Imp1Bi1 # <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)))
BiReplaceBi1Not0Or0 # <title> Substitution </title> # <table> # (<-> ph (-. (\/ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (\/ [ [ [ ch ] th))) # </table>
(<-> ph (-. (\/ ps th))) , (<-> ps ch)(<-> ph (-. (\/ ch th)))
(-> (=q A B) (<-> (qpos A) (qpos B)))
(=q A B)(<-> (qpos A) (qpos B))
(-> ph (=q A B))(-> ph (<-> (qpos A) (qpos B)))
df-qlt # <title> Def. Rational Less Than </title> # <suggest> left('Simplify', '<') </suggest>
(<-> (<q A B) (qpos (-q B A)))
qlteqq1 # <title> Equivalence for <q </title> ##
(-> (=q A C) (<-> (<q A B) (<q C B)))
(=q A C)(<-> (<q A B) (<q C B))
qlteqq2 # <title> Equivalence for <q </title> ##
(-> (=q B C) (<-> (<q A B) (<q A C)))
(-> ph (=q A C))(-> ph (<-> (<q A B) (<q C B)))
(=q B C)(<-> (<q A B) (<q A C))
qlteqq12 # <title> Equivalence for <q </title> ##
(-> (/\ (=q A B) (=q C D)) (<-> (<q A C) (<q B D)))
(-> ph (=q B C))(-> ph (<-> (<q A B) (<q A C)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (<-> (<q A C) (<q B D)))
QeqReplaceBi1Qpos0 # <title> Substitution </title> # <table> # (<-> ph (qpos [ A ] ] ] )) # (=q [ A ] [ B ] ) # (<-> ph (qpos [ [ [ B ] )) # </table>
(<-> ph (qpos A)) , (=q A B)(<-> ph (qpos B))
qltpos # <title> Alternative Def. of Positive Rational </title> # <summary> # The <a href="df-df-qpos">definition of positive rationals</a> was used to construct the # definition of less than. This theorem shows that the usual definition # of a positive number holds once less than has been defined. # </summary>
(<-> (<q (0q) A) (qpos A))
df-qle # <title> Def. Rational Less Than or Equal </title>
(<-> (<=q A B) (\/ (<q A B) (=q A B)))
qleeqq1 # <title> Equivalence for <=q </title> ##
(-> (=q A C) (<-> (<=q A B) (<=q C B)))
(=q A C)(<-> (<=q A B) (<=q C B))
qleeqq2 # <title> Equivalence for <=q </title> ##
(-> (=q B C) (<-> (<=q A B) (<=q A C)))
(-> ph (=q A C))(-> ph (<-> (<=q A B) (<=q C B)))
(=q B C)(<-> (<=q A B) (<=q A C))
qleeqq12 # <title> Equivalence for <=q </title> ##
(-> (/\ (=q A B) (=q C D)) (<-> (<=q A C) (<=q B D)))
(-> ph (=q B C))(-> ph (<-> (<=q A B) (<=q A C)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (<-> (<=q A C) (<=q B D)))
df-qge # <title> Def. of Rational Greater than or Equal </title>
(<-> (>=q A B) (-. (<q A B)))
qgeeqq1 # <title> Equivalence for >=q </title> ##
(-> (=q A C) (<-> (>=q A B) (>=q C B)))
(=q A C)(<-> (>=q A B) (>=q C B))
qgeeqq2 # <title> Equivalence for >=q </title> ##
(-> (=q B C) (<-> (>=q A B) (>=q A C)))
(-> ph (=q A C))(-> ph (<-> (>=q A B) (>=q C B)))
(=q B C)(<-> (>=q A B) (>=q A C))
qgeeqq12 # <title> Equivalence for >=q </title> ##
(-> (/\ (=q A B) (=q C D)) (<-> (>=q A C) (>=q B D)))
(-> ph (=q B C))(-> ph (<-> (>=q A B) (>=q A C)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (<-> (>=q A C) (>=q B D)))
df-qgt # <title> Definition of Rational Greater than </title>
(<-> (>q A B) (-. (<=q A B)))
qgteqq1 # <title> Equivalence for >q </title> ##
(-> (=q A C) (<-> (>q A B) (>q C B)))
(=q A C)(<-> (>q A B) (>q C B))
qgteqq2 # <title> Equivalence for >q </title> ##
(-> (=q B C) (<-> (>q A B) (>q A C)))
(-> ph (=q A C))(-> ph (<-> (>q A B) (>q C B)))
(=q B C)(<-> (>q A B) (>q A C))
qgteqq12 # <title> Equivalence for >q </title> ##
(-> (/\ (=q A B) (=q C D)) (<-> (>q A C) (>q B D)))
(-> ph (=q B C))(-> ph (<-> (>q A B) (>q A C)))
(-> ph (=q A B)) , (-> ph (=q C D))(-> ph (<-> (>q A C) (>q B D)))
qposproduct1 # <title> Product of positive numbers is positive </title>
(-> (/\ (qpos A) (qpos B)) (qpos (*q A B)))
QeqReplaceQeq0Qmul0 # <title> Substitution </title> # <table> # (=q (*q [ A ] ] ] C) D) # (=q [ A ] [ B ] ) # (=q (*q [ [ [ B ] C) D) # </table>
(=q (*q A C) D) , (=q A B)(=q (*q B C) D)
QeqReplaceQeq0Qmul1 # <title> Substitution </title> # <table> # (=q (*q A [ B ] ] ] ) D) # (=q [ B ] [ C ] ) # (=q (*q A [ [ [ C ] ) D) # </table>
(=q (*q A B) D) , (=q B C)(=q (*q A C) D)
QeqReplaceQeq1Qneg0 # <title> Substitution </title> # <table> # (=q A (-qn [ B ] ] ] )) # (=q [ B ] [ C ] ) # (=q A (-qn [ [ [ C ] )) # </table>
(=q A (-qn B)) , (=q B C)(=q A (-qn C))
qnegqmul # <title> Multiply Negated Number </title> # <suggest> right('Simplify', '-') </suggest>
(=q (*q (-qn A) B) (-qn (*q A B)))
qnegqmul2 # <title> Multiply Negated Number </title> # <suggest> right('Simplify', '-') </suggest>
(=q (*q A (-qn B)) (-qn (*q A B)))
qminusdist # <title> Distributive Property </title> # <summary> Distribute multiplication over subtraction. </summary> # <table> # (=q (*q <c> A (+q B C)) (-q (*q <c> A B) (*q <c> A C))) # </table> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(=q (*q A (-q B C)) (-q (*q A B) (*q A C)))
posReciprocal # <title> Positive numbers have positive reciprocals </title>
(<-> (qpos (/ (1q) A)) (qpos A))
0qnotPos # <title> 0 is not positive </title>
(-> (=q A (0q)) (-. (qpos A)))
QeqReplaceImp1Imp1Qpos0 # <title> Substitution </title> # <table> # (-> ph (-> ps (qpos [ A ] ] ] ))) # (=q [ A ] [ B ] ) # (-> ph (-> ps (qpos [ [ [ B ] ))) # </table>
(-> ph (-> ps (qpos A))) , (=q A B)(-> ph (-> ps (qpos B)))
qmulqlt.1 # <title> Multiply a positive number on an inequality </title>
(-> (qpos A) (-> (<q B C) (<q (*q A B) (*q A C))))
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
qltneq # <title> Less Than Implies Not Equal </title>
(-> (e. A (rationals)) (-> (<q A B) (-. (=q A B))))
qmulqlt # <title> Multiply Inequality by a Positive Number </title> # <summary> Multiplication by a positive rational preserves the inequality relation. </summary>
(-> (/\ (<q (0q) A) (e. A (rationals))) (<-> (<q (*q A B) (*q A C)) (<q B C)))
df-2q # <title> Definition of 2 as a Fraction </title>
(=q (2q) (</> (2z) (1z)))
df-3q # <title> Definition of 3 as a Fraction </title>
(=q (3q) (</> (3z) (1z)))
df-4q # <title> Definition of 4 as a Fraction </title>
(=q (4q) (</> (4z) (1z)))
df-5q # <title> Definition of 5 as a Fraction </title>
(=q (5q) (</> (5z) (1z)))
df-6q # <title> Definition of 6 as a Fraction </title>
(=q (6q) (</> (6z) (1z)))
df-7q # <title> Definition of 7 as a Fraction </title>
(=q (7q) (</> (7z) (1z)))
df-8q # <title> Definition of 8 as a Fraction </title>
(=q (8q) (</> (8z) (1z)))
df-9q # <title> Definition of 9 as a Fraction </title>
(=q (9q) (</> (9z) (1z)))
df-10q # <title> Definition of 10 as a Fraction </title>
(=q (10q) (</> (10z) (1z)))
df-.1 # <title> Definition of One-Tenth </title>
(=q (.1) (/ (1q) (10q)))
(T)