Metamath Proof Explorer

Theorem renegscl

Description: The surreal reals are closed under negation. Part of theorem 13(ii) of Conway p. 24. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion renegscl 
|- ( A e. RR_s -> ( -us ` A ) e. RR_s )

Proof

Step Hyp Ref Expression
1 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
2 1 adantr 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( -us ` A ) e. No )
3 nnsno 
 |-  ( n e. NN_s -> n e. No )
4 3 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> n e. No )
5 4 negscld 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` n ) e. No )
6 simpl 
 |-  ( ( A e. No /\ n e. NN_s ) -> A e. No )
7 5 6 sltnegd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` n )  ( -us ` A )
8 negnegs 
 |-  ( n e. No -> ( -us ` ( -us ` n ) ) = n )
9 4 8 syl 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( -us ` n ) ) = n )
10 9 breq2d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` A )  ( -us ` A )
11 7 10 bitrd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` n )  ( -us ` A )
12 6 4 sltnegd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A  ( -us ` n )
13 11 12 anbi12d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( ( -us ` n )  ( ( -us ` A )
14 13 biancomd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( ( -us ` n )  ( ( -us ` n )
15 14 rexbidva 
 |-  ( A e. No -> ( E. n e. NN_s ( ( -us ` n )  E. n e. NN_s ( ( -us ` n )
16 15 biimpa 
 |-  ( ( A e. No /\ E. n e. NN_s ( ( -us ` n )  E. n e. NN_s ( ( -us ` n )
17 16 adantrr 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  E. n e. NN_s ( ( -us ` n )
18 recut 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
19 18 adantr 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } <
20 simprr 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  A = ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } |s { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) )
21 19 20 negsunif 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( -us ` A ) = ( ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) |s ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) ) )
22 negsfn 
 |-  -us Fn No
23 ssltss2 
 |-  ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } < { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } C_ No )
24 18 23 syl 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } C_ No )
25 fvelimab 
 |-  ( ( -us Fn No /\ { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } C_ No ) -> ( y e. ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) <-> E. z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ( -us ` z ) = y ) )
