Theorem 1reno

Description: Surreal one is a surreal real. (Contributed by Scott Fenton, 18-Feb-2026)

	Ref	Expression
Assertion	1reno	⊢ 1s ∈ ℝs

Proof

Step	Hyp	Ref	Expression
1		1sno	⊢ 1s ∈ No
2		2nns	⊢ 2s ∈ ℕs
3		2sno	⊢ 2s ∈ No
4	3	a1i	⊢ ( ⊤ → 2s ∈ No )
5	4	negscld	⊢ ( ⊤ → ( -us ‘ 2s ) ∈ No )
6		0sno	⊢ 0s ∈ No
7	6	a1i	⊢ ( ⊤ → 0s ∈ No )
8	1	a1i	⊢ ( ⊤ → 1s ∈ No )
9		nnsgt0	⊢ ( 2s ∈ ℕs → 0s <s 2s )
10	2 9	ax-mp	⊢ 0s <s 2s
11	4	slt0neg2d	⊢ ( ⊤ → ( 0s <s 2s ↔ ( -us ‘ 2s ) <s 0s ) )
12	10 11	mpbii	⊢ ( ⊤ → ( -us ‘ 2s ) <s 0s )
13		0slt1s	⊢ 0s <s 1s
14	13	a1i	⊢ ( ⊤ → 0s <s 1s )
15	5 7 8 12 14	slttrd	⊢ ( ⊤ → ( -us ‘ 2s ) <s 1s )
16	15	mptru	⊢ ( -us ‘ 2s ) <s 1s
17	8	sltp1d	⊢ ( ⊤ → 1s <s ( 1s +s 1s ) )
18	17	mptru	⊢ 1s <s ( 1s +s 1s )
19		1p1e2s	⊢ ( 1s +s 1s ) = 2s
20	18 19	breqtri	⊢ 1s <s 2s
21	16 20	pm3.2i	⊢ ( ( -us ‘ 2s ) <s 1s ∧ 1s <s 2s )
22		fveq2	⊢ ( 𝑛 = 2s → ( -us ‘ 𝑛 ) = ( -us ‘ 2s ) )
23	22	breq1d	⊢ ( 𝑛 = 2s → ( ( -us ‘ 𝑛 ) <s 1s ↔ ( -us ‘ 2s ) <s 1s ) )
24		breq2	⊢ ( 𝑛 = 2s → ( 1s <s 𝑛 ↔ 1s <s 2s ) )
25	23 24	anbi12d	⊢ ( 𝑛 = 2s → ( ( ( -us ‘ 𝑛 ) <s 1s ∧ 1s <s 𝑛 ) ↔ ( ( -us ‘ 2s ) <s 1s ∧ 1s <s 2s ) ) )
26	25	rspcev	⊢ ( ( 2s ∈ ℕs ∧ ( ( -us ‘ 2s ) <s 1s ∧ 1s <s 2s ) ) → ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 1s ∧ 1s <s 𝑛 ) )
27	2 21 26	mp2an	⊢ ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 1s ∧ 1s <s 𝑛 )
28		1nns	⊢ 1s ∈ ℕs
29		slerflex	⊢ ( 1s ∈ No → 1s ≤s 1s )
30	1 29	ax-mp	⊢ 1s ≤s 1s
31		oveq2	⊢ ( 𝑛 = 1s → ( 1s /su 𝑛 ) = ( 1s /su 1s ) )
32		divs1	⊢ ( 1s ∈ No → ( 1s /su 1s ) = 1s )
33	1 32	ax-mp	⊢ ( 1s /su 1s ) = 1s
34	31 33	eqtrdi	⊢ ( 𝑛 = 1s → ( 1s /su 𝑛 ) = 1s )
35	34	breq1d	⊢ ( 𝑛 = 1s → ( ( 1s /su 𝑛 ) ≤s 1s ↔ 1s ≤s 1s ) )
36	35	rspcev	⊢ ( ( 1s ∈ ℕs ∧ 1s ≤s 1s ) → ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s 1s )
37	28 30 36	mp2an	⊢ ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s 1s
38		left1s	⊢ ( L ‘ 1s ) = { 0s }
39		right1s	⊢ ( R ‘ 1s ) = ∅
40	38 39	uneq12i	⊢ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) = ( { 0s } ∪ ∅ )
41		un0	⊢ ( { 0s } ∪ ∅ ) = { 0s }
42	40 41	eqtri	⊢ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) = { 0s }
43	42	raleqi	⊢ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) ↔ ∀ 𝑥𝑂 ∈ { 0s } ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) )
44	6	elexi	⊢ 0s ∈ V
45		oveq2	⊢ ( 𝑥𝑂 = 0s → ( 1s -s 𝑥𝑂 ) = ( 1s -s 0s ) )
46		subsid1	⊢ ( 1s ∈ No → ( 1s -s 0s ) = 1s )
47	1 46	ax-mp	⊢ ( 1s -s 0s ) = 1s
48	45 47	eqtrdi	⊢ ( 𝑥𝑂 = 0s → ( 1s -s 𝑥𝑂 ) = 1s )
49	48	fveq2d	⊢ ( 𝑥𝑂 = 0s → ( abss ‘ ( 1s -s 𝑥𝑂 ) ) = ( abss ‘ 1s ) )
50	7 8 14	sltled	⊢ ( ⊤ → 0s ≤s 1s )
51	50	mptru	⊢ 0s ≤s 1s
52		abssid	⊢ ( ( 1s ∈ No ∧ 0s ≤s 1s ) → ( abss ‘ 1s ) = 1s )
53	1 51 52	mp2an	⊢ ( abss ‘ 1s ) = 1s
54	49 53	eqtrdi	⊢ ( 𝑥𝑂 = 0s → ( abss ‘ ( 1s -s 𝑥𝑂 ) ) = 1s )
55	54	breq2d	⊢ ( 𝑥𝑂 = 0s → ( ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) ↔ ( 1s /su 𝑛 ) ≤s 1s ) )
56	55	rexbidv	⊢ ( 𝑥𝑂 = 0s → ( ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) ↔ ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s 1s ) )
57	44 56	ralsn	⊢ ( ∀ 𝑥𝑂 ∈ { 0s } ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) ↔ ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s 1s )
58	43 57	bitri	⊢ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) ↔ ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s 1s )
59	37 58	mpbir	⊢ ∀ 𝑥𝑂 ∈ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) )
60	27 59	pm3.2i	⊢ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 1s ∧ 1s <s 𝑛 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) )
61		elreno2	⊢ ( 1s ∈ ℝs ↔ ( 1s ∈ No ∧ ( ∃ 𝑛 ∈ ℕs ( ( -us ‘ 𝑛 ) <s 1s ∧ 1s <s 𝑛 ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 1s ) ∪ ( R ‘ 1s ) ) ∃ 𝑛 ∈ ℕs ( 1s /su 𝑛 ) ≤s ( abss ‘ ( 1s -s 𝑥𝑂 ) ) ) ) )
62	1 60 61	mpbir2an	⊢ 1s ∈ ℝs