![]() |
Metamath
Proof Explorer Theorem List (p. 284 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 | onmulscl 28301 | The surreal ordinals are closed under multiplication. (Contributed by Scott Fenton, 22-Aug-2025.) |
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ Ons) → (𝐴 ·s 𝐵) ∈ Ons) | ||
Theorem | peano2ons 28302 | The successor of a surreal ordinal is a surreal ordinal. (Contributed by Scott Fenton, 22-Aug-2025.) |
⊢ (𝐴 ∈ Ons → (𝐴 +s 1s ) ∈ Ons) | ||
Syntax | cseqs 28303 | Extend class notation with the surreal recursive sequence builder. |
class seqs𝑀( + , 𝐹) | ||
Definition | df-seqs 28304* | Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14039. 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 28305 | Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ seqs𝑀( + , 𝐹) ∈ V | ||
Theorem | seqseq123d 28306 | Equality deduction for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝑀 = 𝑁) & ⊢ (𝜑 → + = 𝑄) & ⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → seqs𝑀( + , 𝐹) = seqs𝑁(𝑄, 𝐺)) | ||
Theorem | nfseqs 28307 | Hypothesis builder for the surreal sequence builder. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ Ⅎ𝑥𝑀 & ⊢ Ⅎ𝑥 + & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥seqs𝑀( + , 𝐹) | ||
Theorem | seqsval 28308* | 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 28309 | 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 28310 | The surreal 𝐴 is a member of the sequence starting at 𝐴. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑍) | ||
Theorem | noseqp1 28311* | 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 28312* | Peano's inductive postulate for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑦 +s 1s ) ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑍 ⊆ 𝐵) | ||
Theorem | noseqinds 28313* | Induction schema for surreal sequences. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝑦 = 𝐴 → (𝜓 ↔ 𝜒)) & ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃)) & ⊢ (𝑦 = (𝑧 +s 1s ) → (𝜓 ↔ 𝜏)) & ⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑍) → (𝜃 → 𝜏)) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝑍) → 𝜂) | ||
Theorem | noseqssno 28314 | A surreal sequence is a subset of the surreals. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) ⇒ ⊢ (𝜑 → 𝑍 ⊆ No ) | ||
Theorem | noseqno 28315 | An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐴) “ ω)) & ⊢ (𝜑 → 𝐴 ∈ No ) & ⊢ (𝜑 → 𝐵 ∈ 𝑍) ⇒ ⊢ (𝜑 → 𝐵 ∈ No ) | ||
Theorem | om2noseq0 28316 | 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 13984. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) ⇒ ⊢ (𝜑 → (𝐺‘∅) = 𝐶) | ||
Theorem | om2noseqsuc 28317* | The value of 𝐺 at a successor. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝐴 ∈ ω) ⇒ ⊢ (𝜑 → (𝐺‘suc 𝐴) = ((𝐺‘𝐴) +s 1s )) | ||
Theorem | om2noseqfo 28318 | Function statement for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺:ω–onto→𝑍) | ||
Theorem | om2noseqlt 28319* | Surreal less-than relation for 𝐺. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 → (𝐺‘𝐴) <s (𝐺‘𝐵))) | ||
Theorem | om2noseqlt2 28320* | The mapping 𝐺 preserves order. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ ((𝜑 ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐴 ∈ 𝐵 ↔ (𝐺‘𝐴) <s (𝐺‘𝐵))) | ||
Theorem | om2noseqf1o 28321* | 𝐺 is a bijection. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺:ω–1-1-onto→𝑍) | ||
Theorem | om2noseqiso 28322* | 𝐺 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 28323* | An alternative definition of 𝐺 in terms of df-oi 9547. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝜑 → 𝐶 ∈ No ) & ⊢ (𝜑 → 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) ↾ ω)) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝐶) “ ω)) ⇒ ⊢ (𝜑 → 𝐺 = OrdIso( <s , 𝑍)) | ||
Theorem | om2noseqrdg 28324* | 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 28325* | 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 28326* | 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 28327* | 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 28328* | 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 28329 | The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.) |
⊢ (𝜑 → 𝑀 ∈ No ) & ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω)) ⇒ ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍) | ||
Theorem | seqs1 28330 | The value of the surreal sequence bulder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.) |
⊢ (𝜑 → 𝑀 ∈ No ) ⇒ ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀)) | ||
Theorem | seqsp1 28331 | 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 28332 | Declare the syntax for surreal non-negative integers. |
class ℕ0s | ||
Syntax | cnns 28333 | Declare the syntax for surreal positive integers. |
class ℕs | ||
Definition | df-n0s 28334 | 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 12264. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω) | ||
Definition | df-nns 28335 | Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕs = (ℕ0s ∖ { 0s }) | ||
Theorem | n0sex 28336 | The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕ0s ∈ V | ||
Theorem | nnsex 28337 | The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕs ∈ V | ||
Theorem | peano5n0s 28338* | Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴) | ||
Theorem | n0ssno 28339 | The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕ0s ⊆ No | ||
Theorem | nnssn0s 28340 | The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕs ⊆ ℕ0s | ||
Theorem | nnssno 28341 | The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕs ⊆ No | ||
Theorem | n0sno 28342 | A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No ) | ||
Theorem | nnsno 28343 | A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No ) | ||
Theorem | n0snod 28344 | A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0s) ⇒ ⊢ (𝜑 → 𝐴 ∈ No ) | ||
Theorem | nnsnod 28345 | A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 𝐴 ∈ No ) | ||
Theorem | nnn0s 28346 | A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s) | ||
Theorem | nnn0sd 28347 | A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℕ0s) | ||
Theorem | 0n0s 28348 | Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ 0s ∈ ℕ0s | ||
Theorem | peano2n0s 28349 | 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 28350* | Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)} | ||
Theorem | n0sind 28351* | Principle of Mathematical Induction (inference schema). Compare nnind 12281 and finds 7918. (Contributed by Scott Fenton, 17-Mar-2025.) |
⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕ0s → 𝜏) | ||
Theorem | n0scut 28352 | A cut form for surreal naturals. (Contributed by Scott Fenton, 2-Apr-2025.) |
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅)) | ||
Theorem | n0ons 28353 | A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.) |
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ Ons) | ||
Theorem | nnne0s 28354 | A surreal positive integer is non-zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝐴 ∈ ℕs → 𝐴 ≠ 0s ) | ||
Theorem | n0sge0 28355 | A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝐴 ∈ ℕ0s → 0s ≤s 𝐴) | ||
Theorem | nnsgt0 28356 | A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝐴 ∈ ℕs → 0s <s 𝐴) | ||
Theorem | elnns 28357 | Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s )) | ||
Theorem | elnns2 28358 | 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 28359* | 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 28360 | A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025.) |
⊢ (𝑁 ∈ ℕs → 1s ≤s 𝑁) | ||
Theorem | n0addscl 28361 | The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 +s 𝐵) ∈ ℕ0s) | ||
Theorem | n0mulscl 28362 | The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 ·s 𝐵) ∈ ℕ0s) | ||
Theorem | nnaddscl 28363 | The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 +s 𝐵) ∈ ℕs) | ||
Theorem | nnmulscl 28364 | The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 ·s 𝐵) ∈ ℕs) | ||
Theorem | 1n0s 28365 | Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ 1s ∈ ℕ0s | ||
Theorem | 1nns 28366 | Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.) |
⊢ 1s ∈ ℕs | ||
Theorem | peano2nns 28367 | 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 28368 | A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ (𝐴 ∈ ℕ0s → ( bday ‘𝐴) ∈ ω) | ||
Theorem | n0ssold 28369 | The non-negative surreal integers are a subset of the old set of ω. (Contributed by Scott Fenton, 18-Apr-2025.) |
⊢ ℕ0s ⊆ ( O ‘ω) | ||
Theorem | nnsrecgt0d 28370 | The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 0s <s ( 1s /su 𝐴)) | ||
Theorem | seqn0sfn 28371 | 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 28372 | A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ ℕs ∨ 𝐴 = 0s )) | ||
Theorem | n0s0m1 28373 | 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 28374 | Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕ0s)) | ||
Theorem | n0p1nns 28375 | 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 28376 | Alternate definition of the positive surreal integers. Compare df-nn 12264. (Contributed by Scott Fenton, 6-Aug-2025.) |
⊢ ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 1s ) “ ω) | ||
Theorem | nnsind 28377* | Principle of Mathematical Induction (inference schema). (Contributed by Scott Fenton, 6-Aug-2025.) |
⊢ (𝑥 = 1s → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) & ⊢ 𝜓 & ⊢ (𝑦 ∈ ℕs → (𝜒 → 𝜃)) ⇒ ⊢ (𝐴 ∈ ℕs → 𝜏) | ||
Syntax | czs 28378 | Declare the syntax for surreal integers. |
class ℤs | ||
Definition | df-zs 28379 | Define the surreal integers. Compare dfz2 12629. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ ℤs = ( -s “ (ℕs × ℕs)) | ||
Theorem | zsex 28380 | The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ ℤs ∈ V | ||
Theorem | zssno 28381 | The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ ℤs ⊆ No | ||
Theorem | zno 28382 | A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ No ) | ||
Theorem | znod 28383 | A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℤs) ⇒ ⊢ (𝜑 → 𝐴 ∈ No ) | ||
Theorem | elzs 28384* | Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ (𝐴 ∈ ℤs ↔ ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦)) | ||
Theorem | nnzsubs 28385 | The difference of two surreal positive integers is an integer. (Contributed by Scott Fenton, 25-Jul-2025.) |
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 -s 𝐵) ∈ ℤs) | ||
Theorem | nnzs 28386 | A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025.) |
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℤs) | ||
Theorem | nnzsd 28387 | A positive surreal integer is a surreal integer. Deduction form. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℕs) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℤs) | ||
Theorem | 0zs 28388 | Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ 0s ∈ ℤs | ||
Theorem | n0zs 28389 | A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ ℤs) | ||
Theorem | n0zsd 28390 | A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℕ0s) ⇒ ⊢ (𝜑 → 𝐴 ∈ ℤs) | ||
Theorem | 1zs 28391 | One is a surreal integer. (Contributed by Scott Fenton, 24-Jul-2025.) |
⊢ 1s ∈ ℤs | ||
Theorem | znegscl 28392 | The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝐴 ∈ ℤs → ( -us ‘𝐴) ∈ ℤs) | ||
Theorem | znegscld 28393 | The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℤs) ⇒ ⊢ (𝜑 → ( -us ‘𝐴) ∈ ℤs) | ||
Theorem | zaddscl 28394 | The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.) |
⊢ ((𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs) → (𝐴 +s 𝐵) ∈ ℤs) | ||
Theorem | zaddscld 28395 | The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℤs) & ⊢ (𝜑 → 𝐵 ∈ ℤs) ⇒ ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ ℤs) | ||
Theorem | zsubscld 28396 | The surreal integers are closed under subtraction. (Contributed by Scott Fenton, 25-Jul-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℤs) & ⊢ (𝜑 → 𝐵 ∈ ℤs) ⇒ ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ ℤs) | ||
Theorem | zmulscld 28397 | The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025.) |
⊢ (𝜑 → 𝐴 ∈ ℤs) & ⊢ (𝜑 → 𝐵 ∈ ℤs) ⇒ ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ ℤs) | ||
Theorem | elzn0s 28398 | 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 28399 | 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 28400 | Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.) |
⊢ (𝑁 ∈ ℕ0s ↔ (𝑁 ∈ ℤs ∧ 0s ≤s 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |