Theorem nnsge1

Description: A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025)

	Ref	Expression
Assertion	nnsge1	$$⊢N\in {\mathbb{N}}_s\to 1_s{\le }_{s}N$$

Proof

Step	Hyp	Ref	Expression
1		elnns	$$⊢N\in {\mathbb{N}}_s\leftrightarrow \left(N\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\ne 0_s\right)$$
2		n0s0suc	$$⊢N\in {\mathbb{N}}_{\mathrm{0s}}\to \left(N=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\right)$$
3		neneq	$$⊢N\ne 0_s\to \neg N=0_s$$
4		pm2.53	$$⊢\left(N=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\right)\to \left(\neg N=0_s\to \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\right)$$
5	4	imp	$$⊢\left(\left(N=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\right)\wedge \neg N=0_s\right)\to \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s$$
6		1sno	$$⊢1_s\in \mathrm{No}$$
7		addslid	$$⊢1_s\in \mathrm{No}\to 0_s{+}_s{1}_s=1_s$$
8	6 7	ax-mp	$$⊢0_s{+}_s{1}_s=1_s$$
9		n0sge0	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to 0_s{\le }_{s}x$$
10		n0sno	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to x\in \mathrm{No}$$
11		0sno	$$⊢0_s\in \mathrm{No}$$
12		sleadd1	$$⊢\left(0_s\in \mathrm{No}\wedge x\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(0_s{\le }_{s}x\leftrightarrow \left(0_s{+}_s{1}_s\right){\le }_s\left(x{+}_s{1}_s\right)\right)$$
13	11 6 12	mp3an13	$$⊢x\in \mathrm{No}\to \left(0_s{\le }_{s}x\leftrightarrow \left(0_s{+}_s{1}_s\right){\le }_s\left(x{+}_s{1}_s\right)\right)$$
14	10 13	syl	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s{\le }_{s}x\leftrightarrow \left(0_s{+}_s{1}_s\right){\le }_s\left(x{+}_s{1}_s\right)\right)$$
15	9 14	mpbid	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left(0_s{+}_s{1}_s\right){\le }_s\left(x{+}_s{1}_s\right)$$
16	8 15	eqbrtrrid	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to 1_s{\le }_s\left(x{+}_s{1}_s\right)$$
17		breq2	$$⊢N=x{+}_s{1}_s\to \left(1_s{\le }_{s}N\leftrightarrow 1_s{\le }_s\left(x{+}_s{1}_s\right)\right)$$
18	16 17	syl5ibrcom	$$⊢x\in {\mathbb{N}}_{\mathrm{0s}}\to \left(N=x{+}_s{1}_s\to 1_s{\le }_{s}N\right)$$
19	18	rexlimiv	$$⊢\exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\to 1_s{\le }_{s}N$$
20	5 19	syl	$$⊢\left(\left(N=0_s\vee \exists x\in {\mathbb{N}}_{\mathrm{0s}}N=x{+}_s{1}_s\right)\wedge \neg N=0_s\right)\to 1_s{\le }_{s}N$$
21	2 3 20	syl2an	$$⊢\left(N\in {\mathbb{N}}_{\mathrm{0s}}\wedge N\ne 0_s\right)\to 1_s{\le }_{s}N$$
22	1 21	sylbi	$$⊢N\in {\mathbb{N}}_s\to 1_s{\le }_{s}N$$