Theorem nn1m1nns

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

	Ref	Expression
Assertion	nn1m1nns	$$⊢A\in {\mathbb{N}}_s\to \left(A=1_s\vee A{-}_s{1}_s\in {\mathbb{N}}_s\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢x=1_s\to \left(x=1_s\leftrightarrow 1_s=1_s\right)$$
2		oveq1	$$⊢x=1_s\to x{-}_s{1}_s=1_s{-}_s{1}_s$$
3	2	eleq1d	$$⊢x=1_s\to \left(x{-}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow 1_s{-}_s{1}_s\in {\mathbb{N}}_s\right)$$
4	1 3	orbi12d	$$⊢x=1_s\to \left(\left(x=1_s\vee x{-}_s{1}_s\in {\mathbb{N}}_s\right)\leftrightarrow \left(1_s=1_s\vee 1_s{-}_s{1}_s\in {\mathbb{N}}_s\right)\right)$$
5		eqeq1	$$⊢x=y\to \left(x=1_s\leftrightarrow y=1_s\right)$$
6		oveq1	$$⊢x=y\to x{-}_s{1}_s=y{-}_s{1}_s$$
7	6	eleq1d	$$⊢x=y\to \left(x{-}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow y{-}_s{1}_s\in {\mathbb{N}}_s\right)$$
8	5 7	orbi12d	$$⊢x=y\to \left(\left(x=1_s\vee x{-}_s{1}_s\in {\mathbb{N}}_s\right)\leftrightarrow \left(y=1_s\vee y{-}_s{1}_s\in {\mathbb{N}}_s\right)\right)$$
9		eqeq1	$$⊢x=y{+}_s{1}_s\to \left(x=1_s\leftrightarrow y{+}_s{1}_s=1_s\right)$$
10		oveq1	$$⊢x=y{+}_s{1}_s\to x{-}_s{1}_s=\left(y{+}_s{1}_s\right){-}_s{1}_s$$
11	10	eleq1d	$$⊢x=y{+}_s{1}_s\to \left(x{-}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_s\right)$$
12	9 11	orbi12d	$$⊢x=y{+}_s{1}_s\to \left(\left(x=1_s\vee x{-}_s{1}_s\in {\mathbb{N}}_s\right)\leftrightarrow \left(y{+}_s{1}_s=1_s\vee \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_s\right)\right)$$
13		eqeq1	$$⊢x=A\to \left(x=1_s\leftrightarrow A=1_s\right)$$
14		oveq1	$$⊢x=A\to x{-}_s{1}_s=A{-}_s{1}_s$$
15	14	eleq1d	$$⊢x=A\to \left(x{-}_s{1}_s\in {\mathbb{N}}_s\leftrightarrow A{-}_s{1}_s\in {\mathbb{N}}_s\right)$$
16	13 15	orbi12d	$$⊢x=A\to \left(\left(x=1_s\vee x{-}_s{1}_s\in {\mathbb{N}}_s\right)\leftrightarrow \left(A=1_s\vee A{-}_s{1}_s\in {\mathbb{N}}_s\right)\right)$$
17		eqid	$$⊢1_s=1_s$$
18	17	orci	$$⊢\left(1_s=1_s\vee 1_s{-}_s{1}_s\in {\mathbb{N}}_s\right)$$
19		nnno	$$⊢y\in {\mathbb{N}}_s\to y\in \mathrm{No}$$
20		1no	$$⊢1_s\in \mathrm{No}$$
21		pncans	$$⊢\left(y\in \mathrm{No}\wedge 1_s\in \mathrm{No}\right)\to \left(y{+}_s{1}_s\right){-}_s{1}_s=y$$
22	19 20 21	sylancl	$$⊢y\in {\mathbb{N}}_s\to \left(y{+}_s{1}_s\right){-}_s{1}_s=y$$
23		id	$$⊢y\in {\mathbb{N}}_s\to y\in {\mathbb{N}}_s$$
24	22 23	eqeltrd	$$⊢y\in {\mathbb{N}}_s\to \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_s$$
25	24	olcd	$$⊢y\in {\mathbb{N}}_s\to \left(y{+}_s{1}_s=1_s\vee \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_s\right)$$
26	25	a1d	$$⊢y\in {\mathbb{N}}_s\to \left(\left(y=1_s\vee y{-}_s{1}_s\in {\mathbb{N}}_s\right)\to \left(y{+}_s{1}_s=1_s\vee \left(y{+}_s{1}_s\right){-}_s{1}_s\in {\mathbb{N}}_s\right)\right)$$
27	4 8 12 16 18 26	nnsind	$$⊢A\in {\mathbb{N}}_s\to \left(A=1_s\vee A{-}_s{1}_s\in {\mathbb{N}}_s\right)$$