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 leftno 
 |-  ( xO e. ( _Left ` A ) -> xO e. No )
19 18 adantl 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO e. No )
20 19 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> xO e. No )
21 simpll 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> A e. No )
22 1no 
 |-  1s e. No
23 22 a1i 
 |-  ( n e. NN_s -> 1s e. No )
24 nnno 
 |-  ( n e. NN_s -> n e. No )
25 nnne0s 
 |-  ( n e. NN_s -> n =/= 0s )
26 23 24 25 divscld 
 |-  ( n e. NN_s -> ( 1s /su n ) e. No )
27 26 adantl 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No )
28 21 27 subscld 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No )
29 20 28 27 leadds1d 
 |-  ( ( ( 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 ) ) ) )
30 npcans 
 |-  ( ( A e. No /\ ( 1s /su n ) e. No ) -> ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) = A )
31 21 27 30 syl2anc 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( ( A -s ( 1s /su n ) ) +s ( 1s /su n ) ) = A )
32 31 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 ) )
33 29 32 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 ) )
34 33 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 ) )
35 34 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 ) )
36 17 35 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 ) )
37 36 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 ) )
38 5 37 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 )
39 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 )
40 eqeq1 
 |-  ( w = y -> ( w = ( A +s ( 1s /su n ) ) <-> y = ( A +s ( 1s /su n ) ) ) )
41 40 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 ) ) ) )
42 41 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 ) )
43 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 ) )
44 ovex 
 |-  ( A +s ( 1s /su n ) ) e. _V
45 breq1 
 |-  ( y = ( A +s ( 1s /su n ) ) -> ( y <_s xO <-> ( A +s ( 1s /su n ) ) <_s xO ) )
46 44 45 ceqsexv 
 |-  ( E. y ( y = ( A +s ( 1s /su n ) ) /\ y <_s xO ) <-> ( A +s ( 1s /su n ) ) <_s xO )
47 46 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 )
48 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 ) )
49 48 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 ) )
50 43 47 49 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 )
51 42 50 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 )
52 simpll 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> A e. No )
53 rightno 
 |-  ( xO e. ( _Right ` A ) -> xO e. No )
54 53 adantl 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> xO e. No )
55 54 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> xO e. No )
56 26 adantl 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( 1s /su n ) e. No )
57 55 56 subscld 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( xO -s ( 1s /su n ) ) e. No )
58 52 57 56 leadds1d 
 |-  ( ( ( 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 ) ) ) )
59 npcans 
 |-  ( ( xO e. No /\ ( 1s /su n ) e. No ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO )
60 55 56 59 syl2anc 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( ( xO -s ( 1s /su n ) ) +s ( 1s /su n ) ) = xO )
61 60 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 ) )
62 58 61 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 ) ) ) )
63 62 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 ) ) ) )
64 51 63 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 ) ) ) )
65 64 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 ) ) ) )
66 65 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 ) ) ) )
67 39 66 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 ) ) )
68 38 67 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 ) ) ) )
69 lrcut 
 |-  ( A e. No -> ( ( _Left ` A ) |s ( _Right ` A ) ) = A )
70 69 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 )
71 lltr 
 |-  ( _Left ` A ) <
72 71 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 ) <
73 34 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 ) ) )
74 73 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 )
75 74 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 ) )
76 75 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 ) )
77 76 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 )
78 77 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 )
79 63 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 )
80 79 51 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 )
81 80 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 ) )
82 81 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 ) )
83 82 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 )
84 83 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 )
85 nnsex 
 |-  NN_s e. _V
86 85 abrexex 
 |-  { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } e. _V
87 86 a1i 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } e. _V )
88 snexg 
 |-  ( A e. No -> { A } e. _V )
89 simpl 
 |-  ( ( A e. No /\ n e. NN_s ) -> A e. No )
90 26 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 1s /su n ) e. No )
91 89 90 subscld 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) ) e. No )
92 eleq1 
 |-  ( w = ( A -s ( 1s /su n ) ) -> ( w e. No <-> ( A -s ( 1s /su n ) ) e. No ) )
93 91 92 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( w = ( A -s ( 1s /su n ) ) -> w e. No ) )
94 93 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s w = ( A -s ( 1s /su n ) ) -> w e. No ) )
95 94 abssdv 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } C_ No )
96 snssi 
 |-  ( A e. No -> { A } C_ No )
97 biid 
 |-  ( A e. No <-> A e. No )
98 vex 
 |-  y e. _V
99 98 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 ) ) )
100 velsn 
 |-  ( z e. { A } <-> z = A )
101 id 
 |-  ( n e. NN_s -> n e. NN_s )
102 101 nnsrecgt0d 
 |-  ( n e. NN_s -> 0s
103 102 adantl 
 |-  ( ( A e. No /\ n e. NN_s ) -> 0s
104 90 89 ltsubsposd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 0s  ( A -s ( 1s /su n ) )
105 103 104 mpbid 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A -s ( 1s /su n ) )
106 breq12 
 |-  ( ( y = ( A -s ( 1s /su n ) ) /\ z = A ) -> ( y  ( A -s ( 1s /su n ) )
107 105 106 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( y = ( A -s ( 1s /su n ) ) /\ z = A ) -> y
108 107 expd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( y = ( A -s ( 1s /su n ) ) -> ( z = A -> y
109 108 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s y = ( A -s ( 1s /su n ) ) -> ( z = A -> y
110 109 3imp 
 |-  ( ( A e. No /\ E. n e. NN_s y = ( A -s ( 1s /su n ) ) /\ z = A ) -> y
111 97 99 100 110 syl3anb 
 |-  ( ( A e. No /\ y e. { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } /\ z e. { A } ) -> y
112 87 88 95 96 111 sltsd 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
113 69 sneqd 
 |-  ( A e. No -> { ( ( _Left ` A ) |s ( _Right ` A ) ) } = { A } )
114 112 113 breqtrrd 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A -s ( 1s /su n ) ) } <
115 114 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 ) ) } <
116 70 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 } )
117 85 abrexex 
 |-  { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } e. _V
118 117 a1i 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } e. _V )
119 89 90 addscld 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( A +s ( 1s /su n ) ) e. No )
120 eleq1 
 |-  ( w = ( A +s ( 1s /su n ) ) -> ( w e. No <-> ( A +s ( 1s /su n ) ) e. No ) )
121 119 120 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( w = ( A +s ( 1s /su n ) ) -> w e. No ) )
122 121 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s w = ( A +s ( 1s /su n ) ) -> w e. No ) )
123 122 abssdv 
 |-  ( A e. No -> { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } C_ No )
124 98 41 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 ) ) )
125 90 89 ltaddspos1d 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( 0s  A
126 103 125 mpbid 
 |-  ( ( A e. No /\ n e. NN_s ) -> A
127 breq12 
 |-  ( ( z = A /\ y = ( A +s ( 1s /su n ) ) ) -> ( z  A
128 126 127 syl5ibrcom 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( ( z = A /\ y = ( A +s ( 1s /su n ) ) ) -> z
129 128 expcomd 
 |-  ( ( A e. No /\ n e. NN_s ) -> ( y = ( A +s ( 1s /su n ) ) -> ( z = A -> z
130 129 rexlimdva 
 |-  ( A e. No -> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) -> ( z = A -> z
131 130 com23 
 |-  ( A e. No -> ( z = A -> ( E. n e. NN_s y = ( A +s ( 1s /su n ) ) -> z
132 131 3imp 
 |-  ( ( A e. No /\ z = A /\ E. n e. NN_s y = ( A +s ( 1s /su n ) ) ) -> z
133 97 100 124 132 syl3anb 
 |-  ( ( A e. No /\ z e. { A } /\ y e. { w | E. n e. NN_s w = ( A +s ( 1s /su n ) ) } ) -> z
134 88 118 96 123 133 sltsd 
 |-  ( A e. No -> { A } <
135 134 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 } <
136 116 135 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 ) ) } <
137 72 78 84 115 136 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 ) ) } ) )
138 70 137 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 ) ) } ) )
139 68 138 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 ) ) ) ) )
140 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 ) ) ) )
141 simpl 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> A e. No )
142 141 19 subscld 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( A -s xO ) e. No )
143 0no 
 |-  0s e. No
144 143 a1i 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s e. No )
145 leftlt 
 |-  ( xO e. ( _Left ` A ) -> xO
