Metamath Proof Explorer

Theorem elreno2

Description: Alternate characterization of the surreal reals. Theorem 4.4(b) of Gonshor p. 39. (Contributed by Scott Fenton, 29-Jan-2026)

Ref Expression
Assertion elreno2 
|- ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )

Proof

Step Hyp Ref Expression
1 elreno 
 |-  ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
2 recut 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
3 2 adantr 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
4 simpr 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) )
5 3 4 cofcutr1d 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y )
6 eqeq1 
 |-  ( w = y -> ( w = ( A -s ( 1s /su n ) ) <-> y = ( A -s ( 1s /su n ) ) ) )
7 6 rexbidv 
 |-  ( w = y -> ( E. n e. NN_s w = ( A -s ( 1s /su n ) ) <-> E. n e. NN_s y = ( A -s ( 1s /su n ) ) ) )
8 7 rexab 
 |-  ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) )
9 rexcom4 
 |-  ( E. n e. NN_s E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. y E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) )
10 ovex 
 |-  ( A -s ( 1s /su n ) ) e. _V
11 breq2 
 |-  ( y = ( A -s ( 1s /su n ) ) -> ( xO <_s y <-> xO <_s ( A -s ( 1s /su n ) ) ) )
12 10 11 ceqsexv 
 |-  ( E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> xO <_s ( A -s ( 1s /su n ) ) )
13 12 rexbii 
 |-  ( E. n e. NN_s E. y ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) )
14 r19.41v 
 |-  ( E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) )
15 14 exbii 
 |-  ( E. y E. n e. NN_s ( y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) )
16 9 13 15 3bitr3ri 
 |-  ( E. y ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ xO <_s y ) <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) )
17 8 16 bitri 
 |-  ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) )
18 leftssno 
 |-  ( _Left ` A ) C_ No
19 18 sseli 
 |-  ( xO e. ( _Left ` A ) -> xO e. No )
20 19 adantl 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO e. No )
21 20 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> xO e. No )
22 simpll 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> A e. No )
23 1sno 
 |-  1s e. No
24 23 a1i 
 |-  ( n e. NN_s -> 1s e. No )
25 nnsno 
 |-  ( n e. NN_s -> n e. No )
26 nnne0s 
 |-  ( n e. NN_s -> n =/= 0s )
27 24 25 26 divscld 
 |-  ( n e. NN_s -> ( 1s /su n ) e. No )
28 27 adantl 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No )
29 22 28 subscld 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No )
30 21 29 28 sleadd1d 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO <_s ( A -s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) ) )
31 npcans 
 |-  ( ( A e. No /\ ( 1s /su n ) e. No ) -> ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) = A )
32 22 28 31 syl2anc 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) = A )
33 32 breq2d 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( xO +s ( 1s /su n ) ) <_s ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) )
34 30 33 bitrd 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO <_s ( A -s ( 1s /su n ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) )
35 34 rexbidva 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) )
36 35 adantlr 
 |-  ( ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) )
37 17 36 bitrid 
 |-  ( ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) /\ xO e. ( _Left ` A ) ) -> ( E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) )
38 37 ralbidva 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y <-> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) )
39 5 38 mpbid 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A )
40 3 4 cofcutr2d 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO )
41 eqeq1 
 |-  ( w = y -> ( w = ( A +s ( 1s /su n ) ) <-> y = ( A +s ( 1s /su n ) ) ) )
42 41 rexbidv 
 |-  ( w = y -> ( E. n e. NN_s w = ( A +s ( 1s /su n ) ) <-> E. n e. NN_s y = ( A +s ( 1s /su n ) ) ) )
43 42 rexab 
 |-  ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) )
44 rexcom4 
 |-  ( E. n e. NN_s E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. y E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) )
45 ovex 
 |-  ( A +s ( 1s /su n ) ) e. _V
46 breq1 
 |-  ( y = ( A +s ( 1s /su n ) ) -> ( y <_s xO <-> ( A +s ( 1s /su n ) ) <_s xO ) )
47 45 46 ceqsexv 
 |-  ( E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( A +s ( 1s /su n ) ) <_s xO )
48 47 rexbii 
 |-  ( E. n e. NN_s E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO )
49 r19.41v 
 |-  ( E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) )
50 49 exbii 
 |-  ( E. y E. n e. NN_s ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) )
51 44 48 50 3bitr3ri 
 |-  ( E. y ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO )
52 43 51 bitri 
 |-  ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO )
53 simpll 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> A e. No )
54 rightssno 
 |-  ( _Right ` A ) C_ No
55 54 sseli 
 |-  ( xO e. ( _Right ` A ) -> xO e. No )
56 55 adantl 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> xO e. No )
57 56 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> xO e. No )
58 27 adantl 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No )
59 57 58 subscld 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( xO -s ( 1s /su n ) ) e. No )
60 53 59 58 sleadd1d 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( A <_s ( xO -s ( 1s /su n ) ) <-> ( A +s ( 1s /su n ) ) <_s ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) ) )
61 npcans 
 |-  ( ( xO e. No /\ ( 1s /su n ) e. No ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO )
62 57 58 61 syl2anc 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO )
63 62 breq2d 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) <_s ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) <-> ( A +s ( 1s /su n ) ) <_s xO ) )
64 60 63 bitr2d 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( A +s ( 1s /su n ) ) <_s xO <-> A <_s ( xO -s ( 1s /su n ) ) ) )
65 64 rexbidva 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
66 52 65 bitrid 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
67 66 ralbidva 
 |-  ( A e. No -> ( A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
68 67 adantr 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
69 40 68 mpbid 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) )
70 39 69 jca 
 |-  ( ( A e. No /\ A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) ) -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
71 lrcut 
 |-  ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
72 71 adantr 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
73 lltropt 
 |-  ( _Left ` A ) <
74 73 a1i 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( _Left ` A ) <
75 35 biimpar 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> E. n e. NN_s xO <_s ( A -s ( 1s /su n ) ) )
76 75 17 sylibr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y )
77 76 ex 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A -> E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) )
78 77 ralimdva 
 |-  ( A e. No -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y ) )
79 78 imp 
 |-  ( ( A e. No /\ A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y )
80 79 adantrr 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A. xO e. ( _Left ` A ) E. y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } xO <_s y )
81 65 biimpar 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> E. n e. NN_s ( A +s ( 1s /su n ) ) <_s xO )
82 81 52 sylibr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO )
83 82 ex 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) -> E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) )
84 83 ralimdva 
 |-  ( A e. No -> ( A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO ) )
85 84 imp 
 |-  ( ( A e. No /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO )
86 85 adantrl 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A. xO e. ( _Right ` A ) E. y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } y <_s xO )
87 nnsex 
 |-  NN_s e. _V
88 87 abrexex 
 |-  { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } e. _V
89 88 a1i 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } e. _V )
90 snexg 
 |-  ( A e. No -> { A } e. _V )
91 simpl 
 |-  ( ( A e. No /\ n e. NN_s ) -> A e. No )
92 27 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 1s /su n ) e. No )
93 91 92 subscld 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No )
94 eleq1 
 |-  ( w = ( A -s ( 1s /su n ) ) -> ( w e. No <-> ( A -s ( 1s /su n ) ) e. No ) )
95 93 94 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( w = ( A -s ( 1s /su n ) ) -> w e. No ) )
96 95 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s w = ( A -s ( 1s /su n ) ) -> w e. No ) )
97 96 abssdv 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } C_ No )
98 snssi 
 |-  ( A e. No -> { A } C_ No )
99 biid 
 |-  ( A e. No <-> A e. No )
100 vex 
 |-  y e. _V
101 100 7 elab 
 |-  ( y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <-> E. n e. NN_s y = ( A -s ( 1s /su n ) ) )
102 velsn 
 |-  ( z e. { A } <-> z = A )
103 id 
 |-  ( n e. NN_s -> n e. NN_s )
104 103 nnsrecgt0d 
 |-  ( n e. NN_s -> 0s
105 104 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> 0s
106 92 91 sltsubposd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 0s  ( A -s ( 1s /su n ) )
107 105 106 mpbid 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) )
108 breq12 
 |-  ( ( y = ( A -s ( 1s /su n ) ) /\ z = A ) -> ( y  ( A -s ( 1s /su n ) )
109 107 108 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( y = ( A -s ( 1s /su n ) ) /\ z = A ) -> y
110 109 expd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( y = ( A -s ( 1s /su n ) ) -> ( z = A -> y
111 110 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) -> ( z = A -> y
112 111 3imp 
 |-  ( ( A e. No /\ E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ z = A ) -> y
113 99 101 102 112 syl3anb 
 |-  ( ( A e. No /\ y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } /\ z e. { A } ) -> y
114 89 90 97 98 113 ssltd 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
115 71 sneqd 
 |-  ( A e. No -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } = { A } )
116 114 115 breqtrrd 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
117 116 adantr 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
118 72 sneqd 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } = { A } )
119 87 abrexex 
 |-  { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } e. _V
120 119 a1i 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } e. _V )
121 91 92 addscld 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A +s ( 1s /su n ) ) e. No )
122 eleq1 
 |-  ( w = ( A +s ( 1s /su n ) ) -> ( w e. No <-> ( A +s ( 1s /su n ) ) e. No ) )
123 121 122 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( w = ( A +s ( 1s /su n ) ) -> w e. No ) )
124 123 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s w = ( A +s ( 1s /su n ) ) -> w e. No ) )
125 124 abssdv 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } C_ No )
126 100 42 elab 
 |-  ( y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } <-> E. n e. NN_s y = ( A +s ( 1s /su n ) ) )
127 92 91 sltaddpos1d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 0s  A
128 105 127 mpbid 
 |-  ( ( A e. No /\ n e. NN_s ) -> A
129 breq12 
 |-  ( ( z = A /\ y = ( A +s ( 1s /su n ) ) ) -> ( z  A
130 128 129 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( z = A /\ y = ( A +s ( 1s /su n ) ) ) -> z
131 130 expcomd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( y = ( A +s ( 1s /su n ) ) -> ( z = A -> z
132 131 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) -> ( z = A -> z
133 132 com23 
 |-  ( A e. No -> ( z = A -> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) -> z
134 133 3imp 
 |-  ( ( A e. No /\ z = A /\ E. n e. NN_s y = ( A +s ( 1s /su n ) ) ) -> z
135 99 102 126 134 syl3anb 
 |-  ( ( A e. No /\ z e. { A } /\ y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) -> z
136 90 120 98 125 135 ssltd 
 |-  ( A e. No -> { A } <
137 136 adantr 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { A } <
138 118 137 eqbrtrd 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } <
139 74 80 86 117 138 cofcut1d 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> ( ( _Left ` A ) |s ( _Right ` A ) ) = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) )
140 72 139 eqtr3d 
 |-  ( ( A e. No /\ ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) -> A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) )
141 70 140 impbida 
 |-  ( A e. No -> ( A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) )
142 ralunb 
 |-  ( A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) /\ A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) )
143 simpl 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> A e. No )
144 143 20 subscld 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( A -s xO ) e. No )
145 0sno 
 |-  0s e. No
146 145 a1i 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s e. No )
147 leftlt 
 |-  ( xO e. ( _Left ` A ) -> xO
148 147 adantl 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO
149 20 143 posdifsd 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO  0s
150 148 149 mpbid 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s
151 146 144 150 sltled 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s <_s ( A -s xO ) )
152 abssid 
 |-  ( ( ( A -s xO ) e. No /\ 0s <_s ( A -s xO ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) )
153 144 151 152 syl2anc 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) )
154 153 breq2d 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) )
155 154 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) )
156 144 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s xO ) e. No )
157 28 156 21 sleadd2d 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( A -s xO ) <-> ( xO +s ( 1s /su n ) ) <_s ( xO +s ( A -s xO ) ) ) )
158 pncan3s 
 |-  ( ( xO e. No /\ A e. No ) -> ( xO +s ( A -s xO ) ) = A )
