Metamath Proof Explorer

Theorem 0reno

Description: Surreal zero is a surreal real. (Contributed by Scott Fenton, 15-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 1nns 
 |-  1s e. NN_s
3 0slt1s 
 |-  0s
4 1sno 
 |-  1s e. No
5 sltneg 
 |-  ( ( 0s e. No /\ 1s e. No ) -> ( 0s  ( -us ` 1s )
6 1 4 5 mp2an 
 |-  ( 0s  ( -us ` 1s )
7 3 6 mpbi 
 |-  ( -us ` 1s )
8 negs0s 
 |-  ( -us ` 0s ) = 0s
9 7 8 breqtri 
 |-  ( -us ` 1s )
10 9 3 pm3.2i 
 |-  ( ( -us ` 1s )
11 fveq2 
 |-  ( n = 1s -> ( -us ` n ) = ( -us ` 1s ) )
12 11 breq1d 
 |-  ( n = 1s -> ( ( -us ` n )  ( -us ` 1s )
13 breq2 
 |-  ( n = 1s -> ( 0s  0s
14 12 13 anbi12d 
 |-  ( n = 1s -> ( ( ( -us ` n )  ( ( -us ` 1s )
15 14 rspcev 
 |-  ( ( 1s e. NN_s /\ ( ( -us ` 1s )  E. n e. NN_s ( ( -us ` n )
16 2 10 15 mp2an 
 |-  E. n e. NN_s ( ( -us ` n )
17 4 a1i 
 |-  ( n e. NN_s -> 1s e. No )
18 nnsno 
 |-  ( n e. NN_s -> n e. No )
19 nnne0s 
 |-  ( n e. NN_s -> n =/= 0s )
20 17 18 19 divscld 
 |-  ( n e. NN_s -> ( 1s /su n ) e. No )
21 20 negsval2d 
 |-  ( n e. NN_s -> ( -us ` ( 1s /su n ) ) = ( 0s -s ( 1s /su n ) ) )
22 21 eqeq2d 
 |-  ( n e. NN_s -> ( x = ( -us ` ( 1s /su n ) ) <-> x = ( 0s -s ( 1s /su n ) ) ) )
23 22 bicomd 
 |-  ( n e. NN_s -> ( x = ( 0s -s ( 1s /su n ) ) <-> x = ( -us ` ( 1s /su n ) ) ) )
24 23 rexbiia 
 |-  ( E. n e. NN_s x = ( 0s -s ( 1s /su n ) ) <-> E. n e. NN_s x = ( -us ` ( 1s /su n ) ) )
25 24 abbii 
 |-  { x | E. n e. NN_s x = ( 0s -s ( 1s /su n ) ) } = { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) }
26 addslid 
 |-  ( ( 1s /su n ) e. No -> ( 0s +s ( 1s /su n ) ) = ( 1s /su n ) )
27 20 26 syl 
 |-  ( n e. NN_s -> ( 0s +s ( 1s /su n ) ) = ( 1s /su n ) )
28 27 eqeq2d 
 |-  ( n e. NN_s -> ( x = ( 0s +s ( 1s /su n ) ) <-> x = ( 1s /su n ) ) )
29 28 rexbiia 
 |-  ( E. n e. NN_s x = ( 0s +s ( 1s /su n ) ) <-> E. n e. NN_s x = ( 1s /su n ) )
30 29 abbii 
 |-  { x | E. n e. NN_s x = ( 0s +s ( 1s /su n ) ) } = { x | E. n e. NN_s x = ( 1s /su n ) }
31 25 30 oveq12i 
 |-  ( { x | E. n e. NN_s x = ( 0s -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( 0s +s ( 1s /su n ) ) } ) = ( { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( 1s /su n ) } )
32 nnsex 
 |-  NN_s e. _V
33 32 abrexex 
 |-  { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } e. _V
34 33 a1i 
 |-  ( T. -> { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } e. _V )
35 snex 
 |-  { 0s } e. _V
36 35 a1i 
 |-  ( T. -> { 0s } e. _V )
37 20 negscld 
 |-  ( n e. NN_s -> ( -us ` ( 1s /su n ) ) e. No )
38 eleq1 
 |-  ( x = ( -us ` ( 1s /su n ) ) -> ( x e. No <-> ( -us ` ( 1s /su n ) ) e. No ) )
39 37 38 syl5ibrcom 
 |-  ( n e. NN_s -> ( x = ( -us ` ( 1s /su n ) ) -> x e. No ) )
40 39 rexlimiv 
 |-  ( E. n e. NN_s x = ( -us ` ( 1s /su n ) ) -> x e. No )
41 40 a1i 
 |-  ( T. -> ( E. n e. NN_s x = ( -us ` ( 1s /su n ) ) -> x e. No ) )
42 41 abssdv 
 |-  ( T. -> { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } C_ No )
43 1 a1i 
 |-  ( T. -> 0s e. No )
44 43 snssd 
 |-  ( T. -> { 0s } C_ No )
45 vex 
 |-  z e. _V
46 eqeq1 
 |-  ( x = z -> ( x = ( -us ` ( 1s /su n ) ) <-> z = ( -us ` ( 1s /su n ) ) ) )
47 46 rexbidv 
 |-  ( x = z -> ( E. n e. NN_s x = ( -us ` ( 1s /su n ) ) <-> E. n e. NN_s z = ( -us ` ( 1s /su n ) ) ) )
48 45 47 elab 
 |-  ( z e. { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } <-> E. n e. NN_s z = ( -us ` ( 1s /su n ) ) )
49 velsn 
 |-  ( y e. { 0s } <-> y = 0s )
50 48 49 anbi12i 
 |-  ( ( z e. { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } /\ y e. { 0s } ) <-> ( E. n e. NN_s z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) )
51 r19.41v 
 |-  ( E. n e. NN_s ( z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) <-> ( E. n e. NN_s z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) )
52 50 51 bitr4i 
 |-  ( ( z e. { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } /\ y e. { 0s } ) <-> E. n e. NN_s ( z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) )
53 muls02 
 |-  ( n e. No -> ( 0s x.s n ) = 0s )
54 18 53 syl 
 |-  ( n e. NN_s -> ( 0s x.s n ) = 0s )
55 54 3 eqbrtrdi 
 |-  ( n e. NN_s -> ( 0s x.s n )
56 1 a1i 
 |-  ( n e. NN_s -> 0s e. No )
57 nnsgt0 
 |-  ( n e. NN_s -> 0s
58 56 17 18 57 sltmuldivd 
 |-  ( n e. NN_s -> ( ( 0s x.s n )  0s
59 55 58 mpbid 
 |-  ( n e. NN_s -> 0s
60 20 slt0neg2d 
 |-  ( n e. NN_s -> ( 0s  ( -us ` ( 1s /su n ) )
61 59 60 mpbid 
 |-  ( n e. NN_s -> ( -us ` ( 1s /su n ) )
62 breq12 
 |-  ( ( z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) -> ( z  ( -us ` ( 1s /su n ) )
63 61 62 syl5ibrcom 
 |-  ( n e. NN_s -> ( ( z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) -> z
64 63 rexlimiv 
 |-  ( E. n e. NN_s ( z = ( -us ` ( 1s /su n ) ) /\ y = 0s ) -> z
65 52 64 sylbi 
 |-  ( ( z e. { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } /\ y e. { 0s } ) -> z
66 65 3adant1 
 |-  ( ( T. /\ z e. { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } /\ y e. { 0s } ) -> z
67 34 36 42 44 66 ssltd 
 |-  ( T. -> { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } <
68 32 abrexex 
 |-  { x | E. n e. NN_s x = ( 1s /su n ) } e. _V
69 68 a1i 
 |-  ( T. -> { x | E. n e. NN_s x = ( 1s /su n ) } e. _V )
70 eleq1 
 |-  ( x = ( 1s /su n ) -> ( x e. No <-> ( 1s /su n ) e. No ) )
71 20 70 syl5ibrcom 
 |-  ( n e. NN_s -> ( x = ( 1s /su n ) -> x e. No ) )
72 71 rexlimiv 
 |-  ( E. n e. NN_s x = ( 1s /su n ) -> x e. No )
73 72 a1i 
 |-  ( T. -> ( E. n e. NN_s x = ( 1s /su n ) -> x e. No ) )
74 73 abssdv 
 |-  ( T. -> { x | E. n e. NN_s x = ( 1s /su n ) } C_ No )
75 eqeq1 
 |-  ( x = z -> ( x = ( 1s /su n ) <-> z = ( 1s /su n ) ) )
76 75 rexbidv 
 |-  ( x = z -> ( E. n e. NN_s x = ( 1s /su n ) <-> E. n e. NN_s z = ( 1s /su n ) ) )
77 45 76 elab 
 |-  ( z e. { x | E. n e. NN_s x = ( 1s /su n ) } <-> E. n e. NN_s z = ( 1s /su n ) )
78 49 77 anbi12i 
 |-  ( ( y e. { 0s } /\ z e. { x | E. n e. NN_s x = ( 1s /su n ) } ) <-> ( y = 0s /\ E. n e. NN_s z = ( 1s /su n ) ) )
79 r19.42v 
 |-  ( E. n e. NN_s ( y = 0s /\ z = ( 1s /su n ) ) <-> ( y = 0s /\ E. n e. NN_s z = ( 1s /su n ) ) )
80 78 79 bitr4i 
 |-  ( ( y e. { 0s } /\ z e. { x | E. n e. NN_s x = ( 1s /su n ) } ) <-> E. n e. NN_s ( y = 0s /\ z = ( 1s /su n ) ) )
81 breq12 
 |-  ( ( y = 0s /\ z = ( 1s /su n ) ) -> ( y  0s
82 59 81 syl5ibrcom 
 |-  ( n e. NN_s -> ( ( y = 0s /\ z = ( 1s /su n ) ) -> y
83 82 rexlimiv 
 |-  ( E. n e. NN_s ( y = 0s /\ z = ( 1s /su n ) ) -> y
84 83 a1i 
 |-  ( T. -> ( E. n e. NN_s ( y = 0s /\ z = ( 1s /su n ) ) -> y
85 80 84 biimtrid 
 |-  ( T. -> ( ( y e. { 0s } /\ z e. { x | E. n e. NN_s x = ( 1s /su n ) } ) -> y
86 85 3impib 
 |-  ( ( T. /\ y e. { 0s } /\ z e. { x | E. n e. NN_s x = ( 1s /su n ) } ) -> y
87 36 69 44 74 86 ssltd 
 |-  ( T. -> { 0s } <
88 67 87 cuteq0 
 |-  ( T. -> ( { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( 1s /su n ) } ) = 0s )
89 88 mptru 
 |-  ( { x | E. n e. NN_s x = ( -us ` ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( 1s /su n ) } ) = 0s
90 31 89 eqtr2i 
 |-  0s = ( { x | E. n e. NN_s x = ( 0s -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( 0s +s ( 1s /su n ) ) } )
91 16 90 pm3.2i 
 |-  ( E. n e. NN_s ( ( -us ` n )
92 elreno 
 |-  ( 0s e. RR_s <-> ( 0s e. No /\ ( E. n e. NN_s ( ( -us ` n )
93 1 91 92 mpbir2an 
 |-  0s e. RR_s