![]() |
Metamath
Proof Explorer Theorem List (p. 281 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | no2indslem 28001* | 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 28002* | 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 28003 | 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 28004 | The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ 𝐹 = norec2 (𝐺) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})))) | ||
Theorem | no3inds 28005* | 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 28006 | Declare the syntax for surreal addition. |
class +s | ||
Definition | df-adds 28007* | 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 28008 | Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ +s Fn ( No × No ) | ||
Theorem | addsval 28009* | 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 28010* | 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 28011 | 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 28012 | 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 28013 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
Theorem | addscomd 28014 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
Theorem | addslid 28015 | Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → ( 0s +s 𝐴) = 𝐴) | ||
Theorem | addsproplem1 28016* | 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 8437 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 28017* | 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 28018* | 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 28019* | 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 28020* | 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 28021* | 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 28022* | 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 28023 | 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 28024* | Lemma for addscut 28025. 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 28025* | 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 28026* | 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 28027 | 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 28028 | 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 28029 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ +s :( No × No )⟶ No | ||
Theorem | addsfo 28030 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ +s :( No × No )–onto→ No | ||
Theorem | peano2no 28031 | 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 28032 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | sltadd2im 28033 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sleadd1im 28034 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵)) | ||
Theorem | sleadd2im 28035 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵) → 𝐴 ≤s 𝐵)) | ||
Theorem | sleadd1 28036 | 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 28037 | 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 28038 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sltadd1 28039 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | addscan2 28040 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addscan1 28041 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sleadd1d 28042 | 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 28043 | 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 28044 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sltadd1d 28045 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | addscan2d 28046 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addscan1d 28047 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | addsuniflem 28048* | Lemma for addsunif 28049. 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 28049* | 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 28050* | 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 28051* | 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 28052 | 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 28053 | 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 28054 | 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 28055 | 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 28056 | 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 28057 | 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 28058 | Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐵 +s 𝐴))) | ||
Theorem | sltaddpos2d 28059 | Addition of a positive number increases the sum. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → ( 0s <s 𝐴 ↔ 𝐵 <s (𝐴 +s 𝐵))) | ||
Theorem | slt2addd 28060 | 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 28061 | 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 28062 | A surreal is less than itself plus one. (Contributed by Scott Fenton, 13-Aug-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → 𝐴 <s (𝐴 +s 1s )) | ||
Theorem | addsbdaylem 28063* | Lemma for addsbday 28064. (Contributed by Scott Fenton, 13-Aug-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday ‘𝑦𝑂))) & ⊢ 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵)) ⇒ ⊢ (𝜑 → ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday ‘𝐵))) | ||
Theorem | addsbday 28064 | 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 28065 | Declare the syntax for surreal negation. |
class -us | ||
Syntax | csubs 28066 | Declare the syntax for surreal subtraction. |
class -s | ||
Definition | df-negs 28067* | 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 28068* | Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ -s = (𝑥 ∈ No , 𝑦 ∈ No ↦ (𝑥 +s ( -us ‘𝑦))) | ||
Theorem | negsfn 28069 | Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ -us Fn No | ||
Theorem | subsfn 28070 | Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.) |
⊢ -s Fn ( No × No ) | ||
Theorem | negsval 28071 | The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴)))) | ||
Theorem | negs0s 28072 | Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ( -us ‘ 0s ) = 0s | ||
Theorem | negs1s 28073 | An expression for negative surreal one. (Contributed by Scott Fenton, 24-Jul-2025.) |
⊢ ( -us ‘ 1s ) = (∅ |s { 0s }) | ||
Theorem | negsproplem1 28074* | 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 28075* | 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 28076* | 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 28077* | 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 28078* | 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 28079* | 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 28080* | 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 28081 | Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))) | ||
Theorem | negscl 28082 | 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 28083 | 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 28084 | The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
Theorem | negscut 28085 | 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 28086 | The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴))) | ||
Theorem | negsid 28087 | 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 28088 | 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 28089* | Every surreal has a negative. Note that this theorem, addscl 28028, addscom 28013, addsass 28052, addsrid 28011, and sltadd1im 28032 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 28090 | 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 28091 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
Theorem | sleneg 28092 | 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 28093 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 14-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
Theorem | slenegd 28094 | 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 28095 | Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | negsdi 28096 | Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵))) | ||
Theorem | slt0neg2d 28097 | Comparison of a surreal and its negative to zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → ( 0s <s 𝐴 ↔ ( -us ‘𝐴) <s 0s )) | ||
Theorem | negsf 28098 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ -us : No ⟶ No | ||
Theorem | negsfo 28099 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ -us : No –onto→ No | ||
Theorem | negsf1o 28100 | Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ -us : No –1-1-onto→ No |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |