Home | Metamath
Proof Explorer Theorem List (p. 343 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfwlim 34201 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ β²π₯π & β’ β²π₯π΄ β β’ β²π₯WLim(π , π΄) | ||
Theorem | elwlim 34202 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ (π β WLim(π , π΄) β (π β π΄ β§ π β inf(π΄, π΄, π ) β§ π = sup(Pred(π , π΄, π), π΄, π ))) | ||
Theorem | wzel 34203 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ ((π We π΄ β§ π Se π΄ β§ π΄ β β ) β inf(π΄, π΄, π ) β π΄) | ||
Theorem | wsuclem 34204* | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) & β’ (π β βπ€ β π΄ ππ π€) β β’ (π β βπ₯ β π΄ (βπ¦ β Pred (β‘π , π΄, π) Β¬ π¦π π₯ β§ βπ¦ β π΄ (π₯π π¦ β βπ§ β Pred (β‘π , π΄, π)π§π π¦))) | ||
Theorem | wsucex 34205 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ (π β π Or π΄) β β’ (π β wsuc(π , π΄, π) β V) | ||
Theorem | wsuccl 34206* | If π is a set with an π successor in π΄, then its well-founded successor is a member of π΄. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) & β’ (π β βπ¦ β π΄ ππ π¦) β β’ (π β wsuc(π , π΄, π) β π΄) | ||
Theorem | wsuclb 34207 | A well-founded successor is a lower bound on points after π. (Contributed by Scott Fenton, 16-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
β’ (π β π We π΄) & β’ (π β π Se π΄) & β’ (π β π β π) & β’ (π β π β π΄) & β’ (π β ππ π) β β’ (π β Β¬ ππ wsuc(π , π΄, π)) | ||
Theorem | wlimss 34208 | The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.) |
β’ WLim(π , π΄) β π΄ | ||
Syntax | cnadd 34209 | Declare the syntax for natural ordinal addition. See df-nadd 34210. |
class +no | ||
Definition | df-nadd 34210* | Define natural ordinal addition. This is a commutative form of addition over the ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ +no = frecs({β¨π₯, π¦β© β£ (π₯ β (On Γ On) β§ π¦ β (On Γ On) β§ (((1st βπ₯) E (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯) E (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))}, (On Γ On), (π§ β V, π β V β¦ β© {π€ β On β£ ((π β ({(1st βπ§)} Γ (2nd βπ§))) β π€ β§ (π β ((1st βπ§) Γ {(2nd βπ§)})) β π€)})) | ||
Theorem | on2recsfn 34211* | Show that double recursion over ordinals yields a function over pairs of ordinals. (Contributed by Scott Fenton, 3-Sep-2024.) |
β’ πΉ = frecs({β¨π₯, π¦β© β£ (π₯ β (On Γ On) β§ π¦ β (On Γ On) β§ (((1st βπ₯) E (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯) E (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))}, (On Γ On), πΊ) β β’ πΉ Fn (On Γ On) | ||
Theorem | on2recsov 34212* | Calculate the value of the double ordinal recursion operator. (Contributed by Scott Fenton, 3-Sep-2024.) |
β’ πΉ = frecs({β¨π₯, π¦β© β£ (π₯ β (On Γ On) β§ π¦ β (On Γ On) β§ (((1st βπ₯) E (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯) E (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))}, (On Γ On), πΊ) β β’ ((π΄ β On β§ π΅ β On) β (π΄πΉπ΅) = (β¨π΄, π΅β©πΊ(πΉ βΎ ((suc π΄ Γ suc π΅) β {β¨π΄, π΅β©})))) | ||
Theorem | on2ind 34213* | Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β On β§ π β On) β ((βπ β π βπ β π π β§ βπ β π π β§ βπ β π π) β π)) β β’ ((π β On β§ π β On) β π) | ||
Theorem | on3ind 34214* | Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024.) |
β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β On β§ π β On β§ π β On) β (((βπ β π βπ β π βπ β π π β§ βπ β π βπ β π π β§ βπ β π βπ β π π) β§ (βπ β π π β§ βπ β π βπ β π π β§ βπ β π π) β§ βπ β π π) β π)) β β’ ((π β On β§ π β On β§ π β On) β π) | ||
Theorem | coflton 34215* | Cofinality theorem for ordinals. If π΄ is cofinal with π΅ and π΅ precedes πΆ, then π΄ precedes πΆ. Compare cofsslt 27155 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ (π β πΆ β On) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) & β’ (π β βπ§ β π΅ βπ€ β πΆ π§ β π€) β β’ (π β βπ β π΄ βπ β πΆ π β π) | ||
Theorem | cofon1 34216* | Cofinality theorem for ordinals. If π΄ is cofinal with π΅ and the upper bound of π΄ dominates π΅, then their upper bounds are equal. Compare with cofcut1 27157 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β π« On) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) & β’ (π β π΅ β β© {π§ β On β£ π΄ β π§}) β β’ (π β β© {π§ β On β£ π΄ β π§} = β© {π€ β On β£ π΅ β π€}) | ||
Theorem | cofon2 34217* | Cofinality theorem for ordinals. If π΄ and π΅ are mutually cofinal, then their upper bounds agree. Compare cofcut2 27159 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β π« On) & β’ (π β π΅ β π« On) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) & β’ (π β βπ§ β π΅ βπ€ β π΄ π§ β π€) β β’ (π β β© {π β On β£ π΄ β π} = β© {π β On β£ π΅ β π}) | ||
Theorem | cofonr 34218* | Inverse cofinality law for ordinals. Contrast with cofcutr 27161 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β On) & β’ (π β π΄ = β© {π₯ β On β£ π β π₯}) β β’ (π β βπ¦ β π΄ βπ§ β π π¦ β π§) | ||
Theorem | naddfn 34219 | Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ +no Fn (On Γ On) | ||
Theorem | naddcllem 34220* | Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ +no π΅) β On β§ (π΄ +no π΅) = β© {π₯ β On β£ (( +no β ({π΄} Γ π΅)) β π₯ β§ ( +no β (π΄ Γ {π΅})) β π₯)})) | ||
Theorem | naddcl 34221 | Closure law for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) β On) | ||
Theorem | naddov 34222* | The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π₯ β On β£ (( +no β ({π΄} Γ π΅)) β π₯ β§ ( +no β (π΄ Γ {π΅})) β π₯)}) | ||
Theorem | naddov2 34223* | Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π₯ β On β£ (βπ¦ β π΅ (π΄ +no π¦) β π₯ β§ βπ§ β π΄ (π§ +no π΅) β π₯)}) | ||
Theorem | naddov3 34224* | Alternate expression for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π₯ β On β£ (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅}))) β π₯}) | ||
Theorem | naddf 34225 | Function statement for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ +no :(On Γ On)βΆOn | ||
Theorem | naddcom 34226 | Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = (π΅ +no π΄)) | ||
Theorem | naddid1 34227 | Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ (π΄ β On β (π΄ +no β ) = π΄) | ||
Theorem | naddssim 34228 | Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddelim 34229 | Ordinal less-than is preserved by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddel1 34230 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddel2 34231 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (πΆ +no π΄) β (πΆ +no π΅))) | ||
Theorem | naddss1 34232 | Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddss2 34233 | Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (πΆ +no π΄) β (πΆ +no π΅))) | ||
Theorem | naddword1 34234 | Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β π΄ β (π΄ +no π΅)) | ||
Theorem | naddunif 34235* | Uniformity theorem for natural addition. If π΄ is the upper bound of π and π΅ is the upper bound of π, then (π΄ +no π΅) can be expressed in terms of π and π. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ (π β π΄ = β© {π₯ β On β£ π β π₯}) & β’ (π β π΅ = β© {π¦ β On β£ π β π¦}) β β’ (π β (π΄ +no π΅) = β© {π§ β On β£ (( +no β (π Γ {π΅})) βͺ ( +no β ({π΄} Γ π))) β π§}) | ||
Theorem | naddasslem1 34236* | Lemma for naddass 34238. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ +no π΅) +no πΆ) = β© {π₯ β On β£ (βπ β π΄ ((π +no π΅) +no πΆ) β π₯ β§ βπ β π΅ ((π΄ +no π) +no πΆ) β π₯ β§ βπ β πΆ ((π΄ +no π΅) +no π) β π₯)}) | ||
Theorem | naddasslem2 34237* | Lemma for naddass 34238. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ +no (π΅ +no πΆ)) = β© {π₯ β On β£ (βπ β π΄ (π +no (π΅ +no πΆ)) β π₯ β§ βπ β π΅ (π΄ +no (π +no πΆ)) β π₯ β§ βπ β πΆ (π΄ +no (π΅ +no π)) β π₯)}) | ||
Theorem | naddass 34238 | Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ +no π΅) +no πΆ) = (π΄ +no (π΅ +no πΆ))) | ||
Theorem | nadd32 34239 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ +no π΅) +no πΆ) = ((π΄ +no πΆ) +no π΅)) | ||
Syntax | cnorec 34240 | Declare the syntax for surreal recursion of one variable. |
class norec (πΉ) | ||
Definition | df-norec 34241* | Define the recursion generator for surreal functions of one variable. This generator creates a recursive function of surreals from their value on their left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ norec (πΉ) = frecs({β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))}, No , πΉ) | ||
Theorem | lrrecval 34242* | The next step in the development of the surreals is to establish induction and recursion across left and right sets. To that end, we are going to develop a relationship π that is founded, partial, and set-like across the surreals. This first theorem just establishes the value of π . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ ((π΄ β No β§ π΅ β No ) β (π΄π π΅ β π΄ β (( L βπ΅) βͺ ( R βπ΅)))) | ||
Theorem | lrrecval2 34243* | Next, we establish an alternate expression for π . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ ((π΄ β No β§ π΅ β No ) β (π΄π π΅ β ( bday βπ΄) β ( bday βπ΅))) | ||
Theorem | lrrecpo 34244* | Now, we establish that π is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ π Po No | ||
Theorem | lrrecse 34245* | Next, we show that π is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ π Se No | ||
Theorem | lrrecfr 34246* | Now we show that π is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ π Fr No | ||
Theorem | lrrecpred 34247* | Finally, we calculate the value of the predecessor class over π . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ (π΄ β No β Pred(π , No , π΄) = (( L βπ΄) βͺ ( R βπ΄))) | ||
Theorem | noinds 34248* | Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π₯ β No β (βπ¦ β (( L βπ₯) βͺ ( R βπ₯))π β π)) β β’ (π΄ β No β π) | ||
Theorem | norecfn 34249 | Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ πΉ = norec (πΊ) β β’ πΉ Fn No | ||
Theorem | norecov 34250 | Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ πΉ = norec (πΊ) β β’ (π΄ β No β (πΉβπ΄) = (π΄πΊ(πΉ βΎ (( L βπ΄) βͺ ( R βπ΄))))) | ||
Syntax | cnorec2 34251 | Declare the syntax for surreal recursion on two arguments. |
class norec2 (πΉ) | ||
Definition | df-norec2 34252* | Define surreal recursion on two variables. This function is key to the development of most of surreal numbers. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ norec2 (πΉ) = frecs({β¨π, πβ© β£ (π β ( No Γ No ) β§ π β ( No Γ No ) β§ (((1st βπ){β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} (1st βπ) β¨ (1st βπ) = (1st βπ)) β§ ((2nd βπ){β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} (2nd βπ) β¨ (2nd βπ) = (2nd βπ)) β§ π β π))}, ( No Γ No ), πΉ) | ||
Theorem | noxpordpo 34253* | To get through most of the textbook defintions in surreal numbers we will need recursion on two variables. This set of theorems sets up the preconditions for double recursion. This theorem establishes the partial ordering. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} & β’ π = {β¨π₯, π¦β© β£ (π₯ β ( No Γ No ) β§ π¦ β ( No Γ No ) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ π Po ( No Γ No ) | ||
Theorem | noxpordfr 34254* | Next we establish the foundedness of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} & β’ π = {β¨π₯, π¦β© β£ (π₯ β ( No Γ No ) β§ π¦ β ( No Γ No ) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ π Fr ( No Γ No ) | ||
Theorem | noxpordse 34255* | Next we establish the set-like nature of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} & β’ π = {β¨π₯, π¦β© β£ (π₯ β ( No Γ No ) β§ π¦ β ( No Γ No ) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ π Se ( No Γ No ) | ||
Theorem | noxpordpred 34256* | Next we calculate the predecessor class of the relationship. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} & β’ π = {β¨π₯, π¦β© β£ (π₯ β ( No Γ No ) β§ π¦ β ( No Γ No ) β§ (((1st βπ₯)π (1st βπ¦) β¨ (1st βπ₯) = (1st βπ¦)) β§ ((2nd βπ₯)π (2nd βπ¦) β¨ (2nd βπ₯) = (2nd βπ¦)) β§ π₯ β π¦))} β β’ ((π΄ β No β§ π΅ β No ) β Pred(π, ( No Γ No ), β¨π΄, π΅β©) = ((((( L βπ΄) βͺ ( R βπ΄)) βͺ {π΄}) Γ ((( L βπ΅) βͺ ( R βπ΅)) βͺ {π΅})) β {β¨π΄, π΅β©})) | ||
Theorem | no2indslem 34257* | Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ π = {β¨π, πβ© β£ π β (( L βπ) βͺ ( R βπ))} & β’ π = {β¨π, πβ© β£ (π β ( No Γ No ) β§ π β ( No Γ No ) β§ (((1st βπ)π (1st βπ) β¨ (1st βπ) = (1st βπ)) β§ ((2nd βπ)π (2nd βπ) β¨ (2nd βπ) = (2nd βπ)) β§ π β π))} & β’ (π₯ = π§ β (π β π)) & β’ (π¦ = π€ β (π β π)) & β’ (π₯ = π§ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ ((π₯ β No β§ π¦ β No ) β ((βπ§ β (( L βπ₯) βͺ ( R βπ₯))βπ€ β (( L βπ¦) βͺ ( R βπ¦))π β§ βπ§ β (( L βπ₯) βͺ ( R βπ₯))π β§ βπ€ β (( L βπ¦) βͺ ( R βπ¦))π) β π)) β β’ ((π΄ β No β§ π΅ β No ) β π) | ||
Theorem | no2inds 34258* | Double induction on surreals. The many substitution instances are to cover all possible cases. (Contributed by Scott Fenton, 22-Aug-2024.) |
β’ (π₯ = π§ β (π β π)) & β’ (π¦ = π€ β (π β π)) & β’ (π₯ = π§ β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ (π¦ = π΅ β (π β π)) & β’ ((π₯ β No β§ π¦ β No ) β ((βπ§ β (( L βπ₯) βͺ ( R βπ₯))βπ€ β (( L βπ¦) βͺ ( R βπ¦))π β§ βπ§ β (( L βπ₯) βͺ ( R βπ₯))π β§ βπ€ β (( L βπ¦) βͺ ( R βπ¦))π) β π)) β β’ ((π΄ β No β§ π΅ β No ) β π) | ||
Theorem | norec2fn 34259 | The double-recursion operator on surreals yields a function on pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ πΉ = norec2 (πΊ) β β’ πΉ Fn ( No Γ No ) | ||
Theorem | norec2ov 34260 | The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ πΉ = norec2 (πΊ) β β’ ((π΄ β No β§ π΅ β No ) β (π΄πΉπ΅) = (β¨π΄, π΅β©πΊ(πΉ βΎ ((((( L βπ΄) βͺ ( R βπ΄)) βͺ {π΄}) Γ ((( L βπ΅) βͺ ( R βπ΅)) βͺ {π΅})) β {β¨π΄, π΅β©})))) | ||
Theorem | no3inds 34261* | Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-2024.) |
β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β No β§ π β No β§ π β No ) β (((βπ β (( L βπ) βͺ ( R βπ))βπ β (( L βπ) βͺ ( R βπ))βπ β (( L βπ) βͺ ( R βπ))π β§ βπ β (( L βπ) βͺ ( R βπ))βπ β (( L βπ) βͺ ( R βπ))π β§ βπ β (( L βπ) βͺ ( R βπ))βπ β (( L βπ) βͺ ( R βπ))π) β§ (βπ β (( L βπ) βͺ ( R βπ))π β§ βπ β (( L βπ) βͺ ( R βπ))βπ β (( L βπ) βͺ ( R βπ))π β§ βπ β (( L βπ) βͺ ( R βπ))π) β§ βπ β (( L βπ) βͺ ( R βπ))π) β π)) β β’ ((π β No β§ π β No β§ π β No ) β π) | ||
Syntax | cadds 34262 | Declare the syntax for surreal addition. |
class +s | ||
Definition | df-adds 34263* | Define surreal addition. This is the first of the field operations on the surreals. Definition from [Conway] p. 5. Definition from [Gonshor] p. 13. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ +s = norec2 ((π₯ β V, π β V β¦ (({π¦ β£ βπ β ( L β(1st βπ₯))π¦ = (ππ(2nd βπ₯))} βͺ {π§ β£ βπ β ( L β(2nd βπ₯))π§ = ((1st βπ₯)ππ)}) |s ({π¦ β£ βπ β ( R β(1st βπ₯))π¦ = (ππ(2nd βπ₯))} βͺ {π§ β£ βπ β ( R β(2nd βπ₯))π§ = ((1st βπ₯)ππ)})))) | ||
Theorem | addsfn 34264 | Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ +s Fn ( No Γ No ) | ||
Theorem | addsval 34265* | The value of surreal addition. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ +s π΅) = (({π¦ β£ βπ β ( L βπ΄)π¦ = (π +s π΅)} βͺ {π§ β£ βπ β ( L βπ΅)π§ = (π΄ +s π)}) |s ({π¦ β£ βπ β ( R βπ΄)π¦ = (π +s π΅)} βͺ {π§ β£ βπ β ( R βπ΅)π§ = (π΄ +s π)}))) | ||
Theorem | addsval2 34266* | The value of surreal addition with different choices for each bound variable. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ +s π΅) = (({π¦ β£ βπ β ( L βπ΄)π¦ = (π +s π΅)} βͺ {π§ β£ βπ β ( L βπ΅)π§ = (π΄ +s π)}) |s ({π€ β£ βπ β ( R βπ΄)π€ = (π +s π΅)} βͺ {π‘ β£ βπ β ( R βπ΅)π‘ = (π΄ +s π )}))) | ||
Theorem | addsid1 34267 | Surreal addition to zero is identity. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ (π΄ β No β (π΄ +s 0s ) = π΄) | ||
Theorem | addsid1d 34268 | Surreal addition to zero is identity. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ (π β π΄ β No ) β β’ (π β (π΄ +s 0s ) = π΄) | ||
Theorem | addscom 34269 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ +s π΅) = (π΅ +s π΄)) | ||
Theorem | addscomd 34270 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) β β’ (π β (π΄ +s π΅) = (π΅ +s π΄)) | ||
Theorem | addsproplem1 34271* | Lemma for surreal addition properties. To prove closure on surreal addition we need to prove that addition is compatible with order at the same time. We do this by inducting over the maximum of two natural sums of the birthdays of surreals numbers. In the final step we will loop around and use tfr3 8312 to prove this of all surreals. This first lemma just instantiates the inductive hypothesis so we do not need to do it continuously throughout the proof. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) & β’ (π β ((( bday βπ΄) +no ( bday βπ΅)) βͺ (( bday βπ΄) +no ( bday βπΆ))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ)))) β β’ (π β ((π΄ +s π΅) β No β§ (π΅ <s πΆ β (π΅ +s π΄) <s (πΆ +s π΄)))) | ||
Theorem | addsproplem2 34272* | Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2, it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π β No ) & β’ (π β π β No ) β β’ (π β ({π β£ βπ β ( L βπ)π = (π +s π)} βͺ {π β£ βπ β ( L βπ)π = (π +s π)}) <<s ({π€ β£ βπ β ( R βπ)π€ = (π +s π)} βͺ {π‘ β£ βπ β ( R βπ)π‘ = (π +s π )})) | ||
Theorem | addsproplem3 34273* | Lemma for surreal addition properties. Show the cut properties of surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π β No ) & β’ (π β π β No ) β β’ (π β ((π +s π) β No β§ ({π β£ βπ β ( L βπ)π = (π +s π)} βͺ {π β£ βπ β ( L βπ)π = (π +s π)}) <<s {(π +s π)} β§ {(π +s π)} <<s ({π€ β£ βπ β ( R βπ)π€ = (π +s π)} βͺ {π‘ β£ βπ β ( R βπ)π‘ = (π +s π )}))) | ||
Theorem | addsproplem4 34274* | Lemma for surreal addition properties. Show the second half of the inductive hypothesis when π is older than π. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π <s π) & β’ (π β ( bday βπ) β ( bday βπ)) β β’ (π β (π +s π) <s (π +s π)) | ||
Theorem | addsproplem5 34275* | Lemma for surreal addition properties. Show the second half of the inductive hypothesis when π is older than π. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π <s π) & β’ (π β ( bday βπ) β ( bday βπ)) β β’ (π β (π +s π) <s (π +s π)) | ||
Theorem | addsproplem6 34276* | Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when π and π are the same age. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π <s π) & β’ (π β ( bday βπ) = ( bday βπ)) β β’ (π β (π +s π) <s (π +s π)) | ||
Theorem | addsproplem7 34277* | Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β βπ₯ β No βπ¦ β No βπ§ β No (((( bday βπ₯) +no ( bday βπ¦)) βͺ (( bday βπ₯) +no ( bday βπ§))) β ((( bday βπ) +no ( bday βπ)) βͺ (( bday βπ) +no ( bday βπ))) β ((π₯ +s π¦) β No β§ (π¦ <s π§ β (π¦ +s π₯) <s (π§ +s π₯))))) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π β No ) & β’ (π β π <s π) β β’ (π β (π +s π) <s (π +s π)) | ||
Theorem | addsprop 34278 | Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of [Gonshor] p. 14. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π β No β§ π β No β§ π β No ) β ((π +s π) β No β§ (π <s π β (π +s π) <s (π +s π)))) | ||
Theorem | addscut 34279* | Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β π β No ) & β’ (π β π β No ) β β’ (π β ((π +s π) β No β§ ({π β£ βπ β ( L βπ)π = (π +s π)} βͺ {π β£ βπ β ( L βπ)π = (π +s π)}) <<s {(π +s π)} β§ {(π +s π)} <<s ({π€ β£ βπ β ( R βπ)π€ = (π +s π)} βͺ {π‘ β£ βπ β ( R βπ)π‘ = (π +s π )}))) | ||
Theorem | addscld 34280 | Surreal numbers are closed under addition. Theorem 6(iii) of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β π β No ) & β’ (π β π β No ) β β’ (π β (π +s π) β No ) | ||
Theorem | addscl 34281 | Surreal numbers are closed under addition. Theorem 6(iii) of [Conway[ p. 18. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ +s π΅) β No ) | ||
Theorem | addsf 34282 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ +s :( No Γ No )βΆ No | ||
Theorem | addsfo 34283 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ +s :( No Γ No )βontoβ No | ||
Theorem | sltadd1im 34284 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (π΄ +s πΆ) <s (π΅ +s πΆ))) | ||
Theorem | sltadd2im 34285 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (πΆ +s π΄) <s (πΆ +s π΅))) | ||
Theorem | sleadd1im 34286 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((π΄ +s πΆ) β€s (π΅ +s πΆ) β π΄ β€s π΅)) | ||
Theorem | sleadd2im 34287 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((πΆ +s π΄) β€s (πΆ +s π΅) β π΄ β€s π΅)) | ||
Theorem | sleadd1 34288 | Addition to both sides of surreal less-than or equal. Theorem 5 of [Conway] p. 18. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ β€s π΅ β (π΄ +s πΆ) β€s (π΅ +s πΆ))) | ||
Theorem | sleadd2 34289 | Addition to both sides of surreal less-than or equal. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ β€s π΅ β (πΆ +s π΄) β€s (πΆ +s π΅))) | ||
Theorem | sltadd2 34290 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (πΆ +s π΄) <s (πΆ +s π΅))) | ||
Theorem | sltadd1 34291 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (π΄ +s πΆ) <s (π΅ +s πΆ))) | ||
Theorem | addscan2 34292 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((π΄ +s πΆ) = (π΅ +s πΆ) β π΄ = π΅)) | ||
Theorem | addscan1 34293 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((πΆ +s π΄) = (πΆ +s π΅) β π΄ = π΅)) | ||
Theorem | addsunif 34294* | Uniformity theorem for surreal addition. This theorem states that we can use any cuts that define π΄ and π΅ in the definition of surreal addition. Theorem 3.2 of [Gonshor] p. 15. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β πΏ <<s π ) & β’ (π β π <<s π) & β’ (π β π΄ = (πΏ |s π )) & β’ (π β π΅ = (π |s π)) β β’ (π β (π΄ +s π΅) = (({π¦ β£ βπ β πΏ π¦ = (π +s π΅)} βͺ {π§ β£ βπ β π π§ = (π΄ +s π)}) |s ({π€ β£ βπ β π π€ = (π +s π΅)} βͺ {π‘ β£ βπ β π π‘ = (π΄ +s π )}))) | ||
Theorem | addsasslem1 34295* | Lemma for addition associativity. Expand one form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) β β’ (π β ((π΄ +s π΅) +s πΆ) = ((({π¦ β£ βπ β ( L βπ΄)π¦ = ((π +s π΅) +s πΆ)} βͺ {π§ β£ βπ β ( L βπ΅)π§ = ((π΄ +s π) +s πΆ)}) βͺ {π€ β£ βπ β ( L βπΆ)π€ = ((π΄ +s π΅) +s π)}) |s (({π β£ βπ β ( R βπ΄)π = ((π +s π΅) +s πΆ)} βͺ {π β£ βπ β ( R βπ΅)π = ((π΄ +s π) +s πΆ)}) βͺ {π β£ βπ β ( R βπΆ)π = ((π΄ +s π΅) +s π)}))) | ||
Theorem | addsasslem2 34296* | Lemma for addition associativity. Expand the other form of the triple sum. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) β β’ (π β (π΄ +s (π΅ +s πΆ)) = ((({π¦ β£ βπ β ( L βπ΄)π¦ = (π +s (π΅ +s πΆ))} βͺ {π§ β£ βπ β ( L βπ΅)π§ = (π΄ +s (π +s πΆ))}) βͺ {π€ β£ βπ β ( L βπΆ)π€ = (π΄ +s (π΅ +s π))}) |s (({π β£ βπ β ( R βπ΄)π = (π +s (π΅ +s πΆ))} βͺ {π β£ βπ β ( R βπ΅)π = (π΄ +s (π +s πΆ))}) βͺ {π β£ βπ β ( R βπΆ)π = (π΄ +s (π΅ +s π))}))) | ||
Theorem | addsass 34297 | Surreal addition is associative. Part of theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 22-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((π΄ +s π΅) +s πΆ) = (π΄ +s (π΅ +s πΆ))) | ||
Theorem | addsassd 34298 | Surreal addition is associative. Part of theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 22-Jan-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) β β’ (π β ((π΄ +s π΅) +s πΆ) = (π΄ +s (π΅ +s πΆ))) | ||
Theorem | adds32d 34299 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 22-Jan-2025.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) & β’ (π β πΆ β No ) β β’ (π β ((π΄ +s π΅) +s πΆ) = ((π΄ +s πΆ) +s π΅)) | ||
Syntax | cnegs 34300 | Declare the syntax for surreal negation. |
class -us |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |