P. 284 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 28301-28400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	noseqrdglem 28301*	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 28302*	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 28303*	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 28304*	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 28305	The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    &   ⊢ (𝜑 → 𝑍 = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 𝑀) “ ω))    ⇒   ⊢ (𝜑 → seqs𝑀( + , 𝐹) Fn 𝑍)
Theorem	seqs1 28306	The value of the surreal sequence bulder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝑀 ∈ No )    ⇒   ⊢ (𝜑 → (seqs𝑀( + , 𝐹)‘𝑀) = (𝐹‘𝑀))
Theorem	seqsp1 28307	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 ))))
15.6.3  Natural numbers
Syntax	cn0s 28308	Declare the syntax for surreal non-negative integers.
class ℕ0s
Syntax	cnns 28309	Declare the syntax for surreal positive integers.
class ℕs
Definition	df-n0s 28310	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 12146. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 0s ) “ ω)
Definition	df-nns 28311	Define the set of positive surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs = (ℕ0s ∖ { 0s })
Theorem	n0sexg 28312	The set of all non-negative surreal integers exists. This theorem avoids the axiom of infinity by including it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2025.)
⊢ (ω ∈ V → ℕ0s ∈ V)
Theorem	n0sex 28313	The set of all non-negative surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ∈ V
Theorem	nnsex 28314	The set of all positive surreal integers exists. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ∈ V
Theorem	peano5n0s 28315*	Peano's inductive postulate for non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (( 0s ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑥 +s 1s ) ∈ 𝐴) → ℕ0s ⊆ 𝐴)
Theorem	n0ssno 28316	The non-negative surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s ⊆ No
Theorem	nnssn0s 28317	The positive surreal integers are a subset of the non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ ℕ0s
Theorem	nnssno 28318	The positive surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕs ⊆ No
Theorem	n0no 28319	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ No )
Theorem	nnno 28320	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ No )
Theorem	n0nod 28321	A non-negative surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnnod 28322	A positive surreal integer is a surreal. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	nnn0s 28323	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℕ0s)
Theorem	nnn0sd 28324	A positive surreal integer is a non-negative surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℕ0s)
Theorem	0n0s 28325	Peano postulate: 0s is a non-negative surreal integer. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ 0s ∈ ℕ0s
Theorem	peano2n0s 28326	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	peano2n0sd 28327	Peano postulate: the successor of a non-negative surreal integer is a non-negative surreal integer. Deduction form. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → (𝐴 +s 1s ) ∈ ℕ0s)
Theorem	dfn0s2 28328*	Alternate definition of the set of non-negative surreal integers. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ ℕ0s = ∩ {𝑥 ∣ ( 0s ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 +s 1s ) ∈ 𝑥)}
Theorem	n0sind 28329*	Principle of Mathematical Induction (inference schema). Compare nnind 12163 and finds 7838. (Contributed by Scott Fenton, 17-Mar-2025.)
⊢ (𝑥 = 0s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕ0s → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕ0s → 𝜏)
Theorem	n0cut 28330	A cut form for non-negative surreal integers. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({(𝐴 -s 1s )} |s ∅))
Theorem	n0cut2 28331	A cut form for the successor of a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 +s 1s ) = ({𝐴} |s ∅))
Theorem	n0on 28332	A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ Ons)
Theorem	nnne0s 28333	A surreal positive integer is non-zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ≠ 0s )
Theorem	n0sge0 28334	A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → 0s ≤s 𝐴)
Theorem	nnsgt0 28335	A positive integer is greater than zero. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs → 0s <s 𝐴)
Theorem	elnns 28336	Membership in the positive surreal integers. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ (𝐴 ∈ ℕs ↔ (𝐴 ∈ ℕ0s ∧ 𝐴 ≠ 0s ))
Theorem	elnns2 28337	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 28338*	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 28339	A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025.)
⊢ (𝑁 ∈ ℕs → 1s ≤s 𝑁)
Theorem	n0addscl 28340	The non-negative surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 +s 𝐵) ∈ ℕ0s)
Theorem	n0mulscl 28341	The non-negative surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕ0s) → (𝐴 ·s 𝐵) ∈ ℕ0s)
Theorem	nnaddscl 28342	The positive surreal integers are closed under addition. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 +s 𝐵) ∈ ℕs)
Theorem	nnmulscl 28343	The positive surreal integers are closed under multiplication. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 ·s 𝐵) ∈ ℕs)
Theorem	1n0s 28344	Surreal one is a non-negative surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕ0s
Theorem	1nns 28345	Surreal one is a positive surreal integer. (Contributed by Scott Fenton, 15-Apr-2025.)
⊢ 1s ∈ ℕs
Theorem	peano2nns 28346	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	nnsrecgt0d 28347	The reciprocal of a positive surreal integer is positive. (Contributed by Scott Fenton, 19-Apr-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 0s <s ( 1s /su 𝐴))
Theorem	n0bday 28348	A non-negative surreal integer has a finite birthday. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ (𝐴 ∈ ℕ0s → ( bday ‘𝐴) ∈ ω)
Theorem	n0ssoldg 28349	The non-negative surreal integers are a subset of the old set of ω. To avoid the axiom of infinity, we include it as an antecedent. (Contributed by Scott Fenton, 20-Feb-2026.)
⊢ (ω ∈ V → ℕ0s ⊆ ( O ‘ω))
Theorem	n0ssold 28350	The non-negative surreal integers are a subset of the old set of ω. (Contributed by Scott Fenton, 18-Apr-2025.)
⊢ ℕ0s ⊆ ( O ‘ω)
Theorem	n0fincut 28351	The simplest number greater than a finite set of non-negative surreal integers is a non-negative surreal integer. (Contributed by Scott Fenton, 5-Nov-2025.)
⊢ ((𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin) → (𝐴 |s ∅) ∈ ℕ0s)
Theorem	onsfi 28352	A surreal ordinal with a finite birthday is a non-negative surreal integer. (Contributed by Scott Fenton, 4-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ ( bday ‘𝐴) ∈ ω) → 𝐴 ∈ ℕ0s)
Theorem	eln0s2 28353	A non-negative surreal integer is a surreal ordinal with a finite birthday. (Contributed by Scott Fenton, 27-Feb-2026.)
⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ Ons ∧ ( bday ‘𝐴) ∈ ω))
Theorem	onltn0s 28354	A surreal ordinal that is less than a non-negative integer is a non-negative integer. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝐴 ∈ Ons ∧ 𝐵 ∈ ℕ0s ∧ 𝐴 <s 𝐵) → 𝐴 ∈ ℕ0s)
Theorem	n0cutlt 28355*	A non-negative surreal integer is the simplest number greater than all previous non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 = ({𝑥 ∈ ℕ0s ∣ 𝑥 <s 𝐴} |s ∅))
Theorem	seqn0sfn 28356	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 28357	A non-negative surreal integer is zero or a positive surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s ↔ (𝐴 ∈ ℕs ∨ 𝐴 = 0s ))
Theorem	n0s0m1 28358	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 28359	Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 26-May-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕ0s))
Theorem	n0subs2 28360	Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 <s 𝑁 ↔ (𝑁 -s 𝑀) ∈ ℕs))
Theorem	n0ltsp1le 28361	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 <s 𝑁 ↔ (𝑀 +s 1s ) ≤s 𝑁))
Theorem	n0lesltp1 28362	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ 𝑀 <s (𝑁 +s 1s )))
Theorem	n0lesm1lt 28363	Non-negative surreal ordering relation. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s) → (𝑀 ≤s 𝑁 ↔ (𝑀 -s 1s ) <s 𝑁))
Theorem	n0lts1e0 28364	A non-negative surreal integer is less than one iff it is zero. (Contributed by Scott Fenton, 23-Feb-2026.)
⊢ (𝐴 ∈ ℕ0s → (𝐴 <s 1s ↔ 𝐴 = 0s ))
Theorem	bdayn0p1 28365	The birthday of 𝐴 +s 1s is the successor of the birthday of 𝐴 when 𝐴 is a non-negative surreal integer. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ (𝐴 ∈ ℕ0s → ( bday ‘(𝐴 +s 1s )) = suc ( bday ‘𝐴))
Theorem	bdayn0sf1o 28366	The birthday function restricted to the non-negative surreal integers is a bijection with the finite ordinals. (Contributed by Scott Fenton, 7-Nov-2025.)
⊢ ( bday ↾ ℕ0s):ℕ0s–1-1-onto→ω
Theorem	n0p1nns 28367	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 28368	Alternate definition of the positive surreal integers. Compare df-nn 12146. (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )), 1s ) “ ω)
Theorem	nnsind 28369*	Principle of Mathematical Induction (inference schema). (Contributed by Scott Fenton, 6-Aug-2025.)
⊢ (𝑥 = 1s → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 +s 1s ) → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))    &   ⊢ 𝜓    &   ⊢ (𝑦 ∈ ℕs → (𝜒 → 𝜃))    ⇒   ⊢ (𝐴 ∈ ℕs → 𝜏)
Theorem	nn1m1nns 28370	Every positive surreal integer is either one or a successor. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝐴 ∈ ℕs → (𝐴 = 1s ∨ (𝐴 -s 1s ) ∈ ℕs))
Theorem	nnm1n0s 28371	A positive surreal integer minus one is a non-negative surreal integer. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ (𝑁 ∈ ℕs → (𝑁 -s 1s ) ∈ ℕ0s)
Theorem	eucliddivs 28372*	Euclid's division lemma for surreal numbers. (Contributed by Scott Fenton, 8-Nov-2025.)
⊢ ((𝐴 ∈ ℕ0s ∧ 𝐵 ∈ ℕs) → ∃𝑝 ∈ ℕ0s ∃𝑞 ∈ ℕ0s (𝐴 = ((𝐵 ·s 𝑝) +s 𝑞) ∧ 𝑞 <s 𝐵))
Theorem	oldfib 28373	The old set of an ordinal is finite iff the ordinal is finite. (Contributed by Scott Fenton, 19-Feb-2026.)
⊢ (𝐴 ∈ On → (𝐴 ∈ ω ↔ ( O ‘𝐴) ∈ Fin))
15.6.4  Integers
Syntax	czs 28374	Declare the syntax for surreal integers.
class ℤs
Definition	df-zs 28375	Define the surreal integers. Compare dfz2 12507. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs = ( -s “ (ℕs × ℕs))
Theorem	zsex 28376	The surreal integers form a set. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs ∈ V
Theorem	zssno 28377	The surreal integers are a subset of the surreals. (Contributed by Scott Fenton, 17-May-2025.)
⊢ ℤs ⊆ No
Theorem	zno 28378	A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℤs → 𝐴 ∈ No )
Theorem	znod 28379	A surreal integer is a surreal. Deduction form. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ No )
Theorem	elzs 28380*	Membership in the set of surreal integers. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℤs ↔ ∃𝑥 ∈ ℕs ∃𝑦 ∈ ℕs 𝐴 = (𝑥 -s 𝑦))
Theorem	nnzsubs 28381	The difference of two surreal positive integers is an integer. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs) → (𝐴 -s 𝐵) ∈ ℤs)
Theorem	nnzs 28382	A positive surreal integer is a surreal integer. (Contributed by Scott Fenton, 17-May-2025.)
⊢ (𝐴 ∈ ℕs → 𝐴 ∈ ℤs)
Theorem	nnzsd 28383	A positive surreal integer is a surreal integer. Deduction form. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕs)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤs)
Theorem	0zs 28384	Zero is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ 0s ∈ ℤs
Theorem	n0zs 28385	A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℕ0s → 𝐴 ∈ ℤs)
Theorem	n0zsd 28386	A non-negative surreal integer is a surreal integer. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℕ0s)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ℤs)
Theorem	1zs 28387	One is a surreal integer. (Contributed by Scott Fenton, 24-Jul-2025.)
⊢ 1s ∈ ℤs
Theorem	znegscl 28388	The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝐴 ∈ ℤs → ( -us ‘𝐴) ∈ ℤs)
Theorem	znegscld 28389	The surreal integers are closed under negation. (Contributed by Scott Fenton, 26-May-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    ⇒   ⊢ (𝜑 → ( -us ‘𝐴) ∈ ℤs)
Theorem	zaddscl 28390	The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ ((𝐴 ∈ ℤs ∧ 𝐵 ∈ ℤs) → (𝐴 +s 𝐵) ∈ ℤs)
Theorem	zaddscld 28391	The surreal integers are closed under addition. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝐵 ∈ ℤs)    ⇒   ⊢ (𝜑 → (𝐴 +s 𝐵) ∈ ℤs)
Theorem	zsubscld 28392	The surreal integers are closed under subtraction. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝐵 ∈ ℤs)    ⇒   ⊢ (𝜑 → (𝐴 -s 𝐵) ∈ ℤs)
Theorem	zmulscld 28393	The surreal integers are closed under multiplication. (Contributed by Scott Fenton, 20-Aug-2025.)
⊢ (𝜑 → 𝐴 ∈ ℤs)    &   ⊢ (𝜑 → 𝐵 ∈ ℤs)    ⇒   ⊢ (𝜑 → (𝐴 ·s 𝐵) ∈ ℤs)
Theorem	elzn0s 28394	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 28395	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 28396	Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑁 ∈ ℕ0s ↔ (𝑁 ∈ ℤs ∧ 0s ≤s 𝑁))
Theorem	elnnzs 28397	Positive surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝑁 ∈ ℕs ↔ (𝑁 ∈ ℤs ∧ 0s <s 𝑁))
Theorem	elznns 28398	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 28399	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 28400*	Peano's inductive postulate for upper surreal integers. (Contributed by Scott Fenton, 25-Jul-2025.)
⊢ (𝜑 → 𝑁 ∈ ℤs)    &   ⊢ (𝜑 → 𝑁 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 +s 1s ) ∈ 𝐴)    ⇒   ⊢ (𝜑 → {𝑘 ∈ ℤs ∣ 𝑁 ≤s 𝑘} ⊆ 𝐴)