![]() |
Metamath
Proof Explorer Theorem List (p. 274 of 474) | < 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-29923) |
![]() (29924-31446) |
![]() (31447-47372) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | norecfn 27301 | Surreal recursion over one variable is a function over the surreals. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝐹 = norec (𝐺) ⇒ ⊢ 𝐹 Fn No | ||
Theorem | norecov 27302 | Calculate the value of the surreal recursion operation. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ 𝐹 = norec (𝐺) ⇒ ⊢ (𝐴 ∈ No → (𝐹‘𝐴) = (𝐴𝐺(𝐹 ↾ (( L ‘𝐴) ∪ ( R ‘𝐴))))) | ||
Syntax | cnorec2 27303 | Declare the syntax for surreal recursion on two arguments. |
class norec2 (𝐹) | ||
Definition | df-norec2 27304* | 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 27305* | 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 27306* | 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 27307* | 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 27308* | 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 27309* | 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 27310* | 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 27311 | 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 27312 | The value of the double-recursion surreal function. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ 𝐹 = norec2 (𝐺) ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴𝐹𝐵) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})))) | ||
Theorem | no3inds 27313* | 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 27314 | Declare the syntax for surreal addition. |
class +s | ||
Definition | df-adds 27315* | 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 27316 | Surreal addition is a function over pairs of surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ +s Fn ( No × No ) | ||
Theorem | addsval 27317* | 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 27318* | 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 27319 | 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 27320 | 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 27321 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
Theorem | addscomd 27322 | Surreal addition commutes. Part of Theorem 3 of [Conway] p. 17. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) = (𝐵 +s 𝐴)) | ||
Theorem | addslid 27323 | Surreal addition to zero is identity. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → ( 0s +s 𝐴) = 𝐴) | ||
Theorem | addsproplem1 27324* | 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 8350 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 27325* | 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 27326* | 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 27327* | 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 27328* | 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 27329* | 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 27330* | 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 27331 | 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 27332* | 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 27333 | 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 27334 | 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 27335 | Function statement for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ +s :( No × No )⟶ No | ||
Theorem | addsfo 27336 | Surreal addition is onto. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ +s :( No × No )–onto→ No | ||
Theorem | sltadd1im 27337 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | sltadd2im 27338 | Surreal less-than is preserved under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 → (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sleadd1im 27339 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) ≤s (𝐵 +s 𝐶) → 𝐴 ≤s 𝐵)) | ||
Theorem | sleadd2im 27340 | Surreal less-than or equal cancels under addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) ≤s (𝐶 +s 𝐵) → 𝐴 ≤s 𝐵)) | ||
Theorem | sleadd1 27341 | 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 27342 | 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 27343 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sltadd1 27344 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | addscan2 27345 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addscan1 27346 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | sleadd1d 27347 | 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 27348 | 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 27349 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 21-Jan-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 +s 𝐴) <s (𝐶 +s 𝐵))) | ||
Theorem | sltadd1d 27350 | Addition to both sides of surreal less-than. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐴 +s 𝐶) <s (𝐵 +s 𝐶))) | ||
Theorem | addscan2d 27351 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 +s 𝐶) = (𝐵 +s 𝐶) ↔ 𝐴 = 𝐵)) | ||
Theorem | addscan1d 27352 | Cancellation law for surreal addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐶 +s 𝐴) = (𝐶 +s 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | addsunif 27353* | 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 27354* | 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 27355* | 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 27356 | 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 27357 | 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 27358 | 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 | adds4d 27359 | 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 27360 | 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 𝐵))) | ||
Syntax | cnegs 27361 | Declare the syntax for surreal negation. |
class -us | ||
Syntax | csubs 27362 | Declare the syntax for surreal subtraction. |
class -s | ||
Definition | df-negs 27363* | 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 27364* | Define surreal subtraction. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ -s = (𝑥 ∈ No , 𝑦 ∈ No ↦ (𝑥 +s ( -us ‘𝑦))) | ||
Theorem | negsfn 27365 | Surreal negation is a function over surreals. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ -us Fn No | ||
Theorem | subsfn 27366 | Surreal subtraction is a function over pairs of surreals. (Contributed by Scott Fenton, 22-Jan-2025.) |
⊢ -s Fn ( No × No ) | ||
Theorem | negsval 27367 | The value of the surreal negation function. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ (𝐴 ∈ No → ( -us ‘𝐴) = (( -us “ ( R ‘𝐴)) |s ( -us “ ( L ‘𝐴)))) | ||
Theorem | negs0s 27368 | Negative surreal zero is surreal zero. (Contributed by Scott Fenton, 20-Aug-2024.) |
⊢ ( -us ‘ 0s ) = 0s | ||
Theorem | negsproplem1 27369* | 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 27370* | 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 27371* | 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 27372* | 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 27373* | 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 27374* | 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 27375* | 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 27376 | Show closure and ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))) | ||
Theorem | negscl 27377 | 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 27378 | 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 27379 | The forward direction of the ordering properties of negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
Theorem | negscut 27380 | 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 27381 | The cut that defines surreal negation is legitimate. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L ‘𝐴))) | ||
Theorem | negsid 27382 | 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 27383 | 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 27384* | Every surreal has a negative. Note that this theorem, addscl 27334, addscom 27321, addsass 27356, addsrid 27319, and sltadd1im 27337 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 27385 | 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 27386 | Negative of both sides of surreal less-than. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us ‘𝐴))) | ||
Theorem | sleneg 27387 | Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 ≤s 𝐵 ↔ ( -us ‘𝐵) ≤s ( -us ‘𝐴))) | ||
Theorem | negs11 27388 | Surreal negation is one-to-one. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (( -us ‘𝐴) = ( -us ‘𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | negsdi 27389 | Distribution of surreal negative over addition. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( -us ‘(𝐴 +s 𝐵)) = (( -us ‘𝐴) +s ( -us ‘𝐵))) | ||
Theorem | negsf 27390 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ -us : No ⟶ No | ||
Theorem | negsfo 27391 | Function statement for surreal negation. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ -us : No –onto→ No | ||
Theorem | negsf1o 27392 | Surreal negation is a bijection. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ -us : No –1-1-onto→ No | ||
Theorem | negsunif 27393 | 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 | subsval 27394 | The value of surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵))) | ||
Theorem | subsvald 27395 | The value of surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 -s 𝐵) = (𝐴 +s ( -us ‘𝐵))) | ||
Theorem | subscl 27396 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 -s 𝐵) ∈ No ) | ||
Theorem | subscld 27397 | Closure law for surreal subtraction. (Contributed by Scott Fenton, 5-Feb-2025.) |
⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ No ) | ||
Theorem | subsid1 27398 | Identity law for subtraction. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → (𝐴 -s 0s ) = 𝐴) | ||
Theorem | subsid 27399 | Subtraction of a surreal from itself. (Contributed by Scott Fenton, 3-Feb-2025.) |
⊢ (𝐴 ∈ No → (𝐴 -s 𝐴) = 0s ) | ||
Theorem | subadds 27400 | 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 > |