| Metamath
Proof Explorer Theorem List (p. 284 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 | noseqno 28301 | An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐵 ∈ No ) | ||
| Theorem | om2noseq0 28302 | The mapping 𝐺 is a one-to-one mapping from ω onto a countable sequence of surreals that will be used to show the properties of seqs. This theorem shows the value of 𝐺 at ordinal zero. Compare the series of theorems starting at om2uz0i 13988. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) ⇒ ⊢ (𝜑 → (𝐺‘∅) = 𝐶) | ||
| Theorem | om2noseqsuc 28303* | The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝐴 ∈ ω) ⇒ ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s )) | ||
| Theorem | om2noseqfo 28304 | Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺:ω–onto→𝑍) | ||
| Theorem | om2noseqlt 28305* | Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵))) | ||
| Theorem | om2noseqlt2 28306* | The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵))) | ||
| Theorem | om2noseqf1o 28307* | 𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍) | ||
| Theorem | om2noseqiso 28308* | 𝐺 is an isomorphism from the finite ordinals to a surreal sequence. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺 Isom E , <s (ω, 𝑍)) | ||
| Theorem | om2noseqoi 28309* | An alternative definition of 𝐺 in terms of df-oi 9550. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍)) | ||
| Theorem | om2noseqrdg 28310* | A helper lemma for the value of a recursive definition generator on a surreal sequence with characteristic function 𝐹(𝑥, 𝑦) and initial value 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ ω) → (𝑅‘𝐵) = 〈(𝐺‘𝐵), (2nd ‘(𝑅‘𝐵))〉) | ||
| Theorem | noseqrdglem 28311* | A helper lemma for the value of a recursive defintion generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 〈𝐵, (2nd ‘(𝑅‘(◡𝐺‘𝐵)))〉 ∈ ran 𝑅) | ||
| Theorem | noseqrdgfn 28312* | The recursive definition generator on surreal sequences is a function. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) & ⊢ (𝜑 → 𝑆 = ran 𝑅) ⇒ ⊢ (𝜑 → 𝑆 Fn 𝑍) | ||
| Theorem | noseqrdg0 28313* | Initial value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) & ⊢ (𝜑 → 𝑆 = ran 𝑅) ⇒ ⊢ (𝜑 → (𝑆‘𝐶) = 𝐴) | ||
| Theorem | noseqrdgsuc 28314* | Successor value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ 〈(𝑥 +s 1s ), (𝑥𝐹𝑦)〉), 〈𝐶, 𝐴〉) ↾ ω)) & ⊢ (𝜑 → 𝑆 = ran 𝑅) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → (𝑆‘(𝐵 +s 1s )) = (𝐵𝐹(𝑆‘𝐵))) | ||
| Theorem | seqsfn 28315 | The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝑀 ∈ No ) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω)) ⇒ ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍) | ||
| Theorem | seqs1 28316 | The value of the surreal sequence bulder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝑀 ∈ No ) ⇒ ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | ||
| Theorem | seqsp1 28317 | The value of the surreal sequence builder at a successor. (Contributed by Scott Fenton, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝑀 ∈ No ) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω)) & ⊢ (𝜑 → 𝑁 ∈ 𝑍) ⇒ ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘(𝑁 +s 1s )) = ((seqs𝑀( + , 𝐹)‘𝑁) + (𝐹‘(𝑁 +s 1s )))) | ||
| Syntax | cnn0s 28318 | Declare the syntax for surreal non-negative integers. |
| class ℕ0s | ||
| Syntax | cnns 28319 | Declare the syntax for surreal positive integers. |
| class ℕs | ||
| Definition | df-n0s 28320 | Define the set of non-negative surreal integers. This set behaves similarly to ω and ℕ0, but it is a set of surreal numbers. Like those two sets, it satisfies the Peano axioms and is closed under (surreal) addition and multiplication. Compare df-nn 12267. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω) | ||
| Definition | df-nns 28321 | Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕs = (ℕ0s ∖ { 0s }) | ||
| Theorem | n0sex 28322 | The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕ0s ∈ V | ||
| Theorem | nnsex 28323 | The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕs ∈ V | ||
| Theorem | peano5n0s 28324* | Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴) | ||
| Theorem | n0ssno 28325 | The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕ0s ⊆ No | ||
| Theorem | nnssn0s 28326 | The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕs ⊆ ℕ0s | ||
| Theorem | nnssno 28327 | The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕs ⊆ No | ||
| Theorem | n0sno 28328 | A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No ) | ||
| Theorem | nnsno 28329 | A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No ) | ||
| Theorem | n0snod 28330 | A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0s) ⇒ ⊢ (𝜑 → 𝐴 ∈ No ) | ||
| Theorem | nnsnod 28331 | A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 𝐴 ∈ No ) | ||
| Theorem | nnn0s 28332 | A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s) | ||
| Theorem | nnn0sd 28333 | A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ0s) | ||
| Theorem | 0n0s 28334 | Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ 0s ∈ ℕ0s | ||
| Theorem | peano2n0s 28335 | Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → (𝐴 +s 1s ) ∈ ℕ0s) | ||
| Theorem | dfn0s2 28336* | Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} | ||
| Theorem | n0sind 28337* | Principle of Mathematical Induction (inference schema). Compare nnind 12284 and finds 7918. (Contributed by Scott Fenton, 17-Mar-2025.) |
| ⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ0s → 𝜏) | ||
| Theorem | n0scut 28338 | A cut form for surreal naturals. (Contributed by Scott Fenton, 2-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅)) | ||
| Theorem | n0ons 28339 | A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ Ons) | ||
| Theorem | nnne0s 28340 | A surreal positive integer is non-zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕs → 𝐴 ≠ 0s ) | ||
| Theorem | n0sge0 28341 | A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → 0s ≤s 𝐴) | ||
| Theorem | nnsgt0 28342 | A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕs → 0s <s 𝐴) | ||
| Theorem | elnns 28343 | Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s )) | ||
| Theorem | elnns2 28344 | A positive surreal integer is a non-negative surreal integer greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 0s <s 𝐴)) | ||
| Theorem | n0s0suc 28345* | A non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-Jul-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → (𝐴 = 0s ∨ ∃𝑥 ∈ ℕ0s 𝐴 = (𝑥 +s 1s ))) | ||
| Theorem | nnsge1 28346 | A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025.) |
| ⊢ (𝑁 ∈ ℕs → 1s ≤s 𝑁) | ||
| Theorem | n0addscl 28347 | The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 +s 𝐵) ∈ ℕ0s) | ||
| Theorem | n0mulscl 28348 | The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 ·s 𝐵) ∈ ℕ0s) | ||
| Theorem | nnaddscl 28349 | The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 +s 𝐵) ∈ ℕs) | ||
| Theorem | nnmulscl 28350 | The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 ·s 𝐵) ∈ ℕs) | ||
| Theorem | 1n0s 28351 | Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ 1s ∈ ℕ0s | ||
| Theorem | 1nns 28352 | Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ 1s ∈ ℕs | ||
| Theorem | peano2nns 28353 | Peano postulate for positive surreal integers. One plus a positive surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕs → (𝐴 +s 1s ) ∈ ℕs) | ||
| Theorem | n0sbday 28354 | A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → ( bday ‘𝐴) ∈ ω) | ||
| Theorem | n0ssold 28355 | The non-negative surreal integers are a subset of the old set of ω. (Contributed by Scott Fenton, 18-Apr-2025.) |
| ⊢ ℕ0s ⊆ ( O ‘ω) | ||
| Theorem | nnsrecgt0d 28356 | The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 0s <s ( 1s /su 𝐴)) | ||
| Theorem | seqn0sfn 28357 | The surreal sequence builder is a function over ℕ0s when started from zero. (Contributed by Scott Fenton, 19-Apr-2025.) |
| ⊢ (𝜑 → seqs 0s ( + , 𝐹) Fn ℕ0s) | ||
| Theorem | eln0s 28358 | A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ ℕs ∨ 𝐴 = 0s )) | ||
| Theorem | n0s0m1 28359 | Every non-negative surreal integer is either zero or a successor. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → (𝐴 = 0s ∨ (𝐴 -s 1s ) ∈ ℕ0s)) | ||
| Theorem | n0subs 28360 | Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕ0s)) | ||
| Theorem | n0p1nns 28361 | One plus a non-negative surreal integer is a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → (𝐴 +s 1s ) ∈ ℕs) | ||
| Theorem | dfnns2 28362 | Alternate definition of the positive surreal integers. Compare df-nn 12267. (Contributed by Scott Fenton, 6-Aug-2025.) |
| ⊢ ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 1s ) “ ω) | ||
| Theorem | nnsind 28363* | Principle of Mathematical Induction (inference schema). (Contributed by Scott Fenton, 6-Aug-2025.) |
| ⊢ (𝑥 = 1s → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕs → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕs → 𝜏) | ||
| Syntax | czs 28364 | Declare the syntax for surreal integers. |
| class ℤs | ||
| Definition | df-zs 28365 | Define the surreal integers. Compare dfz2 12632. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ ℤs = ( -s “ (ℕs × ℕs)) | ||
| Theorem | zsex 28366 | The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ ℤs ∈ V | ||
| Theorem | zssno 28367 | The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ ℤs ⊆ No | ||
| Theorem | zno 28368 | A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ (𝐴 ∈ ℤs → 𝐴 ∈ No ) | ||
| Theorem | znod 28369 | A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤs) ⇒ ⊢ (𝜑 → 𝐴 ∈ No ) | ||
| Theorem | elzs 28370* | Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ (𝐴 ∈ ℤs ↔ ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦)) | ||
| Theorem | nnzsubs 28371 | The difference of two surreal positive integers is an integer. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 -s 𝐵) ∈ ℤs) | ||
| Theorem | nnzs 28372 | A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025.) |
| ⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℤs) | ||
| Theorem | nnzsd 28373 | A positive surreal integer is a surreal integer. Deduction form. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℤs) | ||
| Theorem | 0zs 28374 | Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ 0s ∈ ℤs | ||
| Theorem | n0zs 28375 | A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ ℤs) | ||
| Theorem | n0zsd 28376 | A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ0s) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℤs) | ||
| Theorem | 1zs 28377 | One is a surreal integer. (Contributed by Scott Fenton, 24-Jul-2025.) |
| ⊢ 1s ∈ ℤs | ||
| Theorem | znegscl 28378 | The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℤs → ( -us ‘𝐴) ∈ ℤs) | ||
| Theorem | znegscld 28379 | The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤs) ⇒ ⊢ (𝜑 → ( -us ‘𝐴) ∈ ℤs) | ||
| Theorem | zaddscl 28380 | The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ ((𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs) → (𝐴 +s 𝐵) ∈ ℤs) | ||
| Theorem | zaddscld 28381 | The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤs) & ⊢ (𝜑 → 𝐵 ∈ ℤs) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ ℤs) | ||
| Theorem | zsubscld 28382 | The surreal integers are closed under subtraction. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤs) & ⊢ (𝜑 → 𝐵 ∈ ℤs) ⇒ ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ ℤs) | ||
| Theorem | zmulscld 28383 | The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤs) & ⊢ (𝜑 → 𝐵 ∈ ℤs) ⇒ ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ ℤs) | ||
| Theorem | elzn0s 28384 | A surreal integer is a surreal that is a non-negative integer or whose negative is a non-negative integer. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℤs ↔ (𝐴 ∈ No ∧ (𝐴 ∈ ℕ0s ∨ ( -us ‘𝐴) ∈ ℕ0s))) | ||
| Theorem | elzs2 28385 | A surreal integer is either a positive integer, zero, or the negative of a positive integer. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝑁 ∈ ℤs ↔ (𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ 𝑁 = 0s ∨ ( -us ‘𝑁) ∈ ℕs))) | ||
| Theorem | eln0zs 28386 | Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝑁 ∈ ℕ0s ↔ (𝑁 ∈ ℤs ∧ 0s ≤s 𝑁)) | ||
| Theorem | elnnzs 28387 | Positive surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝑁 ∈ ℕs ↔ (𝑁 ∈ ℤs ∧ 0s <s 𝑁)) | ||
| Theorem | elznns 28388 | Surreal integer property expressed in terms of positive integers and non-negative integers. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝑁 ∈ ℤs ↔ (𝑁 ∈ No ∧ (𝑁 ∈ ℕs ∨ ( -us ‘𝑁) ∈ ℕ0s))) | ||
| Theorem | zn0subs 28389 | The non-negative difference of surreal integers is a non-negative integer. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ ((𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs) → (𝑀 ≤s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕ0s)) | ||
| Theorem | peano5uzs 28390* | Peano's inductive postulate for upper surreal integers. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝜑 → 𝑁 ∈ ℤs) & ⊢ (𝜑 → 𝑁 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 +s 1s ) ∈ 𝐴) ⇒ ⊢ (𝜑 → {𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘} ⊆ 𝐴) | ||
| Theorem | uzsind 28391* | Induction on the upper surreal integers that start at 𝑀. (Contributed by Scott Fenton, 25-Jul-2025.) |
| ⊢ (𝑗 = 𝑀 → (𝜑 ↔ 𝜓)) & ⊢ (𝑗 = 𝑘 → (𝜑 ↔ 𝜒)) & ⊢ (𝑗 = (𝑘 +s 1s ) → (𝜑 ↔ 𝜃)) & ⊢ (𝑗 = 𝑁 → (𝜑 ↔ 𝜏)) & ⊢ (𝑀 ∈ ℤs → 𝜓) & ⊢ ((𝑀 ∈ ℤs ∧ 𝑘 ∈ ℤs ∧ 𝑀 ≤s 𝑘) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ∧ 𝑀 ≤s 𝑁) → 𝜏) | ||
| Theorem | zsbday 28392 | A surreal integer has a finite birthday. (Contributed by Scott Fenton, 26-May-2025.) |
| ⊢ (𝐴 ∈ ℤs → ( bday ‘𝐴) ∈ ω) | ||
| Theorem | zscut 28393 | A cut expression for surreal integers. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ (𝐴 ∈ ℤs → 𝐴 = ({(𝐴 -s 1s )} |s {(𝐴 +s 1s )})) | ||
| Syntax | c2s 28394 | Declare the syntax for surreal two. |
| class 2s | ||
| Definition | df-2s 28395 | Define surreal two. This is the simplest number greater than one. See 1p1e2s 28400 for its addition version. (Contributed by Scott Fenton, 27-May-2025.) |
| ⊢ 2s = ({ 1s } |s ∅) | ||
| Syntax | cexps 28396 | Declare the syntax for surreal exponentiation. |
| class ↑s | ||
| Definition | df-exps 28397* | Define surreal exponentiation. Compare df-exp 14103. (Contributed by Scott Fenton, 27-May-2025.) |
| ⊢ ↑s = (𝑥 ∈ No , 𝑦 ∈ ℤs ↦ if(𝑦 = 0s , 1s , if( 0s <s 𝑦, (seqs 1s ( ·s , (ℕs × {𝑥}))‘𝑦), ( 1s /su (seqs 1s ( ·s , (ℕs × {𝑥}))‘( -us ‘𝑦)))))) | ||
| Syntax | czs12 28398 | Define the syntax for the set of surreal dyadic fractions. |
| class ℤs[1/2] | ||
| Definition | df-zs12 28399* | Define the set of dyadic rationals. This is the set of rationals whose denominator is a power of two. Later we will prove that this is precisely the set of surreals with a finite birthday. (Contributed by Scott Fenton, 27-May-2025.) |
| ⊢ ℤs[1/2] = {𝑥 ∣ ∃𝑦 ∈ ℤs ∃𝑧 ∈ ℕ0s 𝑥 = (𝑦 /su (2s↑s𝑧))} | ||
| Theorem | 1p1e2s 28400 | One plus one is two. Surreal version. (Contributed by Scott Fenton, 27-May-2025.) |
| ⊢ ( 1s +s 1s ) = 2s | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |