![]() |
Metamath
Proof Explorer Theorem List (p. 280 of 486) | < 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: | ![]() (1-30848) |
![]() (30849-32371) |
![]() (32372-48589) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | leftssno 27901 | The left set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( L ‘𝐴) ⊆ No | ||
Theorem | rightssno 27902 | The right set of a surreal number is a subset of the surreals. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( R ‘𝐴) ⊆ No | ||
Theorem | madecut 27903 | Given a section that is a subset of an old set, the cut is a member of the made set. (Contributed by Scott Fenton, 7-Aug-2024.) |
⊢ (((𝐴 ∈ On ∧ 𝐿 <<s 𝑅) ∧ (𝐿 ⊆ ( O ‘𝐴) ∧ 𝑅 ⊆ ( O ‘𝐴))) → (𝐿 |s 𝑅) ∈ ( M ‘𝐴)) | ||
Theorem | madeun 27904 | The made set is the union of the old set and the new set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ( M ‘𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴)) | ||
Theorem | madeoldsuc 27905 | The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( O ‘suc 𝐴)) | ||
Theorem | oldsuc 27906 | The value of the old set at a successor. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ (𝐴 ∈ On → ( O ‘suc 𝐴) = (( O ‘𝐴) ∪ ( N ‘𝐴))) | ||
Theorem | oldlim 27907 | The value of the old set at a limit ordinal. (Contributed by Scott Fenton, 8-Aug-2024.) |
⊢ ((Lim 𝐴 ∧ 𝐴 ∈ 𝑉) → ( O ‘𝐴) = ∪ ( O “ 𝐴)) | ||
Theorem | madebdayim 27908 | If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ (𝑋 ∈ ( M ‘𝐴) → ( bday ‘𝑋) ⊆ 𝐴) | ||
Theorem | oldbdayim 27909 | If 𝑋 is in the old set for 𝐴, then the birthday of 𝑋 is less than 𝐴. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ (𝑋 ∈ ( O ‘𝐴) → ( bday ‘𝑋) ∈ 𝐴) | ||
Theorem | oldirr 27910 | No surreal is a member of its birthday's old set. (Contributed by Scott Fenton, 10-Aug-2024.) |
⊢ ¬ 𝑋 ∈ ( O ‘( bday ‘𝑋)) | ||
Theorem | leftirr 27911 | No surreal is a member of its left set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ¬ 𝑋 ∈ ( L ‘𝑋) | ||
Theorem | rightirr 27912 | No surreal is a member of its right set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ ¬ 𝑋 ∈ ( R ‘𝑋) | ||
Theorem | left0s 27913 | The left set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ( L ‘ 0s ) = ∅ | ||
Theorem | right0s 27914 | The right set of 0s is empty. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ( R ‘ 0s ) = ∅ | ||
Theorem | left1s 27915 | The left set of 1s is the singleton of 0s. (Contributed by Scott Fenton, 4-Feb-2025.) |
⊢ ( L ‘ 1s ) = { 0s } | ||
Theorem | right1s 27916 | The right set of 1s is empty . (Contributed by Scott Fenton, 4-Feb-2025.) |
⊢ ( R ‘ 1s ) = ∅ | ||
Theorem | lrold 27917 | The union of the left and right options of a surreal make its old set. (Contributed by Scott Fenton, 9-Oct-2024.) |
⊢ (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday ‘𝐴)) | ||
Theorem | madebdaylemold 27918* | Lemma for madebday 27920. If the inductive hypothesis of madebday 27920 is satisfied, the converse of oldbdayim 27909 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ ∀𝑏 ∈ 𝐴 ∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( bday ‘𝑋) ∈ 𝐴 → 𝑋 ∈ ( O ‘𝐴))) | ||
Theorem | madebdaylemlrcut 27919* | Lemma for madebday 27920. If the inductive hypothesis of madebday 27920 is satisfied up to the birthday of 𝑋, then the conclusion of lrcut 27923 holds. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((∀𝑏 ∈ ( bday ‘𝑋)∀𝑦 ∈ No (( bday ‘𝑦) ⊆ 𝑏 → 𝑦 ∈ ( M ‘𝑏)) ∧ 𝑋 ∈ No ) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) | ||
Theorem | madebday 27920 | A surreal is part of the set made by ordinal 𝐴 iff its birthday is less than or equal to 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( M ‘𝐴) ↔ ( bday ‘𝑋) ⊆ 𝐴)) | ||
Theorem | oldbday 27921 | A surreal is part of the set older than ordinal 𝐴 iff its birthday is less than 𝐴. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( O ‘𝐴) ↔ ( bday ‘𝑋) ∈ 𝐴)) | ||
Theorem | newbday 27922 | A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in [Conway] p. 29. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ No ) → (𝑋 ∈ ( N ‘𝐴) ↔ ( bday ‘𝑋) = 𝐴)) | ||
Theorem | lrcut 27923 | A surreal is equal to the cut of its left and right sets. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ (𝑋 ∈ No → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) | ||
Theorem | scutfo 27924 | The surreal cut function is onto. (Contributed by Scott Fenton, 23-Aug-2024.) |
⊢ |s : <<s –onto→ No | ||
Theorem | sltn0 27925 | If 𝑋 is less than 𝑌, then either ( L ‘𝑌) or ( R ‘𝑋) is non-empty. (Contributed by Scott Fenton, 10-Dec-2024.) |
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑋 <s 𝑌) → (( L ‘𝑌) ≠ ∅ ∨ ( R ‘𝑋) ≠ ∅)) | ||
Theorem | lruneq 27926 | If two surreals share a birthday, then the union of their left and right sets are equal. (Contributed by Scott Fenton, 17-Sep-2024.) |
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌))) | ||
Theorem | sltlpss 27927 | If two surreals share a birthday, then 𝑋 <s 𝑌 iff the left set of 𝑋 is a proper subset of the left set of 𝑌. (Contributed by Scott Fenton, 17-Sep-2024.) |
⊢ ((𝑋 ∈ No ∧ 𝑌 ∈ No ∧ ( bday ‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌))) | ||
Theorem | slelss 27928 | If two surreals 𝐴 and 𝐵 share a birthday, then 𝐴 ≤s 𝐵 if and only if the left set of 𝐴 is a non-strict subset of the left set of 𝐵. (Contributed by Scott Fenton, 21-Mar-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ ( bday ‘𝐴) = ( bday ‘𝐵)) → (𝐴 ≤s 𝐵 ↔ ( L ‘𝐴) ⊆ ( L ‘𝐵))) | ||
Theorem | 0elold 27929 | Zero is in the old set of any non-zero number. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 ≠ 0s ) ⇒ ⊢ (𝜑 → 0s ∈ ( O ‘( bday ‘𝐴))) | ||
Theorem | 0elleft 27930 | Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) ⇒ ⊢ (𝜑 → 0s ∈ ( L ‘𝐴)) | ||
Theorem | 0elright 27931 | Zero is in the right set of any negative number. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 0s ) ⇒ ⊢ (𝜑 → 0s ∈ ( R ‘𝐴)) | ||
Theorem | cofsslt 27932* | If every element of 𝐴 is bounded above 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 27933* | If 𝐵 is coinitial with 𝐶 and 𝐴 precedes 𝐶, then 𝐴 precedes 𝐵. (Contributed by Scott Fenton, 24-Sep-2024.) |
⊢ ((𝐵 ∈ 𝒫 No ∧ ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐶 𝑦 ≤s 𝑥 ∧ 𝐴 <<s 𝐶) → 𝐴 <<s 𝐵) | ||
Theorem | cofcut1 27934* | 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 | cofcut1d 27935* | 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, 23-Jan-2025.) |
⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) & ⊢ (𝜑 → 𝐶 <<s {(𝐴 |s 𝐵)}) & ⊢ (𝜑 → {(𝐴 |s 𝐵)} <<s 𝐷) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) | ||
Theorem | cofcut2 27936* | 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 | cofcut2d 27937* | 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, 23-Jan-2025.) |
⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝐶 ∈ 𝒫 No ) & ⊢ (𝜑 → 𝐷 ∈ 𝒫 No ) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐶 𝑥 ≤s 𝑦) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐷 𝑤 ≤s 𝑧) & ⊢ (𝜑 → ∀𝑡 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑡 ≤s 𝑢) & ⊢ (𝜑 → ∀𝑟 ∈ 𝐷 ∃𝑠 ∈ 𝐵 𝑠 ≤s 𝑟) ⇒ ⊢ (𝜑 → (𝐴 |s 𝐵) = (𝐶 |s 𝐷)) | ||
Theorem | cofcutr 27938* | 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 | cofcutr1d 27939* | If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐴 is cofinal with ( L ‘𝑋). First half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 23-Jan-2025.) |
⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ ( L ‘𝑋)∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) | ||
Theorem | cofcutr2d 27940* | If 𝑋 is the cut of 𝐴 and 𝐵, then 𝐵 is coinitial with ( R ‘𝑋). Second half of theorem 2.9 of [Gonshor] p. 12. (Contributed by Scott Fenton, 25-Sep-2024.) |
⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ ( R ‘𝑋)∃𝑤 ∈ 𝐵 𝑤 ≤s 𝑧) | ||
Theorem | cofcutrtime 27941* | 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 𝑧)) | ||
Theorem | cofcutrtime1d 27942* | If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( L ‘𝑋) is cofinal with 𝐴. (Contributed by Scott Fenton, 23-Jan-2025.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋))) & ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ( L ‘𝑋)𝑥 ≤s 𝑦) | ||
Theorem | cofcutrtime2d 27943* | If 𝑋 is a timely cut of 𝐴 and 𝐵, then ( R ‘𝑋) is coinitial with 𝐵. (Contributed by Scott Fenton, 23-Jan-2025.) |
⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ ( O ‘( bday ‘𝑋))) & ⊢ (𝜑 → 𝐴 <<s 𝐵) & ⊢ (𝜑 → 𝑋 = (𝐴 |s 𝐵)) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ ( R ‘𝑋)𝑤 ≤s 𝑧) | ||
Theorem | cofss 27944* | Cofinality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑥 ≤s 𝑦) | ||
Theorem | coiniss 27945* | Coinitiality for a subset. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐴 𝑦 ≤s 𝑥) | ||
Theorem | cutlt 27946* | Eliminating all elements below a given element of a cut does not affect the cut. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐿 <<s 𝑅) & ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) & ⊢ (𝜑 → 𝑋 ∈ 𝐿) ⇒ ⊢ (𝜑 → 𝐴 = (({𝑋} ∪ {𝑦 ∈ 𝐿 ∣ 𝑋 <s 𝑦}) |s 𝑅)) | ||
Theorem | cutpos 27947* | Reduce the elements of a cut for a positive number. (Contributed by Scott Fenton, 13-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) ⇒ ⊢ (𝜑 → 𝐴 = (({ 0s } ∪ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}) |s ( R ‘𝐴))) | ||
Syntax | cnorec 27948 | Declare the syntax for surreal recursion of one variable. |
class norec (𝐹) | ||
Definition | df-norec 27949* | 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 27950* | 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 27951* | Next, we establish an alternate expression for 𝑅. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝑅𝐵 ↔ ( bday ‘𝐴) ∈ ( bday ‘𝐵))) | ||
Theorem | lrrecpo 27952* | Now, we establish that 𝑅 is a partial ordering on No . (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Po No | ||
Theorem | lrrecse 27953* | Next, we show that 𝑅 is set-like over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Se No | ||
Theorem | lrrecfr 27954* | Now we show that 𝑅 is founded over No . (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))} ⇒ ⊢ 𝑅 Fr No | ||
Theorem | lrrecpred 27955* | 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 27956* | 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 27957 | Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝐹 = norec (𝐺) ⇒ ⊢ 𝐹 Fn No | ||
Theorem | norecov 27958 | Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝐹 = norec (𝐺) ⇒ ⊢ (𝐴 ∈ No → (𝐹‘𝐴) = (𝐴𝐺(𝐹 ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))))) | ||
Syntax | cnorec2 27959 | Declare the syntax for surreal recursion on two arguments. |
class norec2 (𝐹) | ||
Definition | df-norec2 27960* | 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 27961* | To get through most of the textbook definitions 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 27962* | 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 27963* | 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 27964* | 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 27965* | Double induction on surreals with explicit notation for the relationships. (Contributed by Scott Fenton, 22-Aug-2024.) |
⊢ 𝑅 = {〈𝑎, 𝑏〉 ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))} & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝑤 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜃 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ (𝑦 = 𝐵 → (𝜏 ↔ 𝜂)) & ⊢ ((𝑥 ∈ No ∧ 𝑦 ∈ No ) → ((∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜒 ∧ ∀𝑧 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))𝜓 ∧ ∀𝑤 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))𝜃) → 𝜑)) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝜂) | ||
Theorem | no2inds 27966* | 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 27967 | 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 27968 | The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ 𝐹 = norec2 (𝐺) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})))) | ||
Theorem | no3inds 27969* | 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 27970 | Declare the syntax for surreal addition. |
class +s | ||
Definition | df-adds 27971* | 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 27972 | Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ +s Fn ( No × No ) | ||
Theorem | addsval 27973* | 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 27974* | 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 | addsrid 27975 | 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 | addsridd 27976 | 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 27977 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
Theorem | addscomd 27978 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
Theorem | addslid 27979 | Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → ( 0s +s 𝐴) = 𝐴) | ||
Theorem | addsproplem1 27980* | 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 8421 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 27981* | 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 27982* | 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 27983* | 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 27984* | 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 27985* | 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 27986* | 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 27987 | 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 | addscutlem 27988* | Lemma for addscut 27989. Show the statement with some additional distinct variable conditions. (Contributed by Scott Fenton, 8-Mar-2025.) |
⊢ (𝜑 → 𝑋 ∈ No ) & ⊢ (𝜑 → 𝑌 ∈ No ) ⇒ ⊢ (𝜑 → ((𝑋 +s 𝑌) ∈ No ∧ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))) | ||
Theorem | addscut 27989* | 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 | addscut2 27990* | Show that the cut involved in surreal addition is legitimate. (Contributed by Scott Fenton, 8-Mar-2025.) |
⊢ (𝜑 → 𝑋 ∈ No ) & ⊢ (𝜑 → 𝑌 ∈ No ) ⇒ ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) | ||
Theorem | addscld 27991 | 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 27992 | 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 27993 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ +s :( No × No )⟶ No | ||
Theorem | addsfo 27994 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ +s :( No × No )–onto→ No | ||
Theorem | peano2no 27995 | A theorem for surreals that is analogous to the second Peano postulate peano2 7894. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ (𝐴 ∈ No → (𝐴 +s 1s ) ∈ No ) | ||
Theorem | sltadd1im 27996 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | sltadd2im 27997 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sleadd1im 27998 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵)) | ||
Theorem | sleadd2im 27999 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵) → 𝐴 ≤s 𝐵)) | ||
Theorem | sleadd1 28000 | 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 𝐶))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |