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 e. NN_s -> ( N -s 1s ) e. NN0_s )

Proof

Step	Hyp	Ref	Expression
1		nn1m1nns	|- ( N e. NN_s -> ( N = 1s \/ ( N -s 1s ) e. NN_s ) )
2		nnsno	|- ( N e. NN_s -> N e. No )
3		1sno	|- 1s e. No
4	3	a1i	|- ( N e. NN_s -> 1s e. No )
5	2 4	subseq0d	|- ( N e. NN_s -> ( ( N -s 1s ) = 0s <-> N = 1s ) )
6	5	orbi1d	|- ( N e. NN_s -> ( ( ( N -s 1s ) = 0s \/ ( N -s 1s ) e. NN_s ) <-> ( N = 1s \/ ( N -s 1s ) e. NN_s ) ) )
7	1 6	mpbird	|- ( N e. NN_s -> ( ( N -s 1s ) = 0s \/ ( N -s 1s ) e. NN_s ) )
8	7	orcomd	|- ( N e. NN_s -> ( ( N -s 1s ) e. NN_s \/ ( N -s 1s ) = 0s ) )
9		eln0s	|- ( ( N -s 1s ) e. NN0_s <-> ( ( N -s 1s ) e. NN_s \/ ( N -s 1s ) = 0s ) )
10	8 9	sylibr	|- ( N e. NN_s -> ( N -s 1s ) e. NN0_s )