# List of theorems

List of theorems in peano_new/arithmetic/common/division.gh:

diveq1 # <context> # This theorem is part of a series of proofs on the properties of # <a href="/wiki/peano/arithmetic/divide">division</a>. These theorems # apply to rational and real numbers. # </context> # <title> Divide a number on both sides of an equation </title> # <table> # (-> (= <g> A <b> B) (= (/ <g> A <r> C) (/ <b> B <r> C))) # </table>
(-> (= A B) (= (/ A C) (/ B C)))
diveq2 # <title> Divide a number on both sides of an equation </title>
(-> (= A B) (= (/ C A) (/ C B)))
diveq12i # <title> Equality over Addition </title> # <table> # (= A ] ] ] [ B ] ] ) # (= [ [ C ] [ [ [ D) # (= (/ A ] [ C ] ) (/ [ B ] [ D)) # </table>
(= A B) , (= C D)(= (/ A C) (/ B D))
diveq1d # <title> Equality over Addition </title>
(-> ph (= A B))(-> ph (= (/ A C) (/ B C)))
diveq2d # <title> Equality over Addition </title>
(-> ph (= A B))(-> ph (= (/ C A) (/ C B)))
diveq12d # <title> Equality over Addition </title>
(-> ph (= A B)) , (-> ph (= C D))(-> ph (= (/ A C) (/ B D)))
diveq1i # <title> Add a number to both sides </title> # <table> # (= A ] ] [ B ] ) # (= (/ A ] <g> C) ] (/ [ B ] <g> C)) # </table>
(= A B)(= (/ A C) (/ B C))
diveq2i # <title> Add a number to both sides </title> # <table> # (= [ A ] [ [ B ) # (= (/ <g> C [ A ] ) [ (/ <g> C [ B)) # </table>
(= A B)(= (/ C A) (/ C B))
divcani # <title> Cancel with Division </title>
(-. (= A (0)))(= (* A (/ B A)) B)
reciprocalcan # <title> Cancel with Division </title>
(-> (-. (= A (0))) (= (* A (/ (1) A)) (1)))
reciprocalcani # <title> Cancel with Division </title>
(-. (= A (0)))(= (* A (/ (1) A)) (1))
divcan2 # <title> Cancel With Division </title>
(-> (-. (= A (0))) (= (/ (* A B) A) B))
divcan2i # <title> Cancel with Division </title>
(-. (= A (0)))(= (/ (* A B) A) B)
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq0Div0 # <title> Substitution </title> # <table> # (-> ph (= (/ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (-> ph (= (/ [ [ [ B ] C) D)) # </table>
(-> ph (= (/ A C) D)) , (= A B)(-> ph (= (/ B C) D))
divcan3 # <title> Cancel with Division </title>
(-> (-. (= A (0))) (= (/ (* B A) A) B))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
BiReplaceImp0Not0 # <title> Substitution </title> # <table> # (-> (-. [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (-. [ [ [ ps ] ) ch) # </table>
(-> (-. ph) ch) , (<-> ph ps)(-> (-. ps) ch)
divid # <title> Divide by 1 </title>
(= (/ A (1)) A)
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
EqReplaceImp1Eq1Mul0 # <title> Substitution </title> # <table> # (-> ph (= A (* [ B ] ] ] D))) # (= [ B ] [ C ] ) # (-> ph (= A (* [ [ [ C ] D))) # </table>
(-> ph (= A (* B D))) , (= B C)(-> ph (= A (* C D)))
expandFrac # <title> Expand Fraction </title>
(-> (-. (= B (0))) (= (/ A B) (* A (/ (1) B))))
expandFraci # <title> Expand Fraction </title>
(-. (= B (0)))(= (/ A B) (* A (/ (1) B)))
0div # <title> 0 divided by anything is 0 </title>
(-> (-. (= A (0))) (= (/ (0) A) (0)))
0divi # <title> 0 divided by anything is 0 </title>
(-. (= A (0)))(= (/ (0) A) (0))
frac1 # <title> Cancel using Division </title>
(-> (-. (= A (0))) (= (/ A A) (1)))
frac1i # <title> Cancel using Division </title>
(-. (= A (0)))(= (/ A A) (1))
divmulass # <title> Division & Multiplication Ass. </title>
(-> (-. (= C (0))) (= (* A (/ B C)) (/ (* A B) C)))
divmulassi # <title> Division & Multiplication Ass. </title>
(-. (= C (0)))(= (* A (/ B C)) (/ (* A B) C))
EqReplaceEq1Div0 # <title> Substitution </title> # <table> # (= A (/ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (/ [ [ [ C ] D)) # </table>
(= A (/ B D)) , (= B C)(= A (/ C D))
divmulass2i # <title> Division & Multiplication Ass. </title>
(-. (= C (0)))(= (* (/ B C) A) (/ (* B A) C))
zeroProducti # <title> Zero Product Property </title> # <table> # (-. (= A ] ] ] (0))) # (-. (= [ [ B ] (0))) # (-. (= (* A ] [ B ] ) (0))) # </table>
(-. (= A (0))) , (-. (= B (0)))(-. (= (* A B) (0)))
mulBottom # <title> Multiply Denominators </title>
(-> (/\ (-. (= A (0))) (-. (= B (0)))) (= (* (/ (1) A) (/ (1) B)) (/ (1) (* A B))))
mulBottomi # <title> Multiply Denominators </title>
(-. (= A (0))) , (-. (= B (0)))(= (* (/ (1) A) (/ (1) B)) (/ (1) (* A B)))
fracmul # <title> Multiply Fractions </title>
(-> (/\ (-. (= B (0))) (-. (= D (0)))) (= (* (/ A B) (/ C D)) (/ (* A C) (* B D))))
fracmuli # <title> Multiply Fractions </title>
(-. (= B (0))) , (-. (= D (0)))(= (* (/ A B) (/ C D)) (/ (* A C) (* B D)))
fracFactors # <title> Fraction with common factor </title> # <summary> Numerators and Denominators with common factors can be simplified. </summary>
(-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (* A C) (* B C)) (/ A B)))
fracFactorsi # <title> Fraction with common factor </title> # <summary> Numerators and Denominators with common factors can be simplified. </summary> # <table> # (-. (= B (0)) # (-. (= C (0))) # (= (/ (* A <r> C) (* B <r> C)) (/ A B)) # </table>
(-. (= B (0))) , (-. (= C (0)))(= (/ (* A C) (* B C)) (/ A B))
divdistr # <title> Distribute Division over Addition </title>
(-> (-. (= C (0))) (= (+ (/ A C) (/ B C)) (/ (+ A B) C)))
divdistri # <title> Distribute Division over Addition </title>
(-. (= C (0)))(= (+ (/ A C) (/ B C)) (/ (+ A B) C))
EqReplaceEq1Div1 # <title> Substitution </title> # <table> # (= A (/ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (/ B [ [ [ D ] )) # </table>
(= A (/ B C)) , (= C D)(= A (/ B D))
EqReplaceImp1Eq1Div1 # <title> Substitution </title> # <table> # (-> ph (= A (/ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (-> ph (= A (/ B [ [ [ D ] ))) # </table>
(-> ph (= A (/ B C))) , (= C D)(-> ph (= A (/ B D)))
EqReplaceImp1Eq1Div0 # <title> Substitution </title> # <table> # (-> ph (= A (/ [ B ] ] ] D))) # (= [ B ] [ C ] ) # (-> ph (= A (/ [ [ [ C ] D))) # </table>
(-> ph (= A (/ B D))) , (= B C)(-> ph (= A (/ C D)))
(-> (/\ (-. (= B (0))) (-. (= D (0)))) (= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D))))
(-. (= B (0))) , (-. (= D (0)))(= (+ (/ A B) (/ C D)) (/ (+ (* A D) (* B C)) (* B D)))
negNumerator # <title> Negative Numerator </title> # <summary> A negative numerator is equivalent to a negative fraction. </summary>
(-> (-. (= B (0))) (= (/ (-n A) B) (-n (/ A B))))
negNumeratori # <title> Negative Numerator </title> # <summary> A negative numerator is equivalent to a negative fraction. </summary>
(-. (= B (0)))(= (/ (-n A) B) (-n (/ A B)))
EqReplaceNot0Eq0 # <title> Substitution </title> # <table> # (-. (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-. (= [ [ [ B ] C)) # </table>
(-. (= A C)) , (= A B)(-. (= B C))
EqReplaceEq1Neg0 # <title> Substitution </title> # <table> # (= A (-n [ B ] ] ] )) # (= [ B ] [ C ] ) # (= A (-n [ [ [ C ] )) # </table>
(= A (-n B)) , (= B C)(= A (-n C))
negDenominatori # <title> Negative Denominator </title> # <summary> A negative denominator is equivalent to a negative fraction. </summary>
(-. (= B (0)))(= (/ A (-n B)) (-n (/ A B)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
EqReplaceBi1Not0Eq0 # <title> Substitution </title> # <table> # (<-> ph (-. (= [ A ] ] ] C))) # (= [ A ] [ B ] ) # (<-> ph (-. (= [ [ [ B ] C))) # </table>
(<-> ph (-. (= A C))) , (= A B)(<-> ph (-. (= B C)))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
EqReplaceImp1Eq0Div1 # <title> Substitution </title> # <table> # (-> ph (= (/ A [ B ] ] ] ) D)) # (= [ B ] [ C ] ) # (-> ph (= (/ A [ [ [ C ] ) D)) # </table>
(-> ph (= (/ A B) D)) , (= B C)(-> ph (= (/ A C) D))
EqReplaceImp1Eq0Div1Neg0 # <title> Substitution </title> # <table> # (-> ph (= (/ A (-n [ B ] ] ] )) D)) # (= [ B ] [ C ] ) # (-> ph (= (/ A (-n [ [ [ C ] )) D)) # </table>
(-> ph (= (/ A (-n B)) D)) , (= B C)(-> ph (= (/ A (-n C)) D))
negDenominator # <title> Negative Denominator </title>
(-> (-. (= B (0))) (= (-n (/ A B)) (/ A (-n B))))
doublenegfrac # <title> Double Negative Fraction </title>
(-> (-. (= B (0))) (= (/ (-n A) (-n B)) (/ A B)))
doublenegfraci # <title> Double Negative Fraction </title>
(-. (= B (0)))(= (/ (-n A) (-n B)) (/ A B))
EqReplaceBi0Eq1 # <title> Substitution </title> # <table> # (<-> (= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (= A [ [ [ C ] ) ph) # </table>
(<-> (= A B) ph) , (= B C)(<-> (= A C) ph)
EqReplaceBi0Eq0 # <title> Substitution </title> # <table> # (<-> (= [ A ] ] ] C) ph) # (= [ A ] [ B ] ) # (<-> (= [ [ [ B ] C) ph) # </table>
(<-> (= A C) ph) , (= A B)(<-> (= B C) ph)
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
EqReplaceImp1Bi0Eq1 # <title> Substitution </title> # <table> # (-> ph (<-> (= A [ B ] ] ] ) ps)) # (= [ B ] [ C ] ) # (-> ph (<-> (= A [ [ [ C ] ) ps)) # </table>
(-> ph (<-> (= A B) ps)) , (= B C)(-> ph (<-> (= A C) ps))
reciprocalNot0 # <title> Nonzero numbers have nonzero reciprocal </title>
(-> (-. (= A (0))) (-. (= (/ (1) A) (0))))
EqReplaceEq0Div0 # <title> Substitution </title> # <table> # (= (/ [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (/ [ [ [ B ] C) D) # </table>
(= (/ A C) D) , (= A B)(= (/ B C) D)
EqReplaceEq0Div1 # <title> Substitution </title> # <table> # (= (/ A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (/ A [ [ [ C ] ) D) # </table>
(= (/ A B) D) , (= B C)(= (/ A C) D)
fracFactors2 # <title> Common Division in Fraction </title>
(-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A C) (/ B C)) (/ A B)))
fracFactors2i # <title> Common Division in Fraction </title>
(-. (= B (0))) , (-. (= C (0)))(= (/ (/ A C) (/ B C)) (/ A B))
EqReplaceImp1Eq1Mul1 # <title> Substitution </title> # <table> # (-> ph (= A (* B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (-> ph (= A (* B [ [ [ D ] ))) # </table>
(-> ph (= A (* B C))) , (= C D)(-> ph (= A (* B D)))
divcom # <title> Commute Division </title>
(-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ (/ A C) B)))
divcomi # <title> Commute Division </title>
(-. (= B (0))) , (-. (= C (0)))(= (/ (/ A B) C) (/ (/ A C) B))
EqReplaceEq1Div0Div0 # <title> Substitution </title> # <table> # (= A (/ (/ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (/ (/ [ [ [ C ] D) A')) # </table>
(= A (/ (/ B D) A')) , (= B C)(= A (/ (/ C D) A'))
divideFraci # <title> Divide Fractions </title>
(-. (= B (0))) , (-. (= C (0))) , (-. (= D (0)))(= (/ (* A D) (* B C)) (/ (/ A B) (/ C D)))
divminusdistr # <title> Distribute Division Over Subtraction </title>
(-> (-. (= C (0))) (= (- (/ A C) (/ B C)) (/ (- A B) C)))
divminusdistri # <title> Distribute Division Over Subtraction </title>
(-. (= C (0)))(= (- (/ A C) (/ B C)) (/ (- A B) C))
doublediv # <title> Multiply Two Denominators </title>
(-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ (/ A B) C) (/ A (* B C))))
doubledivi # <title> Multiply Two Denominators </title>
(-. (= B (0))) , (-. (= C (0)))(= (/ (/ A B) C) (/ A (* B C)))
EqReplaceBi0Pos0 # <title> Substitution </title> # <table> # (<-> (pos [ A ] ] ] ) ph) # (= [ A ] [ B ] ) # (<-> (pos [ [ [ B ] ) ph) # </table>
(<-> (pos A) ph) , (= A B)(<-> (pos B) ph)
BiReplaceImp1Imp0 # <title> Substitution </title> # <table> # (-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (-> [ [ [ ch ] th)) # </table>
(-> ph (-> ps th)) , (<-> ps ch)(-> ph (-> ch th))
BiReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (<-> ps ch)(-> ph (\/ ch th))
BiReplaceImp1Or0An0 # <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))
posReciprocal # <title> A positive number has a positive reciprocal </title>
(-> (> A (0)) (> (/ (1) A) (0)))
(-> (/\ (-. (= A (0))) (-. (= B (0)))) (-. (= (/ A B) (0))))
(-. (= A (0))) , (-. (= B (0)))(-. (= (/ A B) (0)))
(-> (/\ (-. (= B (0))) (-. (= C (0)))) (= (/ A (/ B C)) (/ (* A C) B)))
1notEqual0 # <title> One-Digit Inequality </title>
(-. (= (1) (0)))
doubleReciprocal # <title> A number is its reciprocal's reciprocal </title>
(-> (-. (= A (0))) (= (/ (1) (/ (1) A)) A))
(-> (-. (= A (0))) (<-> (> A (0)) (> (/ (1) A) (0))))
moveBottom # <title> Divide Both Sides </title> # <table> # [ (= (* <c> a b) c) # (-> (-. (= <c> a (0))) [ (= b (/ c <c> a))) # </table>
(= (* a b) c)(-> (-. (= a (0))) (= b (/ c a)))
moveBottomi # <title> Divide Both Sides </title> # <table> # (-. (= <c> a ] [ (0))) # (= (* <c> a b) ] [ c) # (= b ] [ (/ c <c> a)) # </table>
(-. (= a (0))) , (= (* a b) c)(= b (/ c a))
EqReplaceEq0Add0 # <title> Substitution </title> # <table> # (= (+ [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (+ [ [ [ B ] C) D) # </table>
(= (+ A C) D) , (= A B)(= (+ B C) D)
EqReplaceEq0Add1 # <title> Substitution </title> # <table> # (= (+ A [ B ] ] ] ) D) # (= [ B ] [ C ] ) # (= (+ A [ [ [ C ] ) D) # </table>
(= (+ A B) D) , (= B C)(= (+ A C) D)
EqReplaceEq0Add0Mul0 # <title> Substitution </title> # <table> # (= (+ (* [ A ] ] ] C) D) A') # (= [ A ] [ B ] ) # (= (+ (* [ [ [ B ] C) D) A') # </table>
(= (+ (* A C) D) A') , (= A B)(= (+ (* B C) D) A')
EqReplaceEq0Add0Minus1 # <title> Substitution </title> # <table> # (= (+ (- A [ B ] ] ] ) D) A') # (= [ B ] [ C ] ) # (= (+ (- A [ [ [ C ] ) D) A') # </table>
(= (+ (- A B) D) A') , (= B C)(= (+ (- A C) D) A')
EqReplaceEq0Add0Minus1Mul0 # <title> Substitution </title> # <table> # (= (+ (- A (* [ B ] ] ] D)) A') B') # (= [ B ] [ C ] ) # (= (+ (- A (* [ [ [ C ] D)) A') B') # </table>
(= (+ (- A (* B D)) A') B') , (= B C)(= (+ (- A (* C D)) A') B')
twoLinearEquations1 # <title> Solve two linear equations </title> # <summary> # Solves a system of two linearly independent equations for one of the # two variables y. The theorem # <a href="twoLinearEquations">twoLinearEquations</a> extends this result # to both variables x and y. This proof starts with three hypotheses: the two # equations and a statement expressing: ad-bc is not 0. # </summary>
(= (+ (* a x) (* b y)) u) , (= (+ (* c x) (* d y)) v) , (-. (= (- (* a d) (* b c)) (0)))(= y (/ (- (* a v) (* c u)) (- (* a d) (* b c))))
EqReplaceNot0Eq1 # <title> Substitution </title> # <table> # (-. (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-. (= A [ [ [ C ] )) # </table>
(-. (= A B)) , (= B C)(-. (= A C))
twoLinearEquations # <title> Solve two linear equations </title> # <summary> # Solves a system of two linearly independent equations involving two # variables x and y. This proof starts with three hypotheses: the two # equations and a statement expressing: ad-bc is not 0. This theorem # uses the theorem <a href="twoLinearEquations1">twoLinearEquations1</a> # which solves for one of the two variables. This theorem solves for # x and y by using <a href="twoLinearEquations1">twoLinearEquations1</a> # twice. # </summary>
(= (+ (* a x) (* b y)) u) , (= (+ (* c x) (* d y)) v) , (-. (= (- (* a d) (* b c)) (0)))(/\ (= x (/ (- (* d u) (* b v)) (- (* a d) (* b c)))) (= y (/ (- (* a v) (* c u)) (- (* a d) (* b c)))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)