146 145 adantl 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> xO
147 19 141 posdifsd 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO  0s
148 146 147 mpbid 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s
149 144 142 148 ltlesd 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> 0s <_s ( A -s xO ) )
150 abssid 
 |-  ( ( ( A -s xO ) e. No /\ 0s <_s ( A -s xO ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) )
151 142 149 150 syl2anc 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( A -s xO ) )
152 151 breq2d 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( ( 1s /su n ) <_s ( abs_s ` ( A -s xO ) ) <-> ( 1s /su n ) <_s ( A -s xO ) ) )
153 152 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 ) ) )
154 142 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( A -s xO ) e. No )
155 27 154 20 leadds2d 
 |-  ( ( ( 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 ) ) ) )
156 pncan3s 
 |-  ( ( xO e. No /\ A e. No ) -> ( xO +s ( A -s xO ) ) = A )
157 19 141 156 syl2anc 
 |-  ( ( A e. No /\ xO e. ( _Left ` A ) ) -> ( xO +s ( A -s xO ) ) = A )
158 157 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Left ` A ) ) /\ n e. NN_s ) -> ( xO +s ( A -s xO ) ) = A )
159 158 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 ) )
160 153 155 159 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 ) )
161 160 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 ) )
162 161 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 ) )
163 abssubs 
 |-  ( ( A e. No /\ xO e. No ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) )
164 53 163 sylan2 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) )
165 164 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( abs_s ` ( xO -s A ) ) )
166 simpl 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A e. No )
167 54 166 subscld 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( xO -s A ) e. No )
168 143 a1i 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s e. No )
169 rightgt 
 |-  ( xO e. ( _Right ` A ) -> A
170 169 adantl 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> A
171 166 54 posdifsd 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( A  0s
172 170 171 mpbid 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s
173 168 167 172 ltlesd 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> 0s <_s ( xO -s A ) )
174 abssid 
 |-  ( ( ( xO -s A ) e. No /\ 0s <_s ( xO -s A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) )
175 167 173 174 syl2anc 
 |-  ( ( A e. No /\ xO e. ( _Right ` A ) ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) )
176 175 adantr 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( xO -s A ) ) = ( xO -s A ) )
177 165 176 eqtrd 
 |-  ( ( ( A e. No /\ xO e. ( _Right ` A ) ) /\ n e. NN_s ) -> ( abs_s ` ( A -s xO ) ) = ( xO -s A ) )
178 177 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 ) ) )
179 56 55 52 lesubsd 
 |-  ( ( ( 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 ) ) ) )
180 178 179 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 ) ) ) )
181 180 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 ) ) ) )
182 181 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 ) ) ) )
183 162 182 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 ) ) ) ) )
184 140 183 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 ) ) ) ) )
185 139 184 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 ) ) ) )
186 185 anbi2d 
 |-  ( A e. No -> ( ( E. n e. NN_s ( ( -us ` n )  ( E. n e. NN_s ( ( -us ` n )
187 186 pm5.32i 
 |-  ( ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )  ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )
188 1 187 bitri 
 |-  ( A e. RR_s <-> ( A e. No /\ ( E. n e. NN_s ( ( -us ` n )