Theorem nn1m1nns

Description: Every positive surreal integer is either one or a successor. (Contributed by Scott Fenton, 8-Nov-2025)

	Ref	Expression
Assertion	nn1m1nns	⊢ ( 𝐴 ∈ ℕs → ( 𝐴 = 1s ∨ ( 𝐴 -s 1s ) ∈ ℕs ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 1s → ( 𝑥 = 1s ↔ 1s = 1s ) )
2		oveq1	⊢ ( 𝑥 = 1s → ( 𝑥 -s 1s ) = ( 1s -s 1s ) )
3	2	eleq1d	⊢ ( 𝑥 = 1s → ( ( 𝑥 -s 1s ) ∈ ℕs ↔ ( 1s -s 1s ) ∈ ℕs ) )
4	1 3	orbi12d	⊢ ( 𝑥 = 1s → ( ( 𝑥 = 1s ∨ ( 𝑥 -s 1s ) ∈ ℕs ) ↔ ( 1s = 1s ∨ ( 1s -s 1s ) ∈ ℕs ) ) )
5		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 1s ↔ 𝑦 = 1s ) )
6		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 -s 1s ) = ( 𝑦 -s 1s ) )
7	6	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 -s 1s ) ∈ ℕs ↔ ( 𝑦 -s 1s ) ∈ ℕs ) )
8	5 7	orbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = 1s ∨ ( 𝑥 -s 1s ) ∈ ℕs ) ↔ ( 𝑦 = 1s ∨ ( 𝑦 -s 1s ) ∈ ℕs ) ) )
9		eqeq1	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑥 = 1s ↔ ( 𝑦 +s 1s ) = 1s ) )
10		oveq1	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( 𝑥 -s 1s ) = ( ( 𝑦 +s 1s ) -s 1s ) )
11	10	eleq1d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝑥 -s 1s ) ∈ ℕs ↔ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕs ) )
12	9 11	orbi12d	⊢ ( 𝑥 = ( 𝑦 +s 1s ) → ( ( 𝑥 = 1s ∨ ( 𝑥 -s 1s ) ∈ ℕs ) ↔ ( ( 𝑦 +s 1s ) = 1s ∨ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕs ) ) )
13		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 1s ↔ 𝐴 = 1s ) )
14		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 -s 1s ) = ( 𝐴 -s 1s ) )
15	14	eleq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 -s 1s ) ∈ ℕs ↔ ( 𝐴 -s 1s ) ∈ ℕs ) )
16	13 15	orbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 1s ∨ ( 𝑥 -s 1s ) ∈ ℕs ) ↔ ( 𝐴 = 1s ∨ ( 𝐴 -s 1s ) ∈ ℕs ) ) )
17		eqid	⊢ 1s = 1s
18	17	orci	⊢ ( 1s = 1s ∨ ( 1s -s 1s ) ∈ ℕs )
19		nnsno	⊢ ( 𝑦 ∈ ℕs → 𝑦 ∈ No )
20		1sno	⊢ 1s ∈ No
21		pncans	⊢ ( ( 𝑦 ∈ No ∧ 1s ∈ No ) → ( ( 𝑦 +s 1s ) -s 1s ) = 𝑦 )
22	19 20 21	sylancl	⊢ ( 𝑦 ∈ ℕs → ( ( 𝑦 +s 1s ) -s 1s ) = 𝑦 )
23		id	⊢ ( 𝑦 ∈ ℕs → 𝑦 ∈ ℕs )
24	22 23	eqeltrd	⊢ ( 𝑦 ∈ ℕs → ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕs )
25	24	olcd	⊢ ( 𝑦 ∈ ℕs → ( ( 𝑦 +s 1s ) = 1s ∨ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕs ) )
26	25	a1d	⊢ ( 𝑦 ∈ ℕs → ( ( 𝑦 = 1s ∨ ( 𝑦 -s 1s ) ∈ ℕs ) → ( ( 𝑦 +s 1s ) = 1s ∨ ( ( 𝑦 +s 1s ) -s 1s ) ∈ ℕs ) ) )
27	4 8 12 16 18 26	nnsind	⊢ ( 𝐴 ∈ ℕs → ( 𝐴 = 1s ∨ ( 𝐴 -s 1s ) ∈ ℕs ) )