26 22 24 25 sylancr 
 |-  ( A e. No -> ( y e. ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) <-> E. z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ( -us ` z ) = y ) )
27 eqeq1 
 |-  ( x = z -> ( x = ( A +s ( 1s /su n ) ) <-> z = ( A +s ( 1s /su n ) ) ) )
28 27 rexbidv 
 |-  ( x = z -> ( E. n e. NN_s x = ( A +s ( 1s /su n ) ) <-> E. n e. NN_s z = ( A +s ( 1s /su n ) ) ) )
29 28 rexab 
 |-  ( E. z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ( -us ` z ) = y <-> E. z ( E. n e. NN_s z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
30 rexcom4 
 |-  ( E. n e. NN_s E. z ( z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. z E. n e. NN_s ( z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
31 ovex 
 |-  ( A +s ( 1s /su n ) ) e. _V
32 fveqeq2 
 |-  ( z = ( A +s ( 1s /su n ) ) -> ( ( -us ` z ) = y <-> ( -us ` ( A +s ( 1s /su n ) ) ) = y ) )
33 31 32 ceqsexv 
 |-  ( E. z ( z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> ( -us ` ( A +s ( 1s /su n ) ) ) = y )
34 33 rexbii 
 |-  ( E. n e. NN_s E. z ( z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. n e. NN_s ( -us ` ( A +s ( 1s /su n ) ) ) = y )
35 r19.41v 
 |-  ( E. n e. NN_s ( z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> ( E. n e. NN_s z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
36 35 exbii 
 |-  ( E. z E. n e. NN_s ( z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. z ( E. n e. NN_s z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
37 30 34 36 3bitr3ri 
 |-  ( E. z ( E. n e. NN_s z = ( A +s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. n e. NN_s ( -us ` ( A +s ( 1s /su n ) ) ) = y )
38 29 37 bitri 
 |-  ( E. z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ( -us ` z ) = y <-> E. n e. NN_s ( -us ` ( A +s ( 1s /su n ) ) ) = y )
39 1sno 
 |-  1s e. No
40 39 a1i 
 |-  ( n e. NN_s -> 1s e. No )
41 nnne0s 
 |-  ( n e. NN_s -> n =/= 0s )
42 40 3 41 divscld 
 |-  ( n e. NN_s -> ( 1s /su n ) e. No )
43 42 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 1s /su n ) e. No )
44 negsdi 
 |-  ( ( A e. No /\ ( 1s /su n ) e. No ) -> ( -us ` ( A +s ( 1s /su n ) ) ) = ( ( -us ` A ) +s ( -us ` ( 1s /su n ) ) ) )
45 43 44 syldan 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( A +s ( 1s /su n ) ) ) = ( ( -us ` A ) +s ( -us ` ( 1s /su n ) ) ) )
46 1 adantr 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` A ) e. No )
47 46 43 subsvald 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` A ) -s ( 1s /su n ) ) = ( ( -us ` A ) +s ( -us ` ( 1s /su n ) ) ) )
48 45 47 eqtr4d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( A +s ( 1s /su n ) ) ) = ( ( -us ` A ) -s ( 1s /su n ) ) )
49 48 eqeq1d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` ( A +s ( 1s /su n ) ) ) = y <-> ( ( -us ` A ) -s ( 1s /su n ) ) = y ) )
50 eqcom 
 |-  ( ( ( -us ` A ) -s ( 1s /su n ) ) = y <-> y = ( ( -us ` A ) -s ( 1s /su n ) ) )
51 49 50 bitrdi 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` ( A +s ( 1s /su n ) ) ) = y <-> y = ( ( -us ` A ) -s ( 1s /su n ) ) ) )
52 51 rexbidva 
 |-  ( A e. No -> ( E. n e. NN_s ( -us ` ( A +s ( 1s /su n ) ) ) = y <-> E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) ) )
53 38 52 bitrid 
 |-  ( A e. No -> ( E. z e. { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ( -us ` z ) = y <-> E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) ) )
54 26 53 bitrd 
 |-  ( A e. No -> ( y e. ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) <-> E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) ) )
55 54 eqabdv 
 |-  ( A e. No -> ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) = { y | E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) } )
56 ssltss1 
 |-  ( { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } < { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } C_ No )
57 18 56 syl 
 |-  ( A e. No -> { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } C_ No )
58 fvelimab 
 |-  ( ( -us Fn No /\ { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } C_ No ) -> ( y e. ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) <-> E. z e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ( -us ` z ) = y ) )
59 22 57 58 sylancr 
 |-  ( A e. No -> ( y e. ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) <-> E. z e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ( -us ` z ) = y ) )
60 eqeq1 
 |-  ( x = z -> ( x = ( A -s ( 1s /su n ) ) <-> z = ( A -s ( 1s /su n ) ) ) )
61 60 rexbidv 
 |-  ( x = z -> ( E. n e. NN_s x = ( A -s ( 1s /su n ) ) <-> E. n e. NN_s z = ( A -s ( 1s /su n ) ) ) )
62 61 rexab 
 |-  ( E. z e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ( -us ` z ) = y <-> E. z ( E. n e. NN_s z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
63 rexcom4 
 |-  ( E. n e. NN_s E. z ( z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. z E. n e. NN_s ( z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
64 ovex 
 |-  ( A -s ( 1s /su n ) ) e. _V
65 fveqeq2 
 |-  ( z = ( A -s ( 1s /su n ) ) -> ( ( -us ` z ) = y <-> ( -us ` ( A -s ( 1s /su n ) ) ) = y ) )
66 64 65 ceqsexv 
 |-  ( E. z ( z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> ( -us ` ( A -s ( 1s /su n ) ) ) = y )
67 66 rexbii 
 |-  ( E. n e. NN_s E. z ( z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. n e. NN_s ( -us ` ( A -s ( 1s /su n ) ) ) = y )
68 r19.41v 
 |-  ( E. n e. NN_s ( z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> ( E. n e. NN_s z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
69 68 exbii 
 |-  ( E. z E. n e. NN_s ( z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. z ( E. n e. NN_s z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) )
70 63 67 69 3bitr3ri 
 |-  ( E. z ( E. n e. NN_s z = ( A -s ( 1s /su n ) ) /\ ( -us ` z ) = y ) <-> E. n e. NN_s ( -us ` ( A -s ( 1s /su n ) ) ) = y )
71 62 70 bitri 
 |-  ( E. z e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ( -us ` z ) = y <-> E. n e. NN_s ( -us ` ( A -s ( 1s /su n ) ) ) = y )
72 6 43 subsvald 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) = ( A +s ( -us ` ( 1s /su n ) ) ) )
73 72 fveq2d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( A -s ( 1s /su n ) ) ) = ( -us ` ( A +s ( -us ` ( 1s /su n ) ) ) ) )
74 43 negscld 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( 1s /su n ) ) e. No )
75 negsdi 
 |-  ( ( A e. No /\ ( -us ` ( 1s /su n ) ) e. No ) -> ( -us ` ( A +s ( -us ` ( 1s /su n ) ) ) ) = ( ( -us ` A ) +s ( -us ` ( -us ` ( 1s /su n ) ) ) ) )
76 74 75 syldan 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( A +s ( -us ` ( 1s /su n ) ) ) ) = ( ( -us ` A ) +s ( -us ` ( -us ` ( 1s /su n ) ) ) ) )
77 negnegs 
 |-  ( ( 1s /su n ) e. No -> ( -us ` ( -us ` ( 1s /su n ) ) ) = ( 1s /su n ) )
78 43 77 syl 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( -us ` ( 1s /su n ) ) ) = ( 1s /su n ) )
79 78 oveq2d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` A ) +s ( -us ` ( -us ` ( 1s /su n ) ) ) ) = ( ( -us ` A ) +s ( 1s /su n ) ) )
80 73 76 79 3eqtrd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( -us ` ( A -s ( 1s /su n ) ) ) = ( ( -us ` A ) +s ( 1s /su n ) ) )
81 80 eqeq1d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` ( A -s ( 1s /su n ) ) ) = y <-> ( ( -us ` A ) +s ( 1s /su n ) ) = y ) )
82 eqcom 
 |-  ( ( ( -us ` A ) +s ( 1s /su n ) ) = y <-> y = ( ( -us ` A ) +s ( 1s /su n ) ) )
83 81 82 bitrdi 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( -us ` ( A -s ( 1s /su n ) ) ) = y <-> y = ( ( -us ` A ) +s ( 1s /su n ) ) ) )
84 83 rexbidva 
 |-  ( A e. No -> ( E. n e. NN_s ( -us ` ( A -s ( 1s /su n ) ) ) = y <-> E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) ) )
85 71 84 bitrid 
 |-  ( A e. No -> ( E. z e. { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ( -us ` z ) = y <-> E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) ) )
86 59 85 bitrd 
 |-  ( A e. No -> ( y e. ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) <-> E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) ) )
87 86 eqabdv 
 |-  ( A e. No -> ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) = { y | E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) } )
88 55 87 oveq12d 
 |-  ( A e. No -> ( ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) |s ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) ) = ( { y | E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) } |s { y | E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) } ) )
89 88 adantr 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( ( -us " { x | E. n e. NN_s x = ( A +s ( 1s /su n ) ) } ) |s ( -us " { x | E. n e. NN_s x = ( A -s ( 1s /su n ) ) } ) ) = ( { y | E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) } |s { y | E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) } ) )
90 21 89 eqtrd 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( -us ` A ) = ( { y | E. n e. NN_s y = ( ( -us ` A ) -s ( 1s /su n ) ) } |s { y | E. n e. NN_s y = ( ( -us ` A ) +s ( 1s /su n ) ) } ) )
91 2 17 90 jca32 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( ( -us ` A ) e. No /\ ( E. n e. NN_s ( ( -us ` n )
92 elreno 
 |-  ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
93 elreno 
 |-  ( ( -us ` A ) e. RR_s <-> ( ( -us ` A ) e. No /\ ( E. n e. NN_s ( ( -us ` n )
94 91 92 93 3imtr4i 
 |-  ( A e. RR_s -> ( -us ` A ) e. RR_s )