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	$$⊢N\in {\mathbb{N}}_s\to N{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$

Proof

Step	Hyp	Ref	Expression
1		nn1m1nns	$$⊢N\in {\mathbb{N}}_s\to \left(N=1_s\vee N{-}_s{1}_s\in {\mathbb{N}}_s\right)$$
2		nnno	$$⊢N\in {\mathbb{N}}_s\to N\in \mathrm{No}$$
3		1no	$$⊢1_s\in \mathrm{No}$$
4	3	a1i	$$⊢N\in {\mathbb{N}}_s\to 1_s\in \mathrm{No}$$
5	2 4	subseq0d	$$⊢N\in {\mathbb{N}}_s\to \left(N{-}_s{1}_s=0_s\leftrightarrow N=1_s\right)$$
6	5	orbi1d	$$⊢N\in {\mathbb{N}}_s\to \left(\left(N{-}_s{1}_s=0_s\vee N{-}_s{1}_s\in {\mathbb{N}}_s\right)\leftrightarrow \left(N=1_s\vee N{-}_s{1}_s\in {\mathbb{N}}_s\right)\right)$$
7	1 6	mpbird	$$⊢N\in {\mathbb{N}}_s\to \left(N{-}_s{1}_s=0_s\vee N{-}_s{1}_s\in {\mathbb{N}}_s\right)$$
8	7	orcomd	$$⊢N\in {\mathbb{N}}_s\to \left(N{-}_s{1}_s\in {\mathbb{N}}_s\vee N{-}_s{1}_s=0_s\right)$$
9		eln0s	$$⊢N{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}\leftrightarrow \left(N{-}_s{1}_s\in {\mathbb{N}}_s\vee N{-}_s{1}_s=0_s\right)$$
10	8 9	sylibr	$$⊢N\in {\mathbb{N}}_s\to N{-}_s{1}_s\in {\mathbb{N}}_{\mathrm{0s}}$$