159 20 143 158 syl2anc 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO +s ( A -s xO ) ) = A )
160 159 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO +s ( A -s xO ) ) = A )
161 160 breq2d 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( xO +s ( 1s /su n ) ) <_s ( xO +s ( A -s xO ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) )
162 155 157 161 3bitrd 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( xO +s ( 1s /su n ) ) <_s A ) )
163 162 rexbidva 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) )
164 163 ralbidva 
 |-  ( A e. No -> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A ) )
165 absssub 
 |-  ( ( A e. No /\ xO e. No ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) )
166 55 165 sylan2 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) )
167 166 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) )
168 simpl 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A e. No )
169 56 168 subscld 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( xO -s A ) e. No )
170 145 a1i 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s e. No )
171 rightgt 
 |-  ( xO e. ( _Right ` A ) -> A
172 171 adantl 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A
173 168 56 posdifsd 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( A  0s
174 172 173 mpbid 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s
175 170 169 174 sltled 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s <_s ( xO -s A ) )
176 abssid 
 |-  ( ( ( xO -s A ) e. No /\ 0s <_s ( xO -s A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) )
177 169 175 176 syl2anc 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) )
178 177 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) )
179 167 178 eqtrd 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( xO -s A ) )
180 179 breq2d 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( xO -s A ) ) )
181 58 57 53 slesubd 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( xO -s A ) <-> A <_s ( xO -s ( 1s /su n ) ) ) )
182 180 181 bitrd 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A <_s ( xO -s ( 1s /su n ) ) ) )
183 182 rexbidva 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
184 183 ralbidva 
 |-  ( A e. No -> ( A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) )
185 164 184 anbi12d 
 |-  ( A e. No -> ( ( A. xO e. ( _Left ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) /\ A. xO e. ( _Right ` A ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) )
186 142 185 bitrid 
 |-  ( A e. No -> ( A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( A. xO e. ( _Left ` A ) E. n e. NN_s ( xO +s ( 1s /su n ) ) <_s A /\ A. xO e. ( _Right ` A ) E. n e. NN_s A <_s ( xO -s ( 1s /su n ) ) ) ) )
187 141 186 bitr4d 
 |-  ( A e. No -> ( A = ( { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } |s { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) <-> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) E. n e. NN_s ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) ) )
188 187 anbi2d 
 |-  ( A e. No -> ( ( E. n e. NN_s ( ( -us ` n )  ( E. n e. NN_s ( ( -us ` n )
189 188 pm5.32i 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
190 1 189 bitri 
 |-  ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )