Theorem nnm1n0s

Description: A positive surreal integer minus one is a non-negative surreal integer. (Contributed by Scott Fenton, 8-Nov-2025)

	Ref	Expression
Assertion	nnm1n0s	⊢ ( 𝑁 ∈ ℕs → ( 𝑁 -s 1s ) ∈ ℕ0s )

Proof

Step	Hyp	Ref	Expression
1		nn1m1nns	⊢ ( 𝑁 ∈ ℕs → ( 𝑁 = 1s ∨ ( 𝑁 -s 1s ) ∈ ℕs ) )
2		nnsno	⊢ ( 𝑁 ∈ ℕs → 𝑁 ∈ No )
3		1sno	⊢ 1s ∈ No
4	3	a1i	⊢ ( 𝑁 ∈ ℕs → 1s ∈ No )
5	2 4	subseq0d	⊢ ( 𝑁 ∈ ℕs → ( ( 𝑁 -s 1s ) = 0s ↔ 𝑁 = 1s ) )
6	5	orbi1d	⊢ ( 𝑁 ∈ ℕs → ( ( ( 𝑁 -s 1s ) = 0s ∨ ( 𝑁 -s 1s ) ∈ ℕs ) ↔ ( 𝑁 = 1s ∨ ( 𝑁 -s 1s ) ∈ ℕs ) ) )
7	1 6	mpbird	⊢ ( 𝑁 ∈ ℕs → ( ( 𝑁 -s 1s ) = 0s ∨ ( 𝑁 -s 1s ) ∈ ℕs ) )
8	7	orcomd	⊢ ( 𝑁 ∈ ℕs → ( ( 𝑁 -s 1s ) ∈ ℕs ∨ ( 𝑁 -s 1s ) = 0s ) )
9		eln0s	⊢ ( ( 𝑁 -s 1s ) ∈ ℕ0s ↔ ( ( 𝑁 -s 1s ) ∈ ℕs ∨ ( 𝑁 -s 1s ) = 0s ) )
10	8 9	sylibr	⊢ ( 𝑁 ∈ ℕs → ( 𝑁 -s 1s ) ∈ ℕ0s )