# List of theorems

List of theorems in peano_new/arithmetic/reals/supremum-def.gh:

df-upperbound-just # <context> # This theorem is part of a series of proofs that define the upperbound and # supremum of a set. We also prove that there is at most one supremum for each # set. This does not rule out the possibility of a set having no supremum. At # this point, we have not introduced the completeness axiom which states that # a supremum exists for every nonempty set with an upperbound. So these theorems # are valid for naturals, integers, and rational numbers. # </context>
(<-> (A. x (-> (e. x S) (<= x A))) (A. y (-> (e. y S) (<= y A))))
df-upperbound # <title> Def. Set Upper Bound </title> # <summary> # A number is an upper bound for a set if all numbers in that set are below it. # For example, 0 and 1 are both upper bounds for the set of negative numbers. # </summary>
(<-> (upperbound A S) (A. x (-> (e. x S) (<= x A))))
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))
upperboundeq1 # <title> Equivalence for upperbound </title> ##
(-> (= A B) (<-> (upperbound A S) (upperbound B S)))
upperboundseq2 # <title> Equivalence for upperbound </title> ##
(-> (=_ S T) (<-> (upperbound A S) (upperbound A T)))
BiReplaceBi1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. [ [ [ ch ] )) # </table>
(<-> ph (-. ps)) , (<-> ps ch)(<-> ph (-. ch))
BiReplaceBi1Not0Ex1 # <title> Substitution </title> # <table> # (<-> ph (-. (E. x [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (E. x [ [ [ ch ] ))) # </table>
(<-> ph (-. (E. x ps))) , (<-> ps ch)(<-> ph (-. (E. x ch)))
BiReplaceBi1Not0Ex1Not0 # <title> Substitution </title> # <table> # (<-> ph (-. (E. x (-. [ ps ] ] ] )))) # (<-> [ ps ] [ ch ] ) # (<-> ph (-. (E. x (-. [ [ [ ch ] )))) # </table>
(<-> ph (-. (E. x (-. ps)))) , (<-> ps ch)(<-> ph (-. (E. x (-. ch))))
BiReplaceBi1Not0Ex1An1 # <title> Substitution </title> # <table> # (<-> ph (-. (E. x (/\ ps [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (E. x (/\ ps [ [ [ th ] )))) # </table>
(<-> ph (-. (E. x (/\ ps ch)))) , (<-> ch th)(<-> ph (-. (E. x (/\ ps th))))
dfupperbound1 # <title> Alternative Upper Bound Definition </title>
(<-> (upperbound A S) (-. (E. x (/\ (e. x S) (> x A)))))
(<-> (/\ (upperbound A S) (-. (E. x (/\ (upperbound x S) (< x A))))) (/\ (upperbound A S) (-. (E. y (/\ (upperbound y S) (< y A))))))
df-supremum # <title> Supremum Definition </title> # <summary> # Define the supremum as a number that is an upper bound of a set and no other upper # bounds are beneath it. This defines a Boolean expression that is true when A is the # supremum of S. <a href="../supremum.gh/df-sup">df-supremum </a> is a related definition # that takes a set and returns its supremum. This definition exists because we have not yet # proved that <a href="supremummo">there can not be multiple supremums</a>. # </summary>
(<-> (supremum A S) (/\ (upperbound A S) (-. (E. x (/\ (upperbound x S) (< x A))))))
(-> ph (=_ S T))(-> ph (<-> (upperbound A S) (upperbound A T)))
(-> ph (= A B))(-> ph (<-> (upperbound A S) (upperbound B S)))
supremumeq1 # <title> Equivalence for supremum </title> ##
(-> (= A B) (<-> (supremum A S) (supremum B S)))
supremumseq2 # <title> Equivalence for supremum </title> ##
(-> (=_ S T) (<-> (supremum A S) (supremum A T)))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
BiReplaceImp1Not0Ex1 # <title> Substitution </title> # <table> # (-> ph (-. (E. x [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (-> ph (-. (E. x [ [ [ ch ] ))) # </table>
(-> ph (-. (E. x ps))) , (<-> ps ch)(-> ph (-. (E. x ch)))
BiReplaceImp1Not0Ex1An0 # <title> Substitution </title> # <table> # (-> ph (-. (E. x (/\ [ ps ] ] ] th)))) # (<-> [ ps ] [ ch ] ) # (-> ph (-. (E. x (/\ [ [ [ ch ] th)))) # </table>
(-> ph (-. (E. x (/\ ps th)))) , (<-> ps ch)(-> ph (-. (E. x (/\ ch th))))
BiReplaceImp1Al1 # <title> Substitution </title> # <table> # (-> ph (A. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x [ [ [ ch ] )) # </table>
(-> ph (A. x ps)) , (<-> ps ch)(-> ph (A. x ch))
BiReplaceImp1Al1Not0 # <title> Substitution </title> # <table> # (-> ph (A. x (-. [ ps ] ] ] ))) # (<-> [ ps ] [ ch ] ) # (-> ph (A. x (-. [ [ [ ch ] ))) # </table>
(-> ph (A. x (-. ps))) , (<-> ps ch)(-> ph (A. x (-. ch)))
BiReplaceImp1Al1Imp1 # <title> Substitution </title> # <table> # (-> ph (A. x (-> ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (A. x (-> ps [ [ [ th ] ))) # </table>
(-> ph (A. x (-> ps ch))) , (<-> ch th)(-> ph (A. x (-> ps th)))
BiReplaceImp1Al1Imp1Not0 # <title> Substitution </title> # <table> # (-> ph (A. x (-> ps (-. [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (-> ph (A. x (-> ps (-. [ [ [ th ] )))) # </table>
(-> ph (A. x (-> ps (-. ch)))) , (<-> ch th)(-> ph (A. x (-> ps (-. th))))
BiReplaceImp1Al1Imp1Ex1 # <title> Substitution </title> # <table> # (-> ph (A. x (-> ps (E. y [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (-> ph (A. x (-> ps (E. y [ [ [ th ] )))) # </table>
(-> ph (A. x (-> ps (E. y ch)))) , (<-> ch th)(-> ph (A. x (-> ps (E. y th))))
BiReplaceImp1Al1Imp1Ex1Not0 # <title> Substitution </title> # <table> # (-> ph (A. x (-> ps (E. y (-. [ ch ] ] ] ))))) # (<-> [ ch ] [ th ] ) # (-> ph (A. x (-> ps (E. y (-. [ [ [ th ] ))))) # </table>
(-> ph (A. x (-> ps (E. y (-. ch))))) , (<-> ch th)(-> ph (A. x (-> ps (E. y (-. th)))))
BiReplaceImp1Al1Imp1Ex1Not0Imp0 # <title> Substitution </title> # <table> # (-> ph (A. x (-> ps (E. y (-. (-> [ ch ] ] ] ta)))))) # (<-> [ ch ] [ th ] ) # (-> ph (A. x (-> ps (E. y (-. (-> [ [ [ th ] ta)))))) # </table>
(-> ph (A. x (-> ps (E. y (-. (-> ch ta)))))) , (<-> ch th)(-> ph (A. x (-> ps (E. y (-. (-> th ta))))))
BiReplaceImp1Al1Imp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (A. x (-> ps (E. y (/\ ch [ th ] ] ] ))))) # (<-> [ th ] [ ta ] ) # (-> ph (A. x (-> ps (E. y (/\ ch [ [ [ ta ] ))))) # </table>
(-> ph (A. x (-> ps (E. y (/\ ch th))))) , (<-> th ta)(-> ph (A. x (-> ps (E. y (/\ ch ta)))))
leastUpperBound # <title> Alternative Least Upper Bound Definition </title>
(-> (supremum A S) (A. x (-> (< x A) (E. y (/\ (e. y S) (> y x))))))
belowSupremum # <title> No upper bounds below the supremum </title> # <summary> # For any number A - ϵ that is below the supremum is not an upper bound and # so there is a number in the set that is above A-ϵ. # </summary>
(-> (/\ (> ep (0)) (supremum A S)) (E. y (/\ (e. y S) (> y (- A ep)))))
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (<-> ps ch)(-> ph (E. x ch))
BiReplaceImp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (E. x (/\ ps ch))) , (<-> ch th)(-> ph (E. x (/\ ps th)))
EqReplaceImp1Ex1An1Gt1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ ps (> A [ B ] ] ] )))) # (= [ B ] [ C ] ) # (-> ph (E. x (/\ ps (> A [ [ [ C ] )))) # </table>
(-> ph (E. x (/\ ps (> A B)))) , (= B C)(-> ph (E. x (/\ ps (> A C))))
EqReplaceImp1Ex1An1Gt1Add1 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ ps (> A (+ B [ C ] ] ] ))))) # (= [ C ] [ D ] ) # (-> ph (E. x (/\ ps (> A (+ B [ [ [ D ] ))))) # </table>
(-> ph (E. x (/\ ps (> A (+ B C))))) , (= C D)(-> ph (E. x (/\ ps (> A (+ B D)))))
supremummo.1 # <title> A supremum has no supremums below it </title>
(-> (/\ (> A B) (supremum A S)) (-. (supremum B S)))
BiReplaceImp1Or0 # <title> Substitution </title> # <table> # (-> ph (\/ [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (\/ [ [ [ ch ] th)) # </table>
(-> ph (\/ ps th)) , (<-> ps ch)(-> ph (\/ ch th))
BiReplaceImp1Or0Not0 # <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))
supremummo.2 # <title> A supremum has no supremums below it </title>
(-> (/\ (supremum A S) (supremum B S)) (<= B A))
supremummo # <title> There is at most one supremum </title>
(E* x (supremum x S))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)