# List of theorems

List of theorems in peano_new/arithmetic/reals/sqrt.gh:

sqrteqi # <context> # This theorem is part of a series of proofs about the properties of square roots. # The numbers here are assumed to be real numbers and we do not allow for negative # numbers to have imaginary square roots. A treatment of square roots for complex # number has not been added yet, but many of the building blocks for complex numbers # have been proven. # </context>
(= a b)(= (sqrt a) (sqrt b))
(-> ph (= a b))(-> ph (= (sqrt a) (sqrt b)))
ImpReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
sqrtsq1 # <title> A Square Root is an inverse of squaring </title>
(-> (>= a (0)) (= a (exp (sqrt a) (2))))
EqReplaceImp1Le0 # <title> Substitution </title> # <table> # (-> ph (<= [ a ] ] ] c)) # (= [ a ] [ b ] ) # (-> ph (<= [ [ [ b ] c)) # </table>
(-> ph (<= a c)) , (= a b)(-> ph (<= b c))
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)
BiReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (<-> ch th)(-> ph (/\ ps th))
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))
negsqrt0 # <title> Square Root Zero or Negative is Zero </title>
(-> (/\ (/\ (>= a (0)) (>= b (0))) (= (* (sqrt a) (sqrt b)) (-n (sqrt (* a b))))) (= (-n (sqrt (* a b))) (sqrt (* a b))))
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= a (* b [ c ] ] ] )) # (= [ c ] [ d ] ) # (= a (* b [ [ [ d ] )) # </table>
(= a (* b c)) , (= c d)(= a (* b d))
1plus1 # <title> One-digit Addition </title>
(= (+ (1) (1)) (2))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ a ] ] ] c) # (= [ a ] [ b ] ) # (= [ [ [ b ] c) # </table>
(= a c) , (= a b)(= b c)
0power2 # <title> Exponentiation </title>
(= (exp (0) (2)) (0))
EqReplaceImp1Eq1Sqrt0 # <title> Substitution </title> # <table> # (-> ph (= a (sqrt [ b ] ] ] ))) # (= [ b ] [ c ] ) # (-> ph (= a (sqrt [ [ [ c ] ))) # </table>
(-> ph (= a (sqrt b))) , (= b c)(-> ph (= a (sqrt c)))
EqReplaceImp0Eq1 # <title> Substitution </title> # <table> # (-> (= a [ b ] ] ] ) ph) # (= [ b ] [ c ] ) # (-> (= a [ [ [ c ] ) ph) # </table>
(-> (= a b) ph) , (= b c)(-> (= a c) ph)
EqReplaceImp0Eq1Neg0 # <title> Substitution </title> # <table> # (-> (= a (-n [ b ] ] ] )) ph) # (= [ b ] [ c ] ) # (-> (= a (-n [ [ [ c ] )) ph) # </table>
(-> (= a (-n b)) ph) , (= b c)(-> (= a (-n c)) ph)
EqReplaceImp0Eq1Neg0Sqrt0 # <title> Substitution </title> # <table> # (-> (= a (-n (sqrt [ b ] ] ] ))) ph) # (= [ b ] [ c ] ) # (-> (= a (-n (sqrt [ [ [ c ] ))) ph) # </table>
(-> (= a (-n (sqrt b))) ph) , (= b c)(-> (= a (-n (sqrt c))) ph)
EqReplaceImp1Eq0Neg0 # <title> Substitution </title> # <table> # (-> ph (= (-n [ a ] ] ] ) c)) # (= [ a ] [ b ] ) # (-> ph (= (-n [ [ [ b ] ) c)) # </table>
(-> ph (= (-n a) c)) , (= a b)(-> ph (= (-n b) c))
EqReplaceImp1Eq0Neg0Sqrt0 # <title> Substitution </title> # <table> # (-> ph (= (-n (sqrt [ a ] ] ] )) c)) # (= [ a ] [ b ] ) # (-> ph (= (-n (sqrt [ [ [ b ] )) c)) # </table>
(-> ph (= (-n (sqrt a)) c)) , (= a b)(-> ph (= (-n (sqrt b)) c))
ImpReplaceOr1 # <title> Substitution </title> # <table> # (\/ ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (\/ ph [ [ [ ch ] ) # </table>
(\/ ph ps) , (-> ps ch)(\/ ph ch)
sqrt0 # <title> Square Root of 0 </title>
(= (0) (sqrt (0)))
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)))
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)))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
ImpReplaceImp1An0 # <title> Substitution </title> # <table> # (-> ph (/\ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (/\ [ [ [ ch ] th)) # </table>
(-> ph (/\ ps th)) , (-> ps ch)(-> ph (/\ ch th))
ImpReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (-> ch th)(-> ph (/\ ps th))
ImpReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (-> ch th)(-> ph (\/ ps th))
EqReplaceImp1Ge1 # <title> Substitution </title> # <table> # (-> ph (>= a [ b ] ] ] )) # (= [ b ] [ c ] ) # (-> ph (>= a [ [ [ c ] )) # </table>
(-> ph (>= a b)) , (= b c)(-> ph (>= a c))
sqrtmul # <title> Multiply Square Roots </title>
(-> (/\ (>= a (0)) (>= b (0))) (= (* (sqrt a) (sqrt b)) (sqrt (* a b))))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= a (+ [ b ] ] ] d)) # (= [ b ] [ c ] ) # (= a (+ [ [ [ c ] d)) # </table>
(= a (+ b d)) , (= b c)(= a (+ c d))
EqReplaceEq0Add0 # <title> Substitution </title> # <table> # (= (+ [ a ] ] ] c) d) # (= [ a ] [ b ] ) # (= (+ [ [ [ b ] c) d) # </table>
(= (+ a c) d) , (= a b)(= (+ b c) d)
EqReplaceEq0Add0Add0 # <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')
EqReplaceGt0 # <title> Substitution </title> # <table> # (> [ a ] ] ] c) # (= [ a ] [ b ] ) # (> [ [ [ b ] c) # </table>
(> a c) , (= a b)(> b c)
EqReplaceGt1 # <title> Substitution </title> # <table> # (> a [ b ] ] ] ) # (= [ b ] [ c ] ) # (> a [ [ [ c ] ) # </table>
(> a b) , (= b c)(> a c)
2greater1 # <title> One-Digit Inequality </title>
(> (2) (1))
GtReplaceGt1 # <title> Substitution </title> # <table> # (> a [ b ] ] ] ) # (> [ b ] [ c ] ) # (> a [ [ [ c ] ) # </table>
(> a b) , (> b c)(> a c)
2greater0 # <title> One-Digit Inequality </title>
(> (2) (0))
2notEqual0 # <title> One-Digit Inequality </title>
(-. (= (2) (0)))
EqReplaceEq0Mul1 # <title> Substitution </title> # <table> # (= (* a [ b ] ] ] ) d) # (= [ b ] [ c ] ) # (= (* a [ [ [ c ] ) d) # </table>
(= (* a b) d) , (= b c)(= (* a c) d)
EqReplaceEq0Add0Add1 # <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')
EqReplaceEq1Mul1Div1 # <title> Substitution </title> # <table> # (= a (* b (/ c [ d ] ] ] ))) # (= [ d ] [ a' ] ) # (= a (* b (/ c [ [ [ a' ] ))) # </table>
(= a (* b (/ c d))) , (= d a')(= a (* b (/ c a')))
EqReplaceEq0Add0Add1Div0 # <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')
EqReplaceEq0Add0Add1Mul1 # <title> Substitution </title> # <table> # (= (+ (+ a (* b [ c ] ] ] )) a') b') # (= [ c ] [ d ] ) # (= (+ (+ a (* b [ [ [ d ] )) a') b') # </table>
(= (+ (+ a (* b c)) a') b') , (= c d)(= (+ (+ a (* b d)) a') b')
EqReplaceEq0Add0Add1Mul0 # <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')
EqReplaceEq1Div0 # <title> Substitution </title> # <table> # (= a (/ [ b ] ] ] d)) # (= [ b ] [ c ] ) # (= a (/ [ [ [ c ] d)) # </table>
(= a (/ b d)) , (= b c)(= a (/ c d))
EqReplaceEq1Div1 # <title> Substitution </title> # <table> # (= a (/ b [ c ] ] ] )) # (= [ c ] [ d ] ) # (= a (/ b [ [ [ d ] )) # </table>
(= a (/ b c)) , (= c d)(= a (/ b d))
EqReplaceEq1Minus0 # <title> Substitution </title> # <table> # (= a (- [ b ] ] ] d)) # (= [ b ] [ c ] ) # (= a (- [ [ [ c ] d)) # </table>
(= a (- b d)) , (= b c)(= a (- c d))
EqReplaceEq0Mul0 # <title> Substitution </title> # <table> # (= (* [ a ] ] ] c) d) # (= [ a ] [ b ] ) # (= (* [ [ [ b ] c) d) # </table>
(= (* a c) d) , (= a b)(= (* b c) d)
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= a (+ b [ c ] ] ] )) # (= [ c ] [ d ] ) # (= a (+ b [ [ [ d ] )) # </table>
(= a (+ b c)) , (= c d)(= a (+ b d))
1plus2 # <title> One-digit Addition </title>
(= (+ (1) (2)) (3))
1plus3 # <title> One-digit Addition </title>
(= (+ (1) (3)) (4))
2plus2 # <title> One-digit Addition </title>
(= (+ (2) (2)) (4))
2times2 # <title> One-digit Multiplication </title>
(= (* (2) (2)) (4))
EqReplaceEq0Mul0Mul0 # <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')
EqReplaceEq1Div1Mul0 # <title> Substitution </title> # <table> # (= a (/ b (* [ c ] ] ] a'))) # (= [ c ] [ d ] ) # (= a (/ b (* [ [ [ d ] a'))) # </table>
(= a (/ b (* c a'))) , (= c d)(= a (/ b (* d a')))
EqReplaceEq0Div1 # <title> Substitution </title> # <table> # (= (/ a [ b ] ] ] ) d) # (= [ b ] [ c ] ) # (= (/ a [ [ [ c ] ) d) # </table>
(= (/ a b) d) , (= b c)(= (/ a c) d)
EqReplaceNot0Eq0 # <title> Substitution </title> # <table> # (-. (= [ a ] ] ] c)) # (= [ a ] [ b ] ) # (-. (= [ [ [ b ] c)) # </table>
(-. (= a c)) , (= a b)(-. (= b c))
EqReplaceGe0 # <title> Substitution </title> # <table> # (>= [ a ] ] ] c) # (= [ a ] [ b ] ) # (>= [ [ [ b ] c) # </table>
(>= a c) , (= a b)(>= b c)
sqrtsq2 # <title> Apply Square Root </title>
(-> (= (exp a (2)) b) (= (abs a) (sqrt b)))
sqrtsq3 # <title> Square is the inverse of squaring </title>
(-> (>= a (0)) (= (exp (sqrt a) (2)) a))
EqReplaceBi1Eq0 # <title> Substitution </title> # <table> # (<-> ph (= [ a ] ] ] c)) # (= [ a ] [ b ] ) # (<-> ph (= [ [ [ b ] c)) # </table>
(<-> ph (= a c)) , (= a b)(<-> ph (= b c))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
EqReplaceImp1Bi1Eq0 # <title> Substitution </title> # <table> # (-> ph (<-> ps (= [ a ] ] ] c))) # (= [ a ] [ b ] ) # (-> ph (<-> ps (= [ [ [ b ] c))) # </table>
(-> ph (<-> ps (= a c))) , (= a b)(-> ph (<-> ps (= b c)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
EqReplaceImp1Bi0Eq0 # <title> Substitution </title> # <table> # (-> ph (<-> (= [ a ] ] ] c) ps)) # (= [ a ] [ b ] ) # (-> ph (<-> (= [ [ [ b ] c) ps)) # </table>
(-> ph (<-> (= a c) ps)) , (= a b)(-> ph (<-> (= b c) ps))
sqrtpos2 # <title> Square root of a positive is positive </title>
(-> (> a (0)) (> (sqrt a) (0)))
sqrtReciprocal # <title> Square root over division </title>
(> a (0))(= (/ (1) (sqrt a)) (sqrt (/ (1) a)))
sqrtdivi # <title> Square root over division </title>
(>= a (0)) , (> b (0))(= (sqrt (/ a b)) (/ (sqrt a) (sqrt b)))
EqReplaceImp1Pos0 # <title> Substitution </title> # <table> # (-> ph (pos [ a ] ] ] )) # (= [ a ] [ b ] ) # (-> ph (pos [ [ [ b ] )) # </table>
(-> ph (pos a)) , (= a b)(-> ph (pos b))
sqrtsq4 # <title> Square Root is the inverse of squaring </title>
(= (sqrt (exp a (2))) (abs a))
posDiscriminant # <title> Discriminant is Positive or 0 </title> # <summary> # Proves that if a solution to the quadratic equation exists, the discriminant must # be positive or zero. This repeats part of the proof in the quadratic equation. # </summary>
(= (+ (+ (* a (exp x (2))) (* b x)) c) (0)) , (-. (= a (0)))(>= (- (exp b (2)) (* (* (4) a) c)) (0))
2aSquarePos # <title> Nonnegative Square is positive </title>
(-> (-. (= a (0))) (> (exp (* (2) a) (2)) (0)))
BiReplaceImp0Or1 # <title> Substitution </title> # <table> # (-> (\/ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (\/ ph [ [ [ ch ] ) th) # </table>
(-> (\/ ph ps) th) , (<-> ps ch)(-> (\/ ph ch) th)
ImpReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (-> ps ch)(-> ph (\/ ch th))
BiReplaceImp1Or1 # <title> Substitution </title> # <table> # (-> ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (\/ ps [ [ [ th ] )) # </table>
(-> ph (\/ ps ch)) , (<-> ch th)(-> ph (\/ ps th))
BiReplaceImp1Or1An1 # <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)))
(-. (= b (0)))(-> (= (/ a b) (0)) (= (/ a (abs b)) (/ a b)))
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))
quadraticEq.2 # <summary> # If a fraction and its numerator are both positive, then either the denominator is positive # or the fraction is zero. In either case, an absolute value on the denominator can be eliminated. # </summary>
(-. (= b (0)))(-> (/\ (>= (/ a b) (0)) (>= a (0))) (= (/ a (abs b)) (/ a b)))
ImpReplaceOr0 # <title> Substitution </title> # <table> # (\/ [ ph ] ] ] ch) # (-> [ ph ] [ ps ] ) # (\/ [ [ [ ps ] ch) # </table>
(\/ ph ch) , (-> ph ps)(\/ ps ch)
BiReplaceOr1Or0 # <title> Substitution </title> # <table> # (\/ ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (\/ ph (\/ [ [ [ ch ] th)) # </table>
(\/ ph (\/ ps th)) , (<-> ps ch)(\/ ph (\/ ch th))
BiReplaceOr1Or1 # <title> Substitution </title> # <table> # (\/ ph (\/ ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (\/ ph (\/ ps [ [ [ th ] )) # </table>
(\/ ph (\/ ps ch)) , (<-> ch th)(\/ ph (\/ ps th))
BiReplaceOr0Or1 # <title> Substitution </title> # <table> # (\/ (\/ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (\/ (\/ ph [ [ [ ch ] ) th) # </table>
(\/ (\/ ph ps) th) , (<-> ps ch)(\/ (\/ ph ch) th)
EqReplaceOr0Or1Eq1 # <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)
EqReplaceBi1Eq1 # <title> Substitution </title> # <table> # (<-> ph (= a [ b ] ] ] )) # (= [ b ] [ c ] ) # (<-> ph (= a [ [ [ c ] )) # </table>
(<-> ph (= a b)) , (= b c)(<-> ph (= a c))
EqReplaceOr1Or1Eq1 # <title> Substitution </title> # <table> # (\/ ph (\/ ps (= a [ b ] ] ] ))) # (= [ b ] [ c ] ) # (\/ ph (\/ ps (= a [ [ [ c ] ))) # </table>
(\/ ph (\/ ps (= a b))) , (= b c)(\/ ph (\/ ps (= a c)))
quadraticEq.3 # <title> Two numbers have the same absolute value </title>
(= (abs a) (/ b (abs c))) , (-. (= c (0)))(\/ (= a (/ b c)) (= a (-n (/ b c))))
EqReplaceOr0Eq1 # <title> Substitution </title> # <table> # (\/ (= a [ b ] ] ] ) ph) # (= [ b ] [ c ] ) # (\/ (= a [ [ [ c ] ) ph) # </table>
(\/ (= a b) ph) , (= b c)(\/ (= a c) ph)
EqReplaceEq0Minus0 # <title> Substitution </title> # <table> # (= (- [ a ] ] ] c) d) # (= [ a ] [ b ] ) # (= (- [ [ [ b ] c) d) # </table>
(= (- a c) d) , (= a b)(= (- b c) d)
EqReplaceOr1Eq1 # <title> Substitution </title> # <table> # (\/ ph (= a [ b ] ] ] )) # (= [ b ] [ c ] ) # (\/ ph (= a [ [ [ c ] )) # </table>
(\/ ph (= a b)) , (= b c)(\/ ph (= a c))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= a (* [ b ] ] ] d)) # (= [ b ] [ c ] ) # (= a (* [ [ [ c ] d)) # </table>
(= a (* b d)) , (= b c)(= a (* c d))
quadraticEq # <title> The Quadratic Equation </title> # <summary> # The quadratic equation gives two possible solutions to a second-order polynomial equation. # This proof begins with the assumption that solutions to the equation exists and that the # constant a is not 0. If the value of a were 0, the equation would be linear not quadratic. # </summary>
(= (+ (+ (* a (exp x (2))) (* b x)) c) (0)) , (-. (= a (0)))(\/ (= x (/ (+ (-n b) (sqrt (- (exp b (2)) (* (* (4) a) c)))) (* (2) a))) (= x (/ (- (-n b) (sqrt (- (exp b (2)) (* (* (4) a) c)))) (* (2) a))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)