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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | on2ind 34201* | Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β On β§ π β On) β ((βπ β π βπ β π π β§ βπ β π π β§ βπ β π π) β π)) β β’ ((π β On β§ π β On) β π) | ||
Theorem | on3ind 34202* | Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024.) |
β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ (π = π β (π β π)) & β’ ((π β On β§ π β On β§ π β On) β (((βπ β π βπ β π βπ β π π β§ βπ β π βπ β π π β§ βπ β π βπ β π π) β§ (βπ β π π β§ βπ β π βπ β π π β§ βπ β π π) β§ βπ β π π) β π)) β β’ ((π β On β§ π β On β§ π β On) β π) | ||
Theorem | coflton 34203* | Cofinality theorem for ordinals. If π΄ is cofinal with π΅ and π΅ precedes πΆ, then π΄ precedes πΆ. Compare cofsslt 34228 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β On) & β’ (π β π΅ β On) & β’ (π β πΆ β On) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) & β’ (π β βπ§ β π΅ βπ€ β πΆ π§ β π€) β β’ (π β βπ β π΄ βπ β πΆ π β π) | ||
Theorem | cofon1 34204* | Cofinality theorem for ordinals. If π΄ is cofinal with π΅ and the upper bound of π΄ dominates π΅, then their upper bounds are equal. Compare with cofcut1 34230 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β π« On) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) & β’ (π β π΅ β β© {π§ β On β£ π΄ β π§}) β β’ (π β β© {π§ β On β£ π΄ β π§} = β© {π€ β On β£ π΅ β π€}) | ||
Theorem | cofon2 34205* | Cofinality theorem for ordinals. If π΄ and π΅ are mutually cofinal, then their upper bounds agree. Compare cofcut2 34231 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β π« On) & β’ (π β π΅ β π« On) & β’ (π β βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦) & β’ (π β βπ§ β π΅ βπ€ β π΄ π§ β π€) β β’ (π β β© {π β On β£ π΄ β π} = β© {π β On β£ π΅ β π}) | ||
Theorem | cofonr 34206* | Inverse cofinality law for ordinals. Contrast with cofcutr 34232 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ (π β π΄ β On) & β’ (π β π΄ = β© {π₯ β On β£ π β π₯}) β β’ (π β βπ¦ β π΄ βπ§ β π π¦ β π§) | ||
Theorem | naddfn 34207 | Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ +no Fn (On Γ On) | ||
Theorem | naddcllem 34208* | Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β ((π΄ +no π΅) β On β§ (π΄ +no π΅) = β© {π₯ β On β£ (( +no β ({π΄} Γ π΅)) β π₯ β§ ( +no β (π΄ Γ {π΅})) β π₯)})) | ||
Theorem | naddcl 34209 | Closure law for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) β On) | ||
Theorem | naddov 34210* | The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π₯ β On β£ (( +no β ({π΄} Γ π΅)) β π₯ β§ ( +no β (π΄ Γ {π΅})) β π₯)}) | ||
Theorem | naddov2 34211* | Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π₯ β On β£ (βπ¦ β π΅ (π΄ +no π¦) β π₯ β§ βπ§ β π΄ (π§ +no π΅) β π₯)}) | ||
Theorem | naddov3 34212* | Alternate expression for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = β© {π₯ β On β£ (( +no β ({π΄} Γ π΅)) βͺ ( +no β (π΄ Γ {π΅}))) β π₯}) | ||
Theorem | naddf 34213 | Function statement for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ +no :(On Γ On)βΆOn | ||
Theorem | naddcom 34214 | Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ ((π΄ β On β§ π΅ β On) β (π΄ +no π΅) = (π΅ +no π΄)) | ||
Theorem | naddid1 34215 | Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
β’ (π΄ β On β (π΄ +no β ) = π΄) | ||
Theorem | naddssim 34216 | Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddelim 34217 | Ordinal less-than is preserved by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddel1 34218 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (π΄ +no πΆ) β (π΅ +no πΆ))) | ||
Theorem | naddel2 34219 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β (π΄ β π΅ β (πΆ +no π΄) β (πΆ +no π΅))) | ||
Theorem | naddss1 34220 | 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 34221 | 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 34222 | Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On) β π΄ β (π΄ +no π΅)) | ||
Theorem | naddunif 34223* | 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 34224* | Lemma for naddass 34226. 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 34225* | Lemma for naddass 34226. 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 34226 | Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025.) |
β’ ((π΄ β On β§ π΅ β On β§ πΆ β On) β ((π΄ +no π΅) +no πΆ) = (π΄ +no (π΅ +no πΆ))) | ||
Theorem | nadd32 34227 | 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 π΅)) | ||
Theorem | cofsslt 34228* | If every element of π΄ is bounded by some element of π΅ and π΅ precedes πΆ, then π΄ precedes πΆ. Note - we will often use the term "cofinal" to denote that every element of π΄ is bounded above by some element of π΅. Similarly, we will use the term "coinitial" to denote that every element of π΄ is bounded below by some element of π΅. (Contributed by Scott Fenton, 24-Sep-2024.) |
β’ ((π΄ β π« No β§ βπ₯ β π΄ βπ¦ β π΅ π₯ β€s π¦ β§ π΅ <<s πΆ) β π΄ <<s πΆ) | ||
Theorem | coinitsslt 34229* | If π΅ is coinitial with πΆ and π΄ precedes πΆ, then π΄ precedes π΅. (Contributed by Scott Fenton, 24-Sep-2024.) |
β’ ((π΅ β π« No β§ βπ₯ β π΅ βπ¦ β πΆ π¦ β€s π₯ β§ π΄ <<s πΆ) β π΄ <<s π΅) | ||
Theorem | cofcut1 34230* | If πΆ is cofinal with π΄ and π· is coinitial with π΅ and the cut of π΄ and π΅ lies between πΆ and π·. Then the cut of πΆ and π· is equal to the cut of π΄ and π΅. Theorem 2.6 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.) |
β’ ((π΄ <<s π΅ β§ (βπ₯ β π΄ βπ¦ β πΆ π₯ β€s π¦ β§ βπ§ β π΅ βπ€ β π· π€ β€s π§) β§ (πΆ <<s {(π΄ |s π΅)} β§ {(π΄ |s π΅)} <<s π·)) β (π΄ |s π΅) = (πΆ |s π·)) | ||
Theorem | cofcut2 34231* | If π΄ and πΆ are mutually cofinal and π΅ and π· are mutually coinitial, then the cut of π΄ and π΅ is equal to the cut of πΆ and π·. Theorem 2.7 of [Gonshor] p. 10. (Contributed by Scott Fenton, 25-Sep-2024.) |
β’ (((π΄ <<s π΅ β§ πΆ β π« No β§ π· β π« No ) β§ (βπ₯ β π΄ βπ¦ β πΆ π₯ β€s π¦ β§ βπ§ β π΅ βπ€ β π· π€ β€s π§) β§ (βπ‘ β πΆ βπ’ β π΄ π‘ β€s π’ β§ βπ β π· βπ β π΅ π β€s π)) β (π΄ |s π΅) = (πΆ |s π·)) | ||
Theorem | cofcutr 34232* | If π is the cut of π΄ and π΅, then π΄ is cofinal with ( L βπ) and π΅ is coinitial with ( R βπ). Theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.) |
β’ ((π΄ <<s π΅ β§ π = (π΄ |s π΅)) β (βπ₯ β ( L βπ)βπ¦ β π΄ π₯ β€s π¦ β§ βπ§ β ( R βπ)βπ€ β π΅ π€ β€s π§)) | ||
Theorem | cofcutrtime 34233* | If π is the cut of π΄ and π΅ and all of π΄ and π΅ are older than π, then ( L βπ) is cofinal with π΄ and ( R βπ) is coinitial with π΅. Note: we will call a cut where all of the elements of the cut are older than the cut itself a "timely" cut. Part of Theorem 4.02(12) of [Alling] p. 125. (Contributed by Scott Fenton, 27-Sep-2024.) |
β’ (((π΄ βͺ π΅) β ( O β( bday βπ)) β§ π΄ <<s π΅ β§ π = (π΄ |s π΅)) β (βπ₯ β π΄ βπ¦ β ( L βπ)π₯ β€s π¦ β§ βπ§ β π΅ βπ€ β ( R βπ)π€ β€s π§)) | ||
Syntax | cnorec 34234 | Declare the syntax for surreal recursion of one variable. |
class norec (πΉ) | ||
Definition | df-norec 34235* | 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 34236* | 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 34237* | Next, we establish an alternate expression for π . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ ((π΄ β No β§ π΅ β No ) β (π΄π π΅ β ( bday βπ΄) β ( bday βπ΅))) | ||
Theorem | lrrecpo 34238* | Now, we establish that π is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ π Po No | ||
Theorem | lrrecse 34239* | Next, we show that π is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ π Se No | ||
Theorem | lrrecfr 34240* | Now we show that π is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ π = {β¨π₯, π¦β© β£ π₯ β (( L βπ¦) βͺ ( R βπ¦))} β β’ π Fr No | ||
Theorem | lrrecpred 34241* | 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 34242* | 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 34243 | Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ πΉ = norec (πΊ) β β’ πΉ Fn No | ||
Theorem | norecov 34244 | Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.) |
β’ πΉ = norec (πΊ) β β’ (π΄ β No β (πΉβπ΄) = (π΄πΊ(πΉ βΎ (( L βπ΄) βͺ ( R βπ΄))))) | ||
Syntax | cnorec2 34245 | Declare the syntax for surreal recursion on two arguments. |
class norec2 (πΉ) | ||
Definition | df-norec2 34246* | 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 34247* | 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 34248* | 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 34249* | 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 34250* | 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 34251* | 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 34252* | 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 34253 | 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 34254 | The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ πΉ = norec2 (πΊ) β β’ ((π΄ β No β§ π΅ β No ) β (π΄πΉπ΅) = (β¨π΄, π΅β©πΊ(πΉ βΎ ((((( L βπ΄) βͺ ( R βπ΄)) βͺ {π΄}) Γ ((( L βπ΅) βͺ ( R βπ΅)) βͺ {π΅})) β {β¨π΄, π΅β©})))) | ||
Theorem | no3inds 34255* | 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 34256 | Declare the syntax for surreal addition. |
class +s | ||
Definition | df-adds 34257* | 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 34258 | Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ +s Fn ( No Γ No ) | ||
Theorem | addsval 34259* | 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 34260* | 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 34261 | 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 34262 | 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 34263 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ((π΄ β No β§ π΅ β No ) β (π΄ +s π΅) = (π΅ +s π΄)) | ||
Theorem | addscomd 34264 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ (π β π΄ β No ) & β’ (π β π΅ β No ) β β’ (π β (π΄ +s π΅) = (π΅ +s π΄)) | ||
Theorem | addsproplem1 34265* | 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 8313 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 34266* | 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 34267* | 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 34268* | 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 34269* | 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 34270* | 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 34271* | 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 34272 | 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 34273* | 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 34274 | 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 34275 | 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 34276 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ +s :( No Γ No )βΆ No | ||
Theorem | addsfo 34277 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ +s :( No Γ No )βontoβ No | ||
Theorem | sltadd1im 34278 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (π΄ +s πΆ) <s (π΅ +s πΆ))) | ||
Theorem | sltadd2im 34279 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (πΆ +s π΄) <s (πΆ +s π΅))) | ||
Theorem | sleadd1im 34280 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((π΄ +s πΆ) β€s (π΅ +s πΆ) β π΄ β€s π΅)) | ||
Theorem | sleadd2im 34281 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((πΆ +s π΄) β€s (πΆ +s π΅) β π΄ β€s π΅)) | ||
Theorem | sleadd1 34282 | 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 34283 | 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 34284 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (πΆ +s π΄) <s (πΆ +s π΅))) | ||
Theorem | sltadd1 34285 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β (π΄ <s π΅ β (π΄ +s πΆ) <s (π΅ +s πΆ))) | ||
Theorem | addscan2 34286 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((π΄ +s πΆ) = (π΅ +s πΆ) β π΄ = π΅)) | ||
Theorem | addscan1 34287 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
β’ ((π΄ β No β§ π΅ β No β§ πΆ β No ) β ((πΆ +s π΄) = (πΆ +s π΅) β π΄ = π΅)) | ||
Theorem | addsunif 34288* | 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 34289* | 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 34290* | 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 34291 | 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 34292 | 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 34293 | 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 34294 | Declare the syntax for surreal negation. |
class -us | ||
Syntax | csubs 34295 | Declare the syntax for surreal subtraction. |
class -s | ||
Definition | df-negs 34296* | Define surreal negation. Definition from [Conway] p. 5. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ -us = norec ((π₯ β V, π β V β¦ ((π β ( R βπ₯)) |s (π β ( L βπ₯))))) | ||
Definition | df-subs 34297* | Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ -s = (π₯ β No , π¦ β No β¦ (π₯ +s ( -us βπ¦))) | ||
Theorem | negsfn 34298 | Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ -us Fn No | ||
Theorem | negsval 34299 | The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ (π΄ β No β ( -us βπ΄) = (( -us β ( R βπ΄)) |s ( -us β ( L βπ΄)))) | ||
Theorem | negs0s 34300 | Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.) |
β’ ( -us β 0s ) = 0s |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |