| Metamath
Proof Explorer Theorem List (p. 283 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 | slemul1d 28201 | Multiplication of both sides of surreal less-than or equal by a positive number. (Contributed by Scott Fenton, 10-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) ⇒ ⊢ (𝜑 → (𝐴 ≤s 𝐵 ↔ (𝐴 ·s 𝐶) ≤s (𝐵 ·s 𝐶))) | ||
| Theorem | sltmulneg1d 28202 | Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 <s 0s ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐵 ·s 𝐶) <s (𝐴 ·s 𝐶))) | ||
| Theorem | sltmulneg2d 28203 | Multiplication of both sides of surreal less-than by a negative number. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 <s 0s ) ⇒ ⊢ (𝜑 → (𝐴 <s 𝐵 ↔ (𝐶 ·s 𝐵) <s (𝐶 ·s 𝐴))) | ||
| Theorem | mulscan2dlem 28204 | Lemma for mulscan2d 28205. Cancellation of multiplication when the right term is positive. (Contributed by Scott Fenton, 10-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | mulscan2d 28205 | Cancellation of surreal multiplication when the right term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐶) = (𝐵 ·s 𝐶) ↔ 𝐴 = 𝐵)) | ||
| Theorem | mulscan1d 28206 | Cancellation of surreal multiplication when the left term is non-zero. (Contributed by Scott Fenton, 10-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐶 ·s 𝐴) = (𝐶 ·s 𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | muls12d 28207 | Commutative/associative law for surreal multiplication. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) ⇒ ⊢ (𝜑 → (𝐴 ·s (𝐵 ·s 𝐶)) = (𝐵 ·s (𝐴 ·s 𝐶))) | ||
| Theorem | slemul1ad 28208 | Multiplication of both sides of surreal less-than or equal by a non-negative number. (Contributed by Scott Fenton, 17-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s ≤s 𝐶) & ⊢ (𝜑 → 𝐴 ≤s 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ·s 𝐶) ≤s (𝐵 ·s 𝐶)) | ||
| Theorem | sltmul12ad 28209 | Comparison of the product of two positive surreals. (Contributed by Scott Fenton, 17-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐷 ∈ No ) & ⊢ (𝜑 → 0s ≤s 𝐴) & ⊢ (𝜑 → 𝐴 <s 𝐵) & ⊢ (𝜑 → 0s ≤s 𝐶) & ⊢ (𝜑 → 𝐶 <s 𝐷) ⇒ ⊢ (𝜑 → (𝐴 ·s 𝐶) <s (𝐵 ·s 𝐷)) | ||
| Theorem | divsmo 28210* | Uniqueness of surreal inversion. Given a non-zero surreal 𝐴, there is at most one surreal giving a particular product. (Contributed by Scott Fenton, 10-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃*𝑥 ∈ No (𝐴 ·s 𝑥) = 𝐵) | ||
| Theorem | muls0ord 28211 | If a surreal product is zero, one of its factors must be zero. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐵) = 0s ↔ (𝐴 = 0s ∨ 𝐵 = 0s ))) | ||
| Theorem | mulsne0bd 28212 | The product of two non-zero surreals is non-zero. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐵) ≠ 0s ↔ (𝐴 ≠ 0s ∧ 𝐵 ≠ 0s ))) | ||
| Syntax | cdivs 28213 | Declare the syntax for surreal division. |
| class /su | ||
| Definition | df-divs 28214* | Define surreal division. This is not the definition used in the literature, but we use it here because it is technically easier to work with. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ /su = (𝑥 ∈ No , 𝑦 ∈ ( No ∖ { 0s }) ↦ (℩𝑧 ∈ No (𝑦 ·s 𝑧) = 𝑥)) | ||
| Theorem | divsval 28215* | The value of surreal division. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) = (℩𝑥 ∈ No (𝐵 ·s 𝑥) = 𝐴)) | ||
| Theorem | norecdiv 28216* | If a surreal has a reciprocal, then it has any division. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s ) → ∃𝑦 ∈ No (𝐴 ·s 𝑦) = 𝐵) | ||
| Theorem | noreceuw 28217* | If a surreal has a reciprocal, then it has unique division. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐴 ≠ 0s ∧ 𝐵 ∈ No ) ∧ ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s ) → ∃!𝑦 ∈ No (𝐴 ·s 𝑦) = 𝐵) | ||
| Theorem | divsmulw 28218* | Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. Later, when we prove precsex 28242, we can eliminate the existence hypothesis (see divsmul 28245). (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) ∧ ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴)) | ||
| Theorem | divsmulwd 28219* | Relationship between surreal division and multiplication. Weak version that does not assume reciprocals. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴)) | ||
| Theorem | divsclw 28220* | Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) ∧ ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) → (𝐴 /su 𝐵) ∈ No ) | ||
| Theorem | divsclwd 28221* | Weak division closure law. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No ) | ||
| Theorem | divscan2wd 28222* | A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴) | ||
| Theorem | divscan1wd 28223* | A weak cancellation law for surreal division. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐵 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴) | ||
| Theorem | sltdivmulwd 28224* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐶 ·s 𝐵))) | ||
| Theorem | sltdivmul2wd 28225* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s 𝐶))) | ||
| Theorem | sltmuldivwd 28226* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶))) | ||
| Theorem | sltmuldiv2wd 28227* | Surreal less-than relationship between division and multiplication. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐶 ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶))) | ||
| Theorem | divsasswd 28228* | An associative law for surreal division. Weak version. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) & ⊢ (𝜑 → ∃𝑥 ∈ No (𝐶 ·s 𝑥) = 1s ) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su 𝐶) = (𝐴 ·s (𝐵 /su 𝐶))) | ||
| Theorem | divs1 28229 | A surreal divided by one is itself. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ (𝐴 ∈ No → (𝐴 /su 1s ) = 𝐴) | ||
| Theorem | precsexlemcbv 28230* | Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) ⇒ ⊢ 𝐹 = rec((𝑞 ∈ V ↦ ⦋(1st ‘𝑞) / 𝑚⦌⦋(2nd ‘𝑞) / 𝑠⦌〈(𝑚 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)} ∪ {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿)})), (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)} ∪ {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅)}))〉), 〈{ 0s }, ∅〉) | ||
| Theorem | precsexlem1 28231 | Lemma for surreal reciprocals. Calculate the value of the recursive left function at zero. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ (𝐿‘∅) = { 0s } | ||
| Theorem | precsexlem2 28232 | Lemma for surreal reciprocals. Calculate the value of the recursive right function at zero. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ (𝑅‘∅) = ∅ | ||
| Theorem | precsexlem3 28233* | Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ (𝐼 ∈ ω → (𝐹‘suc 𝐼) = 〈((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉) | ||
| Theorem | precsexlem4 28234* | Lemma for surreal reciprocals. Calculate the value of the recursive left function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ (𝐼 ∈ ω → (𝐿‘suc 𝐼) = ((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)}))) | ||
| Theorem | precsexlem5 28235* | Lemma for surreal reciprocals. Calculate the value of the recursive right function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ (𝐼 ∈ ω → (𝑅‘suc 𝐼) = ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))) | ||
| Theorem | precsexlem6 28236* | Lemma for surreal reciprocal. Show that 𝐿 is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽) → (𝐿‘𝐼) ⊆ (𝐿‘𝐽)) | ||
| Theorem | precsexlem7 28237* | Lemma for surreal reciprocal. Show that 𝑅 is non-strictly increasing in its argument. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) ⇒ ⊢ ((𝐼 ∈ ω ∧ 𝐽 ∈ ω ∧ 𝐼 ⊆ 𝐽) → (𝑅‘𝐼) ⊆ (𝑅‘𝐽)) | ||
| Theorem | precsexlem8 28238* | Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) & ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s )) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → ((𝐿‘𝐼) ⊆ No ∧ (𝑅‘𝐼) ⊆ No )) | ||
| Theorem | precsexlem9 28239* | Lemma for surreal reciprocal. Show that the product of 𝐴 and a left element is less than one and the product of 𝐴 and a right element is greater than one. (Contributed by Scott Fenton, 14-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) & ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s )) ⇒ ⊢ ((𝜑 ∧ 𝐼 ∈ ω) → (∀𝑏 ∈ (𝐿‘𝐼)(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘𝐼) 1s <s (𝐴 ·s 𝑐))) | ||
| Theorem | precsexlem10 28240* | Lemma for surreal reciprocal. Show that the union of the left sets is less than the union of the right sets. Note that this is the first theorem in the surreal numbers to require the axiom of infinity. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) & ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s )) ⇒ ⊢ (𝜑 → ∪ (𝐿 “ ω) <<s ∪ (𝑅 “ ω)) | ||
| Theorem | precsexlem11 28241* | Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for 𝐴. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ 𝐹 = rec((𝑝 ∈ V ↦ ⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd ‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} ∪ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})), (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} ∪ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)}))〉), 〈{ 0s }, ∅〉) & ⊢ 𝐿 = (1st ∘ 𝐹) & ⊢ 𝑅 = (2nd ∘ 𝐹) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐴) & ⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 → ∃𝑦 ∈ No (𝑥𝑂 ·s 𝑦) = 1s )) & ⊢ 𝑌 = (∪ (𝐿 “ ω) |s ∪ (𝑅 “ ω)) ⇒ ⊢ (𝜑 → (𝐴 ·s 𝑌) = 1s ) | ||
| Theorem | precsex 28242* | Every positive surreal has a reciprocal. Theorem 10(iv) of [Conway] p. 21. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 0s <s 𝐴) → ∃𝑦 ∈ No (𝐴 ·s 𝑦) = 1s ) | ||
| Theorem | recsex 28243* | A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 15-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐴 ≠ 0s ) → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s ) | ||
| Theorem | recsexd 28244* | A non-zero surreal has a reciprocal. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 ≠ 0s ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ No (𝐴 ·s 𝑥) = 1s ) | ||
| Theorem | divsmul 28245 | Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ (𝐶 ∈ No ∧ 𝐶 ≠ 0s )) → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴)) | ||
| Theorem | divsmuld 28246 | Relationship between surreal division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐶) = 𝐵 ↔ (𝐶 ·s 𝐵) = 𝐴)) | ||
| Theorem | divscl 28247 | Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐵 ≠ 0s ) → (𝐴 /su 𝐵) ∈ No ) | ||
| Theorem | divscld 28248 | Surreal division closure law. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) ⇒ ⊢ (𝜑 → (𝐴 /su 𝐵) ∈ No ) | ||
| Theorem | divscan2d 28249 | A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) ⇒ ⊢ (𝜑 → (𝐵 ·s (𝐴 /su 𝐵)) = 𝐴) | ||
| Theorem | divscan1d 28250 | A cancellation law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s 𝐵) = 𝐴) | ||
| Theorem | sltdivmuld 28251 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐶 ·s 𝐵))) | ||
| Theorem | sltdivmul2d 28252 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 ·s 𝐶))) | ||
| Theorem | sltmuldivd 28253 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐶) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶))) | ||
| Theorem | sltmuldiv2d 28254 | Surreal less-than relationship between division and multiplication. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 0s <s 𝐶) ⇒ ⊢ (𝜑 → ((𝐶 ·s 𝐴) <s 𝐵 ↔ 𝐴 <s (𝐵 /su 𝐶))) | ||
| Theorem | divsassd 28255 | An associative law for surreal division. (Contributed by Scott Fenton, 16-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 ·s 𝐵) /su 𝐶) = (𝐴 ·s (𝐵 /su 𝐶))) | ||
| Theorem | divmuldivsd 28256 | Multiplication of two surreal ratios. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐷 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) & ⊢ (𝜑 → 𝐷 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐵) ·s (𝐶 /su 𝐷)) = ((𝐴 ·s 𝐶) /su (𝐵 ·s 𝐷))) | ||
| Theorem | divdivs1d 28257 | Surreal division into a fraction. (Contributed by Scott Fenton, 7-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 /su 𝐵) /su 𝐶) = (𝐴 /su (𝐵 ·s 𝐶))) | ||
| Theorem | divsrecd 28258 | Relationship between surreal division and reciprocal. (Contributed by Scott Fenton, 13-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) ⇒ ⊢ (𝜑 → (𝐴 /su 𝐵) = (𝐴 ·s ( 1s /su 𝐵))) | ||
| Theorem | divsdird 28259 | Distribution of surreal division over addition. (Contributed by Scott Fenton, 13-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐶 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐴 +s 𝐵) /su 𝐶) = ((𝐴 /su 𝐶) +s (𝐵 /su 𝐶))) | ||
| Theorem | divscan3d 28260 | A cancellation law for surreal division. (Contributed by Scott Fenton, 13-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ No ) & ⊢ (𝜑 → 𝐵 ≠ 0s ) ⇒ ⊢ (𝜑 → ((𝐵 ·s 𝐴) /su 𝐵) = 𝐴) | ||
| Syntax | cabss 28261 | Declare the syntax for surreal absolute value. |
| class abss | ||
| Definition | df-abss 28262 | Define the surreal absolute value function. See abssval 28263 for its value and absscl 28264 for its closure. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ abss = (𝑥 ∈ No ↦ if( 0s ≤s 𝑥, 𝑥, ( -us ‘𝑥))) | ||
| Theorem | abssval 28263 | The value of surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝐴 ∈ No → (abss‘𝐴) = if( 0s ≤s 𝐴, 𝐴, ( -us ‘𝐴))) | ||
| Theorem | absscl 28264 | Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝐴 ∈ No → (abss‘𝐴) ∈ No ) | ||
| Theorem | abssid 28265 | The absolute value of a non-negative surreal is itself. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴) | ||
| Theorem | abs0s 28266 | The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (abss‘ 0s ) = 0s | ||
| Theorem | abssnid 28267 | For a negative surreal, its absolute value is its negation. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐴 ≤s 0s ) → (abss‘𝐴) = ( -us ‘𝐴)) | ||
| Theorem | absmuls 28268 | Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (abss‘(𝐴 ·s 𝐵)) = ((abss‘𝐴) ·s (abss‘𝐵))) | ||
| Theorem | abssge0 28269 | The absolute value of a surreal number is non-negative. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝐴 ∈ No → 0s ≤s (abss‘𝐴)) | ||
| Theorem | abssor 28270 | The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝐴 ∈ No → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us ‘𝐴))) | ||
| Theorem | abssneg 28271 | Surreal absolute value of the negative. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝐴 ∈ No → (abss‘( -us ‘𝐴)) = (abss‘𝐴)) | ||
| Theorem | sleabs 28272 | A surreal is less than or equal to its absolute value. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ (𝐴 ∈ No → 𝐴 ≤s (abss‘𝐴)) | ||
| Theorem | absslt 28273 | Surreal absolute value and less-than relation. (Contributed by Scott Fenton, 16-Apr-2025.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → ((abss‘𝐴) <s 𝐵 ↔ (( -us ‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵))) | ||
| Syntax | cons 28274 | Declare the syntax for surreal ordinals. |
| class Ons | ||
| Definition | df-ons 28275 | Define the surreal ordinals. These are the maximum members of each generation of surreals. Variant of definition from [Conway] p. 27. (Contributed by Scott Fenton, 18-Mar-2025.) |
| ⊢ Ons = {𝑥 ∈ No ∣ ( R ‘𝑥) = ∅} | ||
| Theorem | elons 28276 | Membership in the class of surreal ordinals. (Contributed by Scott Fenton, 18-Mar-2025.) |
| ⊢ (𝐴 ∈ Ons ↔ (𝐴 ∈ No ∧ ( R ‘𝐴) = ∅)) | ||
| Theorem | onssno 28277 | The surreal ordinals are a subclass of the surreals. (Contributed by Scott Fenton, 18-Mar-2025.) |
| ⊢ Ons ⊆ No | ||
| Theorem | onsno 28278 | A surreal ordinal is a surreal. (Contributed by Scott Fenton, 18-Mar-2025.) |
| ⊢ (𝐴 ∈ Ons → 𝐴 ∈ No ) | ||
| Theorem | 0ons 28279 | Surreal zero is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.) |
| ⊢ 0s ∈ Ons | ||
| Theorem | 1ons 28280 | Surreal one is a surreal ordinal. (Contributed by Scott Fenton, 18-Mar-2025.) |
| ⊢ 1s ∈ Ons | ||
| Theorem | elons2 28281* | A surreal is ordinal iff it is the cut of some set of surreals and the empty set. Definition from [Conway] p. 27. (Contributed by Scott Fenton, 19-Mar-2025.) |
| ⊢ (𝐴 ∈ Ons ↔ ∃𝑎 ∈ 𝒫 No 𝐴 = (𝑎 |s ∅)) | ||
| Theorem | elons2d 28282 | The cut of any set of surreals and the empty set is a surreal ordinal. (Contributed by Scott Fenton, 19-Mar-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ No ) & ⊢ (𝜑 → 𝑋 = (𝐴 |s ∅)) ⇒ ⊢ (𝜑 → 𝑋 ∈ Ons) | ||
| Theorem | sltonold 28283* | The class of ordinals less than any surreal is a subset of that surreal's old set. (Contributed by Scott Fenton, 22-Mar-2025.) |
| ⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ⊆ ( O ‘( bday ‘𝐴))) | ||
| Theorem | sltonex 28284* | The class of ordinals less than any particular surreal is a set. Theorem 14 of [Conway] p. 27. (Contributed by Scott Fenton, 22-Mar-2025.) |
| ⊢ (𝐴 ∈ No → {𝑥 ∈ Ons ∣ 𝑥 <s 𝐴} ∈ V) | ||
| Theorem | onscutleft 28285 | A surreal ordinal is equal to the cut of its left set and the empty set. (Contributed by Scott Fenton, 29-Mar-2025.) |
| ⊢ (𝐴 ∈ Ons → 𝐴 = (( L ‘𝐴) |s ∅)) | ||
| Theorem | onaddscl 28286 | The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025.) |
| ⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 +s 𝐵) ∈ Ons) | ||
| Theorem | onmulscl 28287 | The surreal ordinals are closed under multiplication. (Contributed by Scott Fenton, 22-Aug-2025.) |
| ⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ·s 𝐵) ∈ Ons) | ||
| Theorem | peano2ons 28288 | The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025.) |
| ⊢ (𝐴 ∈ Ons → (𝐴 +s 1s ) ∈ Ons) | ||
| Syntax | cseqs 28289 | Extend class notation with the surreal recursive sequence builder. |
| class seqs𝑀( + , 𝐹) | ||
| Definition | df-seqs 28290* | Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14043. Note that in the theorems we develop here, we do not require 𝑀 to be an integer. This is because there are infinite surreal numbers and we may want to start our sequence there. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ seqs𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))〉), 〈𝑀, (𝐹‘𝑀)〉) “ ω) | ||
| Theorem | seqsex 28291 | Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ seqs𝑀( + , 𝐹) ∈ V | ||
| Theorem | seqseq123d 28292 | Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → + = 𝑄) & ⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺)) | ||
| Theorem | nfseqs 28293 | Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ Ⅎ𝑥𝑀 & ⊢ Ⅎ𝑥 + & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹) | ||
| Theorem | seqsval 28294* | The value of the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥(𝑧 ∈ V, 𝑤 ∈ V ↦ (𝑤 + (𝐹‘(𝑧 +s 1s ))))𝑦)〉), 〈𝑀, (𝐹‘𝑀)〉) ↾ ω)) ⇒ ⊢ (𝜑 → seqs𝑀( + , 𝐹) = ran 𝑅) | ||
| Theorem | noseqex 28295 | The next several theorems develop the concept of a countable sequence of surreals. This set is denoted by 𝑍 here and is the analogue of the upper integer sets for surreal numbers. However, we do not require the starting point to be an integer so we can accommodate infinite numbers. This first theorem establishes that 𝑍 is a set. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) ⇒ ⊢ (𝜑 → 𝑍 ∈ V) | ||
| Theorem | noseq0 28296 | The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑍) | ||
| Theorem | noseqp1 28297* | One plus an element of 𝑍 is an element of 𝑍. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ 𝑍) ⇒ ⊢ (𝜑 → (𝐵 +s 1s ) ∈ 𝑍) | ||
| Theorem | noseqind 28298* | Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑍 ⊆ 𝐵) | ||
| Theorem | noseqinds 28299* | Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) & ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏)) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂) | ||
| Theorem | noseqssno 28300 | A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → 𝑍 ⊆ No ) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |