Theorem 1reno

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

	Ref	Expression
Assertion	1reno	$$⊢1_s\in {ℝ}_s$$

Proof

Step	Hyp	Ref	Expression
1		1no	$$⊢1_s\in \mathrm{No}$$
2		2nns	Could not format 2s e. NN_s : No typesetting found for |- 2s e. NN_s with typecode |-
3		2no	Could not format 2s e. No : No typesetting found for |- 2s e. No with typecode |-
4	3	a1i	Could not format ( T. -> 2s e. No ) : No typesetting found for |- ( T. -> 2s e. No ) with typecode |-
5	4	negscld	Could not format ( T. -> ( -us ` 2s ) e. No ) : No typesetting found for |- ( T. -> ( -us ` 2s ) e. No ) with typecode |-
6		0no	$$⊢0_s\in \mathrm{No}$$
7	6	a1i	$$⊢\top \to 0_s\in \mathrm{No}$$
8	1	a1i	$$⊢\top \to 1_s\in \mathrm{No}$$
9		nnsgt0	Could not format ( 2s e. NN_s -> 0s 0s
10	2 9	ax-mp	Could not format 0s
11	4	lt0negs2d	Could not format ( T. -> ( 0s ( -us ` 2s ) ( 0s ( -us ` 2s )
12	10 11	mpbii	Could not format ( T. -> ( -us ` 2s ) ( -us ` 2s )
13		0lt1s	$$⊢0_s{<}_s{1}_s$$
14	13	a1i	$$⊢\top \to 0_s{<}_s{1}_s$$
15	5 7 8 12 14	ltstrd	Could not format ( T. -> ( -us ` 2s ) ( -us ` 2s )
16	15	mptru	Could not format ( -us ` 2s )
17	8	ltsp1d	$$⊢\top \to 1_s{<}_s\left(1_s{+}_s{1}_s\right)$$
18	17	mptru	$$⊢1_s{<}_s\left(1_s{+}_s{1}_s\right)$$
19		1p1e2s	Could not format ( 1s +s 1s ) = 2s : No typesetting found for |- ( 1s +s 1s ) = 2s with typecode |-
20	18 19	breqtri	Could not format 1s
21	16 20	pm3.2i	Could not format ( ( -us ` 2s )
22		fveq2	Could not format ( n = 2s -> ( -us ` n ) = ( -us ` 2s ) ) : No typesetting found for |- ( n = 2s -> ( -us ` n ) = ( -us ` 2s ) ) with typecode |-
23	22	breq1d	Could not format ( n = 2s -> ( ( -us ` n ) ( -us ` 2s ) ( ( -us ` n ) ( -us ` 2s )
24		breq2	Could not format ( n = 2s -> ( 1s 1s ( 1s 1s
25	23 24	anbi12d	Could not format ( n = 2s -> ( ( ( -us ` n ) ( ( -us ` 2s ) ( ( ( -us ` n ) ( ( -us ` 2s )
26	25	rspcev	Could not format ( ( 2s e. NN_s /\ ( ( -us ` 2s ) E. n e. NN_s ( ( -us ` n ) E. n e. NN_s ( ( -us ` n )
27	2 21 26	mp2an	$$⊢\exists n\in {\mathbb{N}}_s\left({+}_s\left(n\right){<}_s{1}_s\wedge 1_s{<}_{s}n\right)$$
28		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
29		lesid	$$⊢1_s\in \mathrm{No}\to 1_s{\le }_s{1}_s$$
30	1 29	ax-mp	$$⊢1_s{\le }_s{1}_s$$
31		oveq2	$$⊢n=1_s\to 1_s{/}_{\mathrm{su}}n=1_s{/}_{\mathrm{su}}{1}_s$$
32		divs1	$$⊢1_s\in \mathrm{No}\to 1_s{/}_{\mathrm{su}}{1}_s=1_s$$
33	1 32	ax-mp	$$⊢1_s{/}_{\mathrm{su}}{1}_s=1_s$$
34	31 33	eqtrdi	$$⊢n=1_s\to 1_s{/}_{\mathrm{su}}n=1_s$$
35	34	breq1d	$$⊢n=1_s\to \left(\left(1_s{/}_{\mathrm{su}}n\right){\le }_s{1}_s\leftrightarrow 1_s{\le }_s{1}_s\right)$$
36	35	rspcev	$$⊢\left(1_s\in {\mathbb{N}}_s\wedge 1_s{\le }_s{1}_s\right)\to \exists n\in {\mathbb{N}}_s\left(1_s{/}_{\mathrm{su}}n\right){\le }_s{1}_s$$
37	28 30 36	mp2an	$$⊢\exists n\in {\mathbb{N}}_s\left(1_s{/}_{\mathrm{su}}n\right){\le }_s{1}_s$$
38		left1s	$$⊢L\left(1_s\right)=\left\{0_s\right\}$$
39		right1s	$$⊢R\left(1_s\right)=\varnothing$$
40	38 39	uneq12i	$$⊢L\left(1_s\right)\cup R\left(1_s\right)=\left\{0_s\right\}\cup \varnothing$$
41		un0	$$⊢\left\{0_s\right\}\cup \varnothing =\left\{0_s\right\}$$
42	40 41	eqtri	$$⊢L\left(1_s\right)\cup R\left(1_s\right)=\left\{0_s\right\}$$
43	42	raleqi	Could not format ( A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> A. xO e. { 0s } E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) ) : No typesetting found for |- ( A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> A. xO e. { 0s } E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) ) with typecode |-
44	6	elexi	$$⊢0_s\in \mathrm{V}$$
45		oveq2	Could not format ( xO = 0s -> ( 1s -s xO ) = ( 1s -s 0s ) ) : No typesetting found for |- ( xO = 0s -> ( 1s -s xO ) = ( 1s -s 0s ) ) with typecode |-
46		subsid1	$$⊢1_s\in \mathrm{No}\to 1_s{-}_s{0}_s=1_s$$
47	1 46	ax-mp	$$⊢1_s{-}_s{0}_s=1_s$$
48	45 47	eqtrdi	Could not format ( xO = 0s -> ( 1s -s xO ) = 1s ) : No typesetting found for |- ( xO = 0s -> ( 1s -s xO ) = 1s ) with typecode |-
49	48	fveq2d	Could not format ( xO = 0s -> ( abs_s ` ( 1s -s xO ) ) = ( abs_s ` 1s ) ) : No typesetting found for |- ( xO = 0s -> ( abs_s ` ( 1s -s xO ) ) = ( abs_s ` 1s ) ) with typecode |-
50	7 8 14	ltlesd	$$⊢\top \to 0_s{\le }_s{1}_s$$
51	50	mptru	$$⊢0_s{\le }_s{1}_s$$
52		abssid	$$⊢\left(1_s\in \mathrm{No}\wedge 0_s{\le }_s{1}_s\right)\to {abs}_s\left(1_s\right)=1_s$$
53	1 51 52	mp2an	$$⊢{abs}_s\left(1_s\right)=1_s$$
54	49 53	eqtrdi	Could not format ( xO = 0s -> ( abs_s ` ( 1s -s xO ) ) = 1s ) : No typesetting found for |- ( xO = 0s -> ( abs_s ` ( 1s -s xO ) ) = 1s ) with typecode |-
55	54	breq2d	Could not format ( xO = 0s -> ( ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> ( 1s /su n ) <_s 1s ) ) : No typesetting found for |- ( xO = 0s -> ( ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> ( 1s /su n ) <_s 1s ) ) with typecode |-
56	55	rexbidv	Could not format ( xO = 0s -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> E. n e. NN_s ( 1s /su n ) <_s 1s ) ) : No typesetting found for |- ( xO = 0s -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> E. n e. NN_s ( 1s /su n ) <_s 1s ) ) with typecode |-
57	44 56	ralsn	Could not format ( A. xO e. { 0s } E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> E. n e. NN_s ( 1s /su n ) <_s 1s ) : No typesetting found for |- ( A. xO e. { 0s } E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> E. n e. NN_s ( 1s /su n ) <_s 1s ) with typecode |-
58	43 57	bitri	Could not format ( A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> E. n e. NN_s ( 1s /su n ) <_s 1s ) : No typesetting found for |- ( A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> E. n e. NN_s ( 1s /su n ) <_s 1s ) with typecode |-
59	37 58	mpbir	Could not format A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) : No typesetting found for |- A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) with typecode |-
60	27 59	pm3.2i	Could not format ( E. n e. NN_s ( ( -us ` n )
61		elreno2	Could not format ( 1s e. RR_s <-> ( 1s e. No /\ ( E. n e. NN_s ( ( -us ` n ) ( 1s e. No /\ ( E. n e. NN_s ( ( -us ` n )
62	1 60 61	mpbir2an	$$⊢1_s\in {ℝ}_s$$