| Metamath
Proof Explorer Theorem List (p. 281 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | addslid 28001 | Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → ( 0s +s 𝐴) = 𝐴) | ||
| Theorem | addsproplem1 28002* | 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 8439 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 28003* | 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 28004* | 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 28005* | 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 28006* | 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 28007* | 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 28008* | 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 28009 | 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 28010* | Lemma for addscut 28011. 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 28011* | 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 28012* | 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 28013 | 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 28014 | 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 28015 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ +s :( No × No )⟶ No | ||
| Theorem | addsfo 28016 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ +s :( No × No )–onto→ No | ||
| Theorem | peano2no 28017 | A theorem for surreals that is analogous to the second Peano postulate peano2 7912. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ (𝐴 ∈ No → (𝐴 +s 1s ) ∈ No ) | ||
| Theorem | sltadd1im 28018 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
| Theorem | sltadd2im 28019 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
| Theorem | sleadd1im 28020 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵)) | ||
| Theorem | sleadd2im 28021 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵) → 𝐴 ≤s 𝐵)) | ||
| Theorem | sleadd1 28022 | 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 28023 | 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 28024 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
| Theorem | sltadd1 28025 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
| Theorem | addscan2 28026 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | addscan1 28027 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | sleadd1d 28028 | 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 | sleadd2d 28029 | Addition to both sides of surreal less-than or equal. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵))) | ||
| Theorem | sltadd2d 28030 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
| Theorem | sltadd1d 28031 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
| Theorem | addscan2d 28032 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | addscan1d 28033 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | addsuniflem 28034* | Lemma for addsunif 28035. State the whole theorem with extra distinct variable conditions. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ (𝜑 → 𝐿 <<s 𝑅) & ⊢ (𝜑 → 𝑀 <<s 𝑆) & ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) & ⊢ (𝜑 → 𝐵 = (𝑀 |s 𝑆)) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ 𝐿 𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑚 ∈ 𝑀 𝑧 = (𝐴 +s 𝑚)}) |s ({𝑤 ∣ ∃𝑟 ∈ 𝑅 𝑤 = (𝑟 +s 𝐵)} ∪ {𝑡 ∣ ∃𝑠 ∈ 𝑆 𝑡 = (𝐴 +s 𝑠)}))) | ||
| Theorem | addsunif 28035* | 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 28036* | 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 28037* | 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 28038 | 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 28039 | 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 28040 | 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 𝐵)) | ||
| Theorem | adds12d 28041 | Commutative/associative law that swaps the first two terms in a triple sum. (Contributed by Scott Fenton, 9-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s (𝐵 +s 𝐶)) = (𝐵 +s (𝐴 +s 𝐶))) | ||
| Theorem | adds4d 28042 | Rearrangement of four terms in a surreal sum. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐷 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 +s 𝐵) +s (𝐶 +s 𝐷)) = ((𝐴 +s 𝐶) +s (𝐵 +s 𝐷))) | ||
| Theorem | adds42d 28043 | Rearrangement of four terms in a surreal sum. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐷 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 +s 𝐵) +s (𝐶 +s 𝐷)) = ((𝐴 +s 𝐶) +s (𝐷 +s 𝐵))) | ||
| Theorem | sltaddpos1d 28044 | Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐵 +s 𝐴))) | ||
| Theorem | sltaddpos2d 28045 | Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐴 +s 𝐵))) | ||
| Theorem | slt2addd 28046 | Adding both sides of two surreal less-than relations. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐷 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐶) & ⊢ (𝜑 → 𝐵 <s 𝐷) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) <s (𝐶 +s 𝐷)) | ||
| Theorem | addsgt0d 28047 | The sum of two positive surreals is positive. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) & ⊢ (𝜑 → 0s <s 𝐵) ⇒ ⊢ (𝜑 → 0s <s (𝐴 +s 𝐵)) | ||
| Theorem | sltp1d 28048 | A surreal is less than itself plus one. (Contributed by Scott Fenton, 13-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → 𝐴 <s (𝐴 +s 1s )) | ||
| Theorem | addsbdaylem 28049* | Lemma for addsbday 28050. (Contributed by Scott Fenton, 13-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday ‘𝑦𝑂))) & ⊢ 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵)) ⇒ ⊢ (𝜑 → ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday ‘𝐵))) | ||
| Theorem | addsbday 28050 | The birthday of the sum of two surreals is less than or equal to the natural ordinal sum of their individual birthdays. Theorem 6.1 of [Gonshor] p. 95. (Contributed by Scott Fenton, 12-Aug-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( bday ‘(𝐴 +s 𝐵)) ⊆ (( bday ‘𝐴) +no ( bday ‘𝐵))) | ||
| Syntax | cnegs 28051 | Declare the syntax for surreal negation. |
| class -us | ||
| Syntax | csubs 28052 | Declare the syntax for surreal subtraction. |
| class -s | ||
| Definition | df-negs 28053* | 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 28054* | Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ -s = (𝑥 ∈ No , 𝑦 ∈ No ↦ (𝑥 +s ( -us ‘𝑦))) | ||
| Theorem | negsfn 28055 | Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ -us Fn No | ||
| Theorem | subsfn 28056 | Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.) |
| ⊢ -s Fn ( No × No ) | ||
| Theorem | negsval 28057 | The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ (𝐴 ∈ No → ( -us ‘𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴)))) | ||
| Theorem | negs0s 28058 | Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.) |
| ⊢ ( -us ‘ 0s ) = 0s | ||
| Theorem | negs1s 28059 | An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025.) |
| ⊢ ( -us ‘ 1s ) = (∅ |s { 0s }) | ||
| Theorem | negsproplem1 28060* | Lemma for surreal negation. We prove a pair of properties of surreal negation simultaneously. First, we instantiate some quantifiers. (Contributed by Scott Fenton, 2-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝑋 ∈ No ) & ⊢ (𝜑 → 𝑌 ∈ No ) & ⊢ (𝜑 → (( bday ‘𝑋) ∪ ( bday ‘𝑌)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵))) ⇒ ⊢ (𝜑 → (( -us ‘𝑋) ∈ No ∧ (𝑋 <s 𝑌 → ( -us ‘𝑌) <s ( -us ‘𝑋)))) | ||
| Theorem | negsproplem2 28061* | Lemma for surreal negation. Show that the cut that defines negation is legitimate. (Contributed by Scott Fenton, 2-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴))) | ||
| Theorem | negsproplem3 28062* | Lemma for surreal negation. Give the cut properties of surreal negation. (Contributed by Scott Fenton, 2-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → (( -us ‘𝐴) ∈ No ∧ ( -us “ ( R ‘𝐴)) <<s {( -us ‘𝐴)} ∧ {( -us ‘𝐴)} <<s ( -us “ ( L ‘𝐴)))) | ||
| Theorem | negsproplem4 28063* | Lemma for surreal negation. Show the second half of the inductive hypothesis when 𝐴 is simpler than 𝐵. (Contributed by Scott Fenton, 2-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) & ⊢ (𝜑 → ( bday ‘𝐴) ∈ ( bday ‘𝐵)) ⇒ ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴)) | ||
| Theorem | negsproplem5 28064* | Lemma for surreal negation. Show the second half of the inductive hypothesis when 𝐵 is simpler than 𝐴. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) & ⊢ (𝜑 → ( bday ‘𝐵) ∈ ( bday ‘𝐴)) ⇒ ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴)) | ||
| Theorem | negsproplem6 28065* | Lemma for surreal negation. Show the second half of the inductive hypothesis when 𝐴 is the same age as 𝐵. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) & ⊢ (𝜑 → ( bday ‘𝐴) = ( bday ‘𝐵)) ⇒ ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴)) | ||
| Theorem | negsproplem7 28066* | Lemma for surreal negation. Show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝜑 → ∀𝑥 ∈ No ∀𝑦 ∈ No ((( bday ‘𝑥) ∪ ( bday ‘𝑦)) ∈ (( bday ‘𝐴) ∪ ( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐴 <s 𝐵) ⇒ ⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴)) | ||
| Theorem | negsprop 28067 | Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))) | ||
| Theorem | negscl 28068 | The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → ( -us ‘𝐴) ∈ No ) | ||
| Theorem | negscld 28069 | The surreals are closed under negation. Theorem 6(ii) of [Conway] p. 18. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → ( -us ‘𝐴) ∈ No ) | ||
| Theorem | sltnegim 28070 | The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
| Theorem | negscut 28071 | The cut properties of surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → (( -us ‘𝐴) ∈ No ∧ ( -us “ ( R ‘𝐴)) <<s {( -us ‘𝐴)} ∧ {( -us ‘𝐴)} <<s ( -us “ ( L ‘𝐴)))) | ||
| Theorem | negscut2 28072 | The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴))) | ||
| Theorem | negsid 28073 | Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → (𝐴 +s ( -us ‘𝐴)) = 0s ) | ||
| Theorem | negsidd 28074 | Surreal addition of a number and its negative. Theorem 4(iii) of [Conway] p. 17. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s ( -us ‘𝐴)) = 0s ) | ||
| Theorem | negsex 28075* | Every surreal has a negative. Note that this theorem, addscl 28014, addscom 27999, addsass 28038, addsrid 27997, and sltadd1im 28018 are the ordered Abelian group axioms. However, the surreals cannot be said to be an ordered Abelian group because No is a proper class. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → ∃𝑥 ∈ No (𝐴 +s 𝑥) = 0s ) | ||
| Theorem | negnegs 28076 | A surreal is equal to the negative of its negative. Theorem 4(ii) of [Conway] p. 17. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → ( -us ‘( -us ‘𝐴)) = 𝐴) | ||
| Theorem | sltneg 28077 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
| Theorem | sleneg 28078 | Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ( -us ‘𝐵) ≤s ( -us ‘𝐴))) | ||
| Theorem | sltnegd 28079 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
| Theorem | slenegd 28080 | Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ ( -us ‘𝐵) ≤s ( -us ‘𝐴))) | ||
| Theorem | negs11 28081 | Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | negsdi 28082 | Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵))) | ||
| Theorem | slt0neg2d 28083 | Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -us ‘𝐴) <s 0s )) | ||
| Theorem | negsf 28084 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ -us : No ⟶ No | ||
| Theorem | negsfo 28085 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ -us : No –onto→ No | ||
| Theorem | negsf1o 28086 | Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ -us : No –1-1-onto→ No | ||
| Theorem | negsunif 28087 | Uniformity property for surreal negation. If 𝐿 and 𝑅 are any cut that represents 𝐴, then they may be used instead of ( L ‘𝐴) and ( R ‘𝐴) in the definition of negation. (Contributed by Scott Fenton, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐿 <<s 𝑅) & ⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) ⇒ ⊢ (𝜑 → ( -us ‘𝐴) = (( -us “ 𝑅) |s ( -us “ 𝐿))) | ||
| Theorem | negsbdaylem 28088 | Lemma for negsbday 28089. Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025.) |
| ⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) ⊆ ( bday ‘𝐴)) | ||
| Theorem | negsbday 28089 | Negation of a surreal number preserves birthday. (Contributed by Scott Fenton, 8-Mar-2025.) |
| ⊢ (𝐴 ∈ No → ( bday ‘( -us ‘𝐴)) = ( bday ‘𝐴)) | ||
| Theorem | subsval 28090 | The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵))) | ||
| Theorem | subsvald 28091 | The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵))) | ||
| Theorem | subscl 28092 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) ∈ No ) | ||
| Theorem | subscld 28093 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ No ) | ||
| Theorem | subsf 28094 | Function statement for surreal subtraction. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ -s :( No × No )⟶ No | ||
| Theorem | subsfo 28095 | Surreal subtraction is an onto function. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ -s :( No × No )–onto→ No | ||
| Theorem | negsval2 28096 | Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ No → ( -us ‘𝐴) = ( 0s -s 𝐴)) | ||
| Theorem | negsval2d 28097 | Surreal negation in terms of subtraction. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → ( -us ‘𝐴) = ( 0s -s 𝐴)) | ||
| Theorem | subsid1 28098 | Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → (𝐴 -s 0s ) = 𝐴) | ||
| Theorem | subsid 28099 | Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ (𝐴 ∈ No → (𝐴 -s 𝐴) = 0s ) | ||
| Theorem | subadds 28100 | Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 3-Feb-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 -s 𝐵) = 𝐶 ↔ (𝐵 +s 𝐶) = 𝐴)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |