# List of theorems

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

df-sqrt # <context> # This theorem is part of a series of proofs about the existence of square roots. # The numbers here are all assumed to be real numbers. This theorem is leading up # to a proof that every nonnegative number has exactly one square root. Remember that # square roots are defined to be positive, so -2 is not a square root of 4. First, we # prove that there exists at most one square root. However, the existence proof is not # complete yet. (We've shown there cannot be more than one square root, but haven't yet # ruled out the possibility of there being no square roots for a positive number.) # </context> # <title> Def. Square Root </title>
(= (sqrt A) (iota ({|} x (/\ (= (exp x (2)) A) (>= x (0))))))
EqReplaceImp1Gt0 # <title> Substitution </title> # <table> # (-> ph (> [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (> [ [ [ B ] C)) # </table>
(-> ph (> A C)) , (= A B)(-> ph (> B C))
BiReplaceBi1An0 # <title> Substitution </title> # <table> # (<-> ph (/\ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (/\ [ [ [ ch ] th)) # </table>
(<-> ph (/\ ps th)) , (<-> ps ch)(<-> ph (/\ ch th))
EqReplaceImp1Gt1 # <title> Substitution </title> # <table> # (-> ph (> A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (> A [ [ [ C ] )) # </table>
(-> ph (> A B)) , (= B C)(-> ph (> A C))
sqrtmo.1 # <title> Squares are not equal </title>
(-> (/\ (> A B) (/\ (> A (0)) (> B (0)))) (-. (= (exp A (2)) (exp B (2)))))
BiReplaceImp0An1 # <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)
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
sqrtmo.2 # <title> Squares are not equal </title>
(-> (/\ (-. (= A B)) (/\ (> A (0)) (> B (0)))) (-. (= (exp A (2)) (exp B (2)))))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
BiReplaceBi1Not0Or0 # <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))
sqrtmo.3 # <title> Squares are equal implies equality </title>
(-> (/\ (= (exp A (2)) (exp B (2))) (/\ (> A (0)) (> B (0)))) (= A B))
posSquares2 # <title> Non-zero Squares are positive </title>
(-> (-. (= A (0))) (> (exp A (2)) (0)))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
square0 # <title> Squares are zero, only for zero </title>
(<-> (= A (0)) (= (exp A (2)) (0)))
ImpReplaceImp1An1 # <title> Substitution </title> # <table> # (-> ph (/\ ps [ ch ] ] ] )) # (-> [ ch ] [ th ] ) # (-> ph (/\ ps [ [ [ th ] )) # </table>
(-> ph (/\ ps ch)) , (-> ch th)(-> ph (/\ ps th))
impossibleSq # <title> Squares cannot be zero and positive </title>
(-. (/\ (= (exp A (2)) C) (/\ (= (exp B (2)) C) (/\ (= A (0)) (> B (0))))))
BiReplaceImp0An1An1 # <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)
BiReplaceNot0An1 # <title> Substitution </title> # <table> # (-. (/\ ph [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-. (/\ ph [ [ [ ch ] )) # </table>
(-. (/\ ph ps)) , (<-> ps ch)(-. (/\ ph ch))
BiReplaceNot0An1An1 # <title> Substitution </title> # <table> # (-. (/\ ph (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-. (/\ ph (/\ ps [ [ [ th ] ))) # </table>
(-. (/\ ph (/\ ps ch))) , (<-> ch th)(-. (/\ ph (/\ ps th)))
BiReplaceNot0An0 # <title> Substitution </title> # <table> # (-. (/\ [ ph ] ] ] ch)) # (<-> [ ph ] [ ps ] ) # (-. (/\ [ [ [ ps ] ch)) # </table>
(-. (/\ ph ch)) , (<-> ph ps)(-. (/\ ps ch))
sqrtmo.4 # <title> Equal Squares implies equality </title>
(-> (/\ (= (exp A (2)) C) (/\ (= (exp B (2)) C) (/\ (>= A (0)) (>= B (0))))) (= A B))
sqrtmo # <title> There exists at most one square root </title>
(E* x (/\ (= (exp x (2)) A) (>= x (0))))
EqReplaceBi1Le0 # <title> Substitution </title> # <table> # (<-> ph (<= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (<-> ph (<= [ [ [ B ] C)) # </table>
(<-> ph (<= A C)) , (= A B)(<-> ph (<= B C))
setSquares # <title> Determine when set of squares is empty </title>
(<-> (>= A (0)) (e. (0) ({|} x (<= (exp x (2)) A))))
sqrteq # <title> Equivalence for square root </title>
(-> (= A B) (= (sqrt A) (sqrt B)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)