Metamath Proof Explorer

Theorem 1reno

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

Ref Expression
Assertion 1reno 
|- 1s e. RR_s

Proof

Step Hyp Ref Expression
1 1sno 
 |-  1s e. No
2 2nns 
 |-  2s e. NN_s
3 2sno 
 |-  2s e. No
4 3 a1i 
 |-  ( T. -> 2s e. No )
5 4 negscld 
 |-  ( T. -> ( -us ` 2s ) e. No )
6 0sno 
 |-  0s e. No
7 6 a1i 
 |-  ( T. -> 0s e. No )
8 1 a1i 
 |-  ( T. -> 1s e. No )
9 nnsgt0 
 |-  ( 2s e. NN_s -> 0s
10 2 9 ax-mp 
 |-  0s
11 4 slt0neg2d 
 |-  ( T. -> ( 0s  ( -us ` 2s )
12 10 11 mpbii 
 |-  ( T. -> ( -us ` 2s )
13 0slt1s 
 |-  0s
14 13 a1i 
 |-  ( T. -> 0s
15 5 7 8 12 14 slttrd 
 |-  ( T. -> ( -us ` 2s )
16 15 mptru 
 |-  ( -us ` 2s )
17 8 sltp1d 
 |-  ( T. -> 1s
18 17 mptru 
 |-  1s
19 1p1e2s 
 |-  ( 1s +s 1s ) = 2s
20 18 19 breqtri 
 |-  1s
21 16 20 pm3.2i 
 |-  ( ( -us ` 2s )
22 fveq2 
 |-  ( n = 2s -> ( -us ` n ) = ( -us ` 2s ) )
23 22 breq1d 
 |-  ( n = 2s -> ( ( -us ` n )  ( -us ` 2s )
24 breq2 
 |-  ( n = 2s -> ( 1s  1s
25 23 24 anbi12d 
 |-  ( n = 2s -> ( ( ( -us ` n )  ( ( -us ` 2s )
26 25 rspcev 
 |-  ( ( 2s e. NN_s /\ ( ( -us ` 2s )  E. n e. NN_s ( ( -us ` n )
27 2 21 26 mp2an 
 |-  E. n e. NN_s ( ( -us ` n )
28 1nns 
 |-  1s e. NN_s
29 slerflex 
 |-  ( 1s e. No -> 1s <_s 1s )
30 1 29 ax-mp 
 |-  1s <_s 1s
31 oveq2 
 |-  ( n = 1s -> ( 1s /su n ) = ( 1s /su 1s ) )
32 divs1 
 |-  ( 1s e. No -> ( 1s /su 1s ) = 1s )
33 1 32 ax-mp 
 |-  ( 1s /su 1s ) = 1s
34 31 33 eqtrdi 
 |-  ( n = 1s -> ( 1s /su n ) = 1s )
35 34 breq1d 
 |-  ( n = 1s -> ( ( 1s /su n ) <_s 1s <-> 1s <_s 1s ) )
36 35 rspcev 
 |-  ( ( 1s e. NN_s /\ 1s <_s 1s ) -> E. n e. NN_s ( 1s /su n ) <_s 1s )
37 28 30 36 mp2an 
 |-  E. n e. NN_s ( 1s /su n ) <_s 1s
38 left1s 
 |-  ( _Left ` 1s ) = { 0s }
39 right1s 
 |-  ( _Right ` 1s ) = (/)
40 38 39 uneq12i 
 |-  ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) = ( { 0s } u. (/) )
41 un0 
 |-  ( { 0s } u. (/) ) = { 0s }
42 40 41 eqtri 
 |-  ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) = { 0s }
43 42 raleqi 
 |-  ( 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 ) ) )
44 6 elexi 
 |-  0s e. _V
45 oveq2 
 |-  ( xO = 0s -> ( 1s -s xO ) = ( 1s -s 0s ) )
46 subsid1 
 |-  ( 1s e. No -> ( 1s -s 0s ) = 1s )
47 1 46 ax-mp 
 |-  ( 1s -s 0s ) = 1s
48 45 47 eqtrdi 
 |-  ( xO = 0s -> ( 1s -s xO ) = 1s )
49 48 fveq2d 
 |-  ( xO = 0s -> ( abs_s ` ( 1s -s xO ) ) = ( abs_s ` 1s ) )
50 7 8 14 sltled 
 |-  ( T. -> 0s <_s 1s )
51 50 mptru 
 |-  0s <_s 1s
52 abssid 
 |-  ( ( 1s e. No /\ 0s <_s 1s ) -> ( abs_s ` 1s ) = 1s )
53 1 51 52 mp2an 
 |-  ( abs_s ` 1s ) = 1s
54 49 53 eqtrdi 
 |-  ( xO = 0s -> ( abs_s ` ( 1s -s xO ) ) = 1s )
55 54 breq2d 
 |-  ( xO = 0s -> ( ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) ) <-> ( 1s /su n ) <_s 1s ) )
56 55 rexbidv 
 |-  ( 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 ) )
57 44 56 ralsn 
 |-  ( 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 )
58 43 57 bitri 
 |-  ( 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 )
59 37 58 mpbir 
 |-  A. xO e. ( ( _Left ` 1s ) u. ( _Right ` 1s ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( 1s -s xO ) )
60 27 59 pm3.2i 
 |-  ( E. n e. NN_s ( ( -us ` n )
61 elreno2 
 |-  ( 1s e. RR_s <-> ( 1s e. No /\ ( E. n e. NN_s ( ( -us ` n )
62 1 60 61 mpbir2an 
 |-  1s e. RR_s