Metamath Proof Explorer

Theorem ioodvbdlimc1lem2

Description: Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc1lem2.a 
|- ( ph -> A e. RR )
ioodvbdlimc1lem2.b 
|- ( ph -> B e. RR )
ioodvbdlimc1lem2.altb 
|- ( ph -> A < B )
ioodvbdlimc1lem2.f 
|- ( ph -> F : ( A (,) B ) --> RR )
ioodvbdlimc1lem2.dmdv 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
ioodvbdlimc1lem2.dvbd 
|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
ioodvbdlimc1lem2.y 
|- Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
ioodvbdlimc1lem2.m 
|- M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )
ioodvbdlimc1lem2.s 
|- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( A + ( 1 / j ) ) ) )
ioodvbdlimc1lem2.r 
|- R = ( j e. ( ZZ>= ` M ) |-> ( A + ( 1 / j ) ) )
ioodvbdlimc1lem2.n 
|- N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
ioodvbdlimc1lem2.ch 
|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
Assertion ioodvbdlimc1lem2 
|- ( ph -> ( limsup ` S ) e. ( F limCC A ) )

Proof

Step Hyp Ref Expression
1 ioodvbdlimc1lem2.a 
 |-  ( ph -> A e. RR )
2 ioodvbdlimc1lem2.b 
 |-  ( ph -> B e. RR )
3 ioodvbdlimc1lem2.altb 
 |-  ( ph -> A < B )
4 ioodvbdlimc1lem2.f 
 |-  ( ph -> F : ( A (,) B ) --> RR )
5 ioodvbdlimc1lem2.dmdv 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6 ioodvbdlimc1lem2.dvbd 
 |-  ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
7 ioodvbdlimc1lem2.y 
 |-  Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
8 ioodvbdlimc1lem2.m 
 |-  M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )
9 ioodvbdlimc1lem2.s 
 |-  S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( A + ( 1 / j ) ) ) )
10 ioodvbdlimc1lem2.r 
 |-  R = ( j e. ( ZZ>= ` M ) |-> ( A + ( 1 / j ) ) )
11 ioodvbdlimc1lem2.n 
 |-  N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
12 ioodvbdlimc1lem2.ch 
 |-  ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
13 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
14 zssre 
 |-  ZZ C_ RR
15 13 14 sstri 
 |-  ( ZZ>= ` M ) C_ RR
16 15 a1i 
 |-  ( ph -> ( ZZ>= ` M ) C_ RR )
17 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
18 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
19 3 18 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
20 19 gt0ne0d 
 |-  ( ph -> ( B - A ) =/= 0 )
21 17 20 rereccld 
 |-  ( ph -> ( 1 / ( B - A ) ) e. RR )
22 0red 
 |-  ( ph -> 0 e. RR )
23 17 19 recgt0d 
 |-  ( ph -> 0 < ( 1 / ( B - A ) ) )
24 22 21 23 ltled 
 |-  ( ph -> 0 <_ ( 1 / ( B - A ) ) )
25 flge0nn0 
 |-  ( ( ( 1 / ( B - A ) ) e. RR /\ 0 <_ ( 1 / ( B - A ) ) ) -> ( |_ ` ( 1 / ( B - A ) ) ) e. NN0 )
26 21 24 25 syl2anc 
 |-  ( ph -> ( |_ ` ( 1 / ( B - A ) ) ) e. NN0 )
27 peano2nn0 
 |-  ( ( |_ ` ( 1 / ( B - A ) ) ) e. NN0 -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. NN0 )
28 26 27 syl 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. NN0 )
29 8 28 eqeltrid 
 |-  ( ph -> M e. NN0 )
30 29 nn0zd 
 |-  ( ph -> M e. ZZ )
31 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
32 31 uzsup 
 |-  ( M e. ZZ -> sup ( ( ZZ>= ` M ) , RR* , < ) = +oo )
33 30 32 syl 
 |-  ( ph -> sup ( ( ZZ>= ` M ) , RR* , < ) = +oo )
34 4 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> F : ( A (,) B ) --> RR )
35 1 rexrd 
 |-  ( ph -> A e. RR* )
36 35 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A e. RR* )
37 2 rexrd 
 |-  ( ph -> B e. RR* )
38 37 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> B e. RR* )
39 1 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A e. RR )
40 eluzelre 
 |-  ( j e. ( ZZ>= ` M ) -> j e. RR )
41 40 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. RR )
42 0red 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 e. RR )
43 0red 
 |-  ( j e. ( ZZ>= ` M ) -> 0 e. RR )
44 1red 
 |-  ( j e. ( ZZ>= ` M ) -> 1 e. RR )
45 43 44 readdcld 
 |-  ( j e. ( ZZ>= ` M ) -> ( 0 + 1 ) e. RR )
46 45 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) e. RR )
47 43 ltp1d 
 |-  ( j e. ( ZZ>= ` M ) -> 0 < ( 0 + 1 ) )
48 47 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 < ( 0 + 1 ) )
49 eluzel2 
 |-  ( j e. ( ZZ>= ` M ) -> M e. ZZ )
50 49 zred 
 |-  ( j e. ( ZZ>= ` M ) -> M e. RR )
51 50 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M e. RR )
52 21 flcld 
 |-  ( ph -> ( |_ ` ( 1 / ( B - A ) ) ) e. ZZ )
53 52 zred 
 |-  ( ph -> ( |_ ` ( 1 / ( B - A ) ) ) e. RR )
54 1red 
 |-  ( ph -> 1 e. RR )
55 26 nn0ge0d 
 |-  ( ph -> 0 <_ ( |_ ` ( 1 / ( B - A ) ) ) )
56 22 53 54 55 leadd1dd 
 |-  ( ph -> ( 0 + 1 ) <_ ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
57 56 8 breqtrrdi 
 |-  ( ph -> ( 0 + 1 ) <_ M )
58 57 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) <_ M )
59 eluzle 
 |-  ( j e. ( ZZ>= ` M ) -> M <_ j )
60 59 adantl 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M <_ j )
61 46 51 41 58 60 letrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 0 + 1 ) <_ j )
62 42 46 41 48 61 ltletrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 < j )
63 62 gt0ne0d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j =/= 0 )
64 41 63 rereccld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) e. RR )
65 39 64 readdcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) e. RR )
66 41 62 elrpd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. RR+ )
67 66 rpreccld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) e. RR+ )
68 39 67 ltaddrpd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> A < ( A + ( 1 / j ) ) )
69 29 nn0red 
 |-  ( ph -> M e. RR )
70 22 54 readdcld 
 |-  ( ph -> ( 0 + 1 ) e. RR )
71 53 54 readdcld 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. RR )
72 22 ltp1d 
 |-  ( ph -> 0 < ( 0 + 1 ) )
73 22 70 71 72 56 ltletrd 
 |-  ( ph -> 0 < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
74 73 8 breqtrrdi 
 |-  ( ph -> 0 < M )
75 74 gt0ne0d 
 |-  ( ph -> M =/= 0 )
76 69 75 rereccld 
 |-  ( ph -> ( 1 / M ) e. RR )
77 76 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / M ) e. RR )
78 39 77 readdcld 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / M ) ) e. RR )
79 2 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> B e. RR )
80 69 74 elrpd 
 |-  ( ph -> M e. RR+ )
81 80 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> M e. RR+ )
82 1red 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 1 e. RR )
83 0le1 
 |-  0 <_ 1
84 83 a1i 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> 0 <_ 1 )
85 81 66 82 84 60 lediv2ad 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( 1 / j ) <_ ( 1 / M ) )
86 64 77 39 85 leadd2dd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) <_ ( A + ( 1 / M ) ) )
87 8 eqcomi 
 |-  ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) = M
88 87 oveq2i 
 |-  ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) = ( 1 / M )
89 88 76 eqeltrid 
 |-  ( ph -> ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) e. RR )
90 21 23 elrpd 
 |-  ( ph -> ( 1 / ( B - A ) ) e. RR+ )
91 71 73 elrpd 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. RR+ )
92 1rp 
 |-  1 e. RR+
93 92 a1i 
 |-  ( ph -> 1 e. RR+ )
94 fllelt 
 |-  ( ( 1 / ( B - A ) ) e. RR -> ( ( |_ ` ( 1 / ( B - A ) ) ) <_ ( 1 / ( B - A ) ) /\ ( 1 / ( B - A ) ) < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
95 21 94 syl 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) <_ ( 1 / ( B - A ) ) /\ ( 1 / ( B - A ) ) < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
96 95 simprd 
 |-  ( ph -> ( 1 / ( B - A ) ) < ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
97 90 91 93 96 ltdiv2dd 
 |-  ( ph -> ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) < ( 1 / ( 1 / ( B - A ) ) ) )
98 17 recnd 
 |-  ( ph -> ( B - A ) e. CC )
99 98 20 recrecd 
 |-  ( ph -> ( 1 / ( 1 / ( B - A ) ) ) = ( B - A ) )
100 97 99 breqtrd 
 |-  ( ph -> ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) < ( B - A ) )
101 89 17 1 100 ltadd2dd 
 |-  ( ph -> ( A + ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) < ( A + ( B - A ) ) )
102 8 oveq2i 
 |-  ( 1 / M ) = ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) )
103 102 oveq2i 
 |-  ( A + ( 1 / M ) ) = ( A + ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) )
104 103 a1i 
 |-  ( ph -> ( A + ( 1 / M ) ) = ( A + ( 1 / ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) ) ) )
105 1 recnd 
 |-  ( ph -> A e. CC )
106 2 recnd 
 |-  ( ph -> B e. CC )
107 105 106 pncan3d 
 |-  ( ph -> ( A + ( B - A ) ) = B )
108 107 eqcomd 
 |-  ( ph -> B = ( A + ( B - A ) ) )
109 101 104 108 3brtr4d 
 |-  ( ph -> ( A + ( 1 / M ) ) < B )
110 109 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / M ) ) < B )
111 65 78 79 86 110 lelttrd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) < B )
112 36 38 65 68 111 eliood 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) e. ( A (,) B ) )
113 34 112 ffvelrnd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( A + ( 1 / j ) ) ) e. RR )
114 113 9 fmptd 
 |-  ( ph -> S : ( ZZ>= ` M ) --> RR )
115 1 2 3 4 5 6 dvbdfbdioo 
 |-  ( ph -> E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
116 69 adantr 
 |-  ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> M e. RR )
117 simpr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> j e. ( ZZ>= ` M ) )
118 9 fvmpt2 
 |-  ( ( j e. ( ZZ>= ` M ) /\ ( F ` ( A + ( 1 / j ) ) ) e. RR ) -> ( S ` j ) = ( F ` ( A + ( 1 / j ) ) ) )
119 117 113 118 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( S ` j ) = ( F ` ( A + ( 1 / j ) ) ) )
120 119 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) = ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) )
121 120 adantlr 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) = ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) )
122 simplr 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )
123 112 adantlr 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) e. ( A (,) B ) )
124 2fveq3 
 |-  ( x = ( A + ( 1 / j ) ) -> ( abs ` ( F ` x ) ) = ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) )
125 124 breq1d 
 |-  ( x = ( A + ( 1 / j ) ) -> ( ( abs ` ( F ` x ) ) <_ b <-> ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) <_ b ) )
126 125 rspccva 
 |-  ( ( A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b /\ ( A + ( 1 / j ) ) e. ( A (,) B ) ) -> ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) <_ b )
127 122 123 126 syl2anc 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( F ` ( A + ( 1 / j ) ) ) ) <_ b )
128 121 127 eqbrtrd 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( abs ` ( S ` j ) ) <_ b )
129 128 a1d 
 |-  ( ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) /\ j e. ( ZZ>= ` M ) ) -> ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
130 129 ralrimiva 
 |-  ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
131 breq1 
 |-  ( k = M -> ( k <_ j <-> M <_ j ) )
132 131 imbi1d 
 |-  ( k = M -> ( ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) <-> ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
133 132 ralbidv 
 |-  ( k = M -> ( A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) <-> A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
134 133 rspcev 
 |-  ( ( M e. RR /\ A. j e. ( ZZ>= ` M ) ( M <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
135 116 130 134 syl2anc 
 |-  ( ( ph /\ A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b ) -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
136 135 ex 
 |-  ( ph -> ( A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b -> E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
137 136 reximdv 
 |-  ( ph -> ( E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b -> E. b e. RR E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) ) )
138 115 137 mpd 
 |-  ( ph -> E. b e. RR E. k e. RR A. j e. ( ZZ>= ` M ) ( k <_ j -> ( abs ` ( S ` j ) ) <_ b ) )
139 16 33 114 138 limsupre 
 |-  ( ph -> ( limsup ` S ) e. RR )
140 139 recnd 
 |-  ( ph -> ( limsup ` S ) e. CC )
141 eluzelre 
 |-  ( j e. ( ZZ>= ` N ) -> j e. RR )
142 141 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> j e. RR )
143 0red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 e. RR )
144 52 peano2zd 
 |-  ( ph -> ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 ) e. ZZ )
145 8 144 eqeltrid 
 |-  ( ph -> M e. ZZ )
146 145 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> M e. ZZ )
147 146 zred 
 |-  ( ( ph /\ x e. RR+ ) -> M e. RR )
148 147 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M e. RR )
149 74 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < M )
150 ioomidp 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
151 1 2 3 150 syl3anc 
 |-  ( ph -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
152 ne0i 
 |-  ( ( ( A + B ) / 2 ) e. ( A (,) B ) -> ( A (,) B ) =/= (/) )
153 151 152 syl 
 |-  ( ph -> ( A (,) B ) =/= (/) )
154 ioossre 
 |-  ( A (,) B ) C_ RR
155 154 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
156 dvfre 
 |-  ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
157 4 155 156 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
158 5 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : ( A (,) B ) --> RR ) )
159 157 158 mpbid 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> RR )
160 159 ffvelrnda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. RR )
161 160 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
162 161 abscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
163 eqid 
 |-  ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
164 eqid 
 |-  sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
165 153 162 6 163 164 suprnmpt 
 |-  ( ph -> ( sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR /\ A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) )
166 165 simpld 
 |-  ( ph -> sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR )
167 7 166 eqeltrid 
 |-  ( ph -> Y e. RR )
168 167 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> Y e. RR )
169 rpre 
 |-  ( x e. RR+ -> x e. RR )
170 169 rehalfcld 
 |-  ( x e. RR+ -> ( x / 2 ) e. RR )
171 170 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR )
172 169 recnd 
 |-  ( x e. RR+ -> x e. CC )
173 172 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. CC )
174 2cnd 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. CC )
175 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
176 175 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x =/= 0 )
177 2ne0 
 |-  2 =/= 0
178 177 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 =/= 0 )
179 173 174 176 178 divne0d 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) =/= 0 )
180 168 171 179 redivcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( Y / ( x / 2 ) ) e. RR )
181 180 flcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` ( Y / ( x / 2 ) ) ) e. ZZ )
182 181 peano2zd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. ZZ )
183 182 146 ifcld 
 |-  ( ( ph /\ x e. RR+ ) -> if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) e. ZZ )
184 11 183 eqeltrid 
 |-  ( ( ph /\ x e. RR+ ) -> N e. ZZ )
185 184 zred 
 |-  ( ( ph /\ x e. RR+ ) -> N e. RR )
186 185 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> N e. RR )
187 182 zred 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR )
188 max1 
 |-  ( ( M e. RR /\ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR ) -> M <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
189 147 187 188 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> M <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
190 189 11 breqtrrdi 
 |-  ( ( ph /\ x e. RR+ ) -> M <_ N )
191 190 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M <_ N )
192 eluzle 
 |-  ( j e. ( ZZ>= ` N ) -> N <_ j )
193 192 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> N <_ j )
194 148 186 142 191 193 letrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> M <_ j )
195 143 148 142 149 194 ltletrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < j )
196 195 gt0ne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> j =/= 0 )
197 142 196 rereccld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> ( 1 / j ) e. RR )
198 142 195 recgt0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> 0 < ( 1 / j ) )
199 197 198 elrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) -> ( 1 / j ) e. RR+ )
200 199 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> ( 1 / j ) e. RR+ )
201 12 biimpi 
 |-  ( ch -> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )
202 simp-5l 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ph )
203 201 202 syl 
 |-  ( ch -> ph )
204 203 4 syl 
 |-  ( ch -> F : ( A (,) B ) --> RR )
205 201 simplrd 
 |-  ( ch -> z e. ( A (,) B ) )
206 204 205 ffvelrnd 
 |-  ( ch -> ( F ` z ) e. RR )
207 206 recnd 
 |-  ( ch -> ( F ` z ) e. CC )
208 203 114 syl 
 |-  ( ch -> S : ( ZZ>= ` M ) --> RR )
209 simp-5r 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> x e. RR+ )
210 201 209 syl 
 |-  ( ch -> x e. RR+ )
211 eluz2 
 |-  ( N e. ( ZZ>= ` M ) <-> ( M e. ZZ /\ N e. ZZ /\ M <_ N ) )
212 146 184 190 211 syl3anbrc 
 |-  ( ( ph /\ x e. RR+ ) -> N e. ( ZZ>= ` M ) )
213 203 210 212 syl2anc 
 |-  ( ch -> N e. ( ZZ>= ` M ) )
214 uzss 
 |-  ( N e. ( ZZ>= ` M ) -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
215 213 214 syl 
 |-  ( ch -> ( ZZ>= ` N ) C_ ( ZZ>= ` M ) )
216 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> j e. ( ZZ>= ` N ) )
217 201 216 syl 
 |-  ( ch -> j e. ( ZZ>= ` N ) )
218 215 217 sseldd 
 |-  ( ch -> j e. ( ZZ>= ` M ) )
219 208 218 ffvelrnd 
 |-  ( ch -> ( S ` j ) e. RR )
220 219 recnd 
 |-  ( ch -> ( S ` j ) e. CC )
221 203 140 syl 
 |-  ( ch -> ( limsup ` S ) e. CC )
222 207 220 221 npncand 
 |-  ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) = ( ( F ` z ) - ( limsup ` S ) ) )
223 222 eqcomd 
 |-  ( ch -> ( ( F ` z ) - ( limsup ` S ) ) = ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) )
224 223 fveq2d 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) = ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) )
225 206 219 resubcld 
 |-  ( ch -> ( ( F ` z ) - ( S ` j ) ) e. RR )
226 203 139 syl 
 |-  ( ch -> ( limsup ` S ) e. RR )
227 219 226 resubcld 
 |-  ( ch -> ( ( S ` j ) - ( limsup ` S ) ) e. RR )
228 225 227 readdcld 
 |-  ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) e. RR )
229 228 recnd 
 |-  ( ch -> ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) e. CC )
230 229 abscld 
 |-  ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) e. RR )
231 225 recnd 
 |-  ( ch -> ( ( F ` z ) - ( S ` j ) ) e. CC )
232 231 abscld 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) e. RR )
233 227 recnd 
 |-  ( ch -> ( ( S ` j ) - ( limsup ` S ) ) e. CC )
234 233 abscld 
 |-  ( ch -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) e. RR )
235 232 234 readdcld 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) e. RR )
236 210 rpred 
 |-  ( ch -> x e. RR )
237 231 233 abstrid 
 |-  ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) <_ ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) )
238 236 rehalfcld 
 |-  ( ch -> ( x / 2 ) e. RR )
239 207 220 abssubd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) = ( abs ` ( ( S ` j ) - ( F ` z ) ) ) )
240 203 218 119 syl2anc 
 |-  ( ch -> ( S ` j ) = ( F ` ( A + ( 1 / j ) ) ) )
241 240 fvoveq1d 
 |-  ( ch -> ( abs ` ( ( S ` j ) - ( F ` z ) ) ) = ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) )
242 203 218 113 syl2anc 
 |-  ( ch -> ( F ` ( A + ( 1 / j ) ) ) e. RR )
243 242 206 resubcld 
 |-  ( ch -> ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) e. RR )
244 243 recnd 
 |-  ( ch -> ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) e. CC )
245 244 abscld 
 |-  ( ch -> ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) e. RR )
246 203 167 syl 
 |-  ( ch -> Y e. RR )
247 203 218 65 syl2anc 
 |-  ( ch -> ( A + ( 1 / j ) ) e. RR )
248 154 205 sselid 
 |-  ( ch -> z e. RR )
249 247 248 resubcld 
 |-  ( ch -> ( ( A + ( 1 / j ) ) - z ) e. RR )
250 246 249 remulcld 
 |-  ( ch -> ( Y x. ( ( A + ( 1 / j ) ) - z ) ) e. RR )
251 203 1 syl 
 |-  ( ch -> A e. RR )
252 203 2 syl 
 |-  ( ch -> B e. RR )
253 203 5 syl 
 |-  ( ch -> dom ( RR _D F ) = ( A (,) B ) )
254 165 simprd 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
255 7 breq2i 
 |-  ( ( abs ` ( ( RR _D F ) ` x ) ) <_ Y <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
256 255 ralbii 
 |-  ( A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
257 254 256 sylibr 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
258 203 257 syl 
 |-  ( ch -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
259 2fveq3 
 |-  ( w = x -> ( abs ` ( ( RR _D F ) ` w ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
260 259 breq1d 
 |-  ( w = x -> ( ( abs ` ( ( RR _D F ) ` w ) ) <_ Y <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ Y ) )
261 260 cbvralvw 
 |-  ( A. w e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` w ) ) <_ Y <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ Y )
262 258 261 sylibr 
 |-  ( ch -> A. w e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` w ) ) <_ Y )
263 248 rexrd 
 |-  ( ch -> z e. RR* )
264 203 37 syl 
 |-  ( ch -> B e. RR* )
265 248 251 resubcld 
 |-  ( ch -> ( z - A ) e. RR )
266 265 recnd 
 |-  ( ch -> ( z - A ) e. CC )
267 266 abscld 
 |-  ( ch -> ( abs ` ( z - A ) ) e. RR )
268 15 218 sselid 
 |-  ( ch -> j e. RR )
269 203 218 63 syl2anc 
 |-  ( ch -> j =/= 0 )
270 268 269 rereccld 
 |-  ( ch -> ( 1 / j ) e. RR )
271 265 leabsd 
 |-  ( ch -> ( z - A ) <_ ( abs ` ( z - A ) ) )
272 201 simprd 
 |-  ( ch -> ( abs ` ( z - A ) ) < ( 1 / j ) )
273 265 267 270 271 272 lelttrd 
 |-  ( ch -> ( z - A ) < ( 1 / j ) )
274 248 251 270 ltsubadd2d 
 |-  ( ch -> ( ( z - A ) < ( 1 / j ) <-> z < ( A + ( 1 / j ) ) ) )
275 273 274 mpbid 
 |-  ( ch -> z < ( A + ( 1 / j ) ) )
276 203 218 111 syl2anc 
 |-  ( ch -> ( A + ( 1 / j ) ) < B )
277 263 264 247 275 276 eliood 
 |-  ( ch -> ( A + ( 1 / j ) ) e. ( z (,) B ) )
278 251 252 204 253 246 262 205 277 dvbdfbdioolem1 
 |-  ( ch -> ( ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( Y x. ( ( A + ( 1 / j ) ) - z ) ) /\ ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( Y x. ( B - A ) ) ) )
279 278 simpld 
 |-  ( ch -> ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( Y x. ( ( A + ( 1 / j ) ) - z ) ) )
280 203 218 64 syl2anc 
 |-  ( ch -> ( 1 / j ) e. RR )
281 246 280 remulcld 
 |-  ( ch -> ( Y x. ( 1 / j ) ) e. RR )
282 159 151 ffvelrnd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. RR )
283 282 recnd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. CC )
284 283 abscld 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) e. RR )
285 283 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
286 2fveq3 
 |-  ( x = ( ( A + B ) / 2 ) -> ( abs ` ( ( RR _D F ) ` x ) ) = ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
287 7 eqcomi 
 |-  sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = Y
288 287 a1i 
 |-  ( x = ( ( A + B ) / 2 ) -> sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) = Y )
289 286 288 breq12d 
 |-  ( x = ( ( A + B ) / 2 ) -> ( ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y ) )
290 289 rspcva 
 |-  ( ( ( ( A + B ) / 2 ) e. ( A (,) B ) /\ A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y )
291 151 254 290 syl2anc 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ Y )
292 22 284 167 285 291 letrd 
 |-  ( ph -> 0 <_ Y )
293 203 292 syl 
 |-  ( ch -> 0 <_ Y )
294 203 35 syl 
 |-  ( ch -> A e. RR* )
295 ioogtlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ z e. ( A (,) B ) ) -> A < z )
296 294 264 205 295 syl3anc 
 |-  ( ch -> A < z )
297 251 248 247 296 ltsub2dd 
 |-  ( ch -> ( ( A + ( 1 / j ) ) - z ) < ( ( A + ( 1 / j ) ) - A ) )
298 203 105 syl 
 |-  ( ch -> A e. CC )
299 280 recnd 
 |-  ( ch -> ( 1 / j ) e. CC )
300 298 299 pncan2d 
 |-  ( ch -> ( ( A + ( 1 / j ) ) - A ) = ( 1 / j ) )
301 297 300 breqtrd 
 |-  ( ch -> ( ( A + ( 1 / j ) ) - z ) < ( 1 / j ) )
302 249 270 301 ltled 
 |-  ( ch -> ( ( A + ( 1 / j ) ) - z ) <_ ( 1 / j ) )
303 249 270 246 293 302 lemul2ad 
 |-  ( ch -> ( Y x. ( ( A + ( 1 / j ) ) - z ) ) <_ ( Y x. ( 1 / j ) ) )
304 281 adantr 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) e. RR )
305 238 adantr 
 |-  ( ( ch /\ Y = 0 ) -> ( x / 2 ) e. RR )
306 oveq1 
 |-  ( Y = 0 -> ( Y x. ( 1 / j ) ) = ( 0 x. ( 1 / j ) ) )
307 299 mul02d 
 |-  ( ch -> ( 0 x. ( 1 / j ) ) = 0 )
308 306 307 sylan9eqr 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) = 0 )
309 210 rphalfcld 
 |-  ( ch -> ( x / 2 ) e. RR+ )
310 309 rpgt0d 
 |-  ( ch -> 0 < ( x / 2 ) )
311 310 adantr 
 |-  ( ( ch /\ Y = 0 ) -> 0 < ( x / 2 ) )
312 308 311 eqbrtrd 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) < ( x / 2 ) )
313 304 305 312 ltled 
 |-  ( ( ch /\ Y = 0 ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
314 246 adantr 
 |-  ( ( ch /\ -. Y = 0 ) -> Y e. RR )
315 293 adantr 
 |-  ( ( ch /\ -. Y = 0 ) -> 0 <_ Y )
316 neqne 
 |-  ( -. Y = 0 -> Y =/= 0 )
317 316 adantl 
 |-  ( ( ch /\ -. Y = 0 ) -> Y =/= 0 )
318 314 315 317 ne0gt0d 
 |-  ( ( ch /\ -. Y = 0 ) -> 0 < Y )
319 281 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) e. RR )
320 15 213 sselid 
 |-  ( ch -> N e. RR )
321 0red 
 |-  ( ch -> 0 e. RR )
322 203 210 147 syl2anc 
 |-  ( ch -> M e. RR )
323 203 74 syl 
 |-  ( ch -> 0 < M )
324 203 210 190 syl2anc 
 |-  ( ch -> M <_ N )
325 321 322 320 323 324 ltletrd 
 |-  ( ch -> 0 < N )
326 325 gt0ne0d 
 |-  ( ch -> N =/= 0 )
327 320 326 rereccld 
 |-  ( ch -> ( 1 / N ) e. RR )
328 246 327 remulcld 
 |-  ( ch -> ( Y x. ( 1 / N ) ) e. RR )
329 328 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) e. RR )
330 238 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( x / 2 ) e. RR )
331 280 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / j ) e. RR )
332 327 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / N ) e. RR )
333 246 adantr 
 |-  ( ( ch /\ 0 < Y ) -> Y e. RR )
334 293 adantr 
 |-  ( ( ch /\ 0 < Y ) -> 0 <_ Y )
335 320 325 elrpd 
 |-  ( ch -> N e. RR+ )
336 203 218 66 syl2anc 
 |-  ( ch -> j e. RR+ )
337 1red 
 |-  ( ch -> 1 e. RR )
338 83 a1i 
 |-  ( ch -> 0 <_ 1 )
339 217 192 syl 
 |-  ( ch -> N <_ j )
340 335 336 337 338 339 lediv2ad 
 |-  ( ch -> ( 1 / j ) <_ ( 1 / N ) )
341 340 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / j ) <_ ( 1 / N ) )
342 331 332 333 334 341 lemul2ad 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) <_ ( Y x. ( 1 / N ) ) )
343 236 recnd 
 |-  ( ch -> x e. CC )
344 2cnd 
 |-  ( ch -> 2 e. CC )
345 210 rpne0d 
 |-  ( ch -> x =/= 0 )
346 177 a1i 
 |-  ( ch -> 2 =/= 0 )
347 343 344 345 346 divne0d 
 |-  ( ch -> ( x / 2 ) =/= 0 )
348 246 238 347 redivcld 
 |-  ( ch -> ( Y / ( x / 2 ) ) e. RR )
349 348 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. RR )
350 simpr 
 |-  ( ( ch /\ 0 < Y ) -> 0 < Y )
351 310 adantr 
 |-  ( ( ch /\ 0 < Y ) -> 0 < ( x / 2 ) )
352 333 330 350 351 divgt0d 
 |-  ( ( ch /\ 0 < Y ) -> 0 < ( Y / ( x / 2 ) ) )
353 349 352 elrpd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. RR+ )
354 353 rprecred 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / ( Y / ( x / 2 ) ) ) e. RR )
355 335 adantr 
 |-  ( ( ch /\ 0 < Y ) -> N e. RR+ )
356 1red 
 |-  ( ( ch /\ 0 < Y ) -> 1 e. RR )
357 83 a1i 
 |-  ( ( ch /\ 0 < Y ) -> 0 <_ 1 )
358 348 flcld 
 |-  ( ch -> ( |_ ` ( Y / ( x / 2 ) ) ) e. ZZ )
359 358 peano2zd 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. ZZ )
360 359 zred 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR )
361 203 145 syl 
 |-  ( ch -> M e. ZZ )
362 359 361 ifcld 
 |-  ( ch -> if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) e. ZZ )
363 11 362 eqeltrid 
 |-  ( ch -> N e. ZZ )
364 363 zred 
 |-  ( ch -> N e. RR )
365 flltp1 
 |-  ( ( Y / ( x / 2 ) ) e. RR -> ( Y / ( x / 2 ) ) < ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) )
366 348 365 syl 
 |-  ( ch -> ( Y / ( x / 2 ) ) < ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) )
367 203 69 syl 
 |-  ( ch -> M e. RR )
368 max2 
 |-  ( ( M e. RR /\ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) e. RR ) -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
369 367 360 368 syl2anc 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M ) )
370 369 11 breqtrrdi 
 |-  ( ch -> ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) <_ N )
371 348 360 364 366 370 ltletrd 
 |-  ( ch -> ( Y / ( x / 2 ) ) < N )
372 348 320 371 ltled 
 |-  ( ch -> ( Y / ( x / 2 ) ) <_ N )
373 372 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) <_ N )
374 353 355 356 357 373 lediv2ad 
 |-  ( ( ch /\ 0 < Y ) -> ( 1 / N ) <_ ( 1 / ( Y / ( x / 2 ) ) ) )
375 332 354 333 334 374 lemul2ad 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) <_ ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) )
376 333 recnd 
 |-  ( ( ch /\ 0 < Y ) -> Y e. CC )
377 349 recnd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) e. CC )
378 352 gt0ne0d 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( x / 2 ) ) =/= 0 )
379 376 377 378 divrecd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( Y / ( x / 2 ) ) ) = ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) )
380 330 recnd 
 |-  ( ( ch /\ 0 < Y ) -> ( x / 2 ) e. CC )
381 350 gt0ne0d 
 |-  ( ( ch /\ 0 < Y ) -> Y =/= 0 )
382 347 adantr 
 |-  ( ( ch /\ 0 < Y ) -> ( x / 2 ) =/= 0 )
383 376 380 381 382 ddcand 
 |-  ( ( ch /\ 0 < Y ) -> ( Y / ( Y / ( x / 2 ) ) ) = ( x / 2 ) )
384 379 383 eqtr3d 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / ( Y / ( x / 2 ) ) ) ) = ( x / 2 ) )
385 375 384 breqtrd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / N ) ) <_ ( x / 2 ) )
386 319 329 330 342 385 letrd 
 |-  ( ( ch /\ 0 < Y ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
387 318 386 syldan 
 |-  ( ( ch /\ -. Y = 0 ) -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
388 313 387 pm2.61dan 
 |-  ( ch -> ( Y x. ( 1 / j ) ) <_ ( x / 2 ) )
389 250 281 238 303 388 letrd 
 |-  ( ch -> ( Y x. ( ( A + ( 1 / j ) ) - z ) ) <_ ( x / 2 ) )
390 245 250 238 279 389 letrd 
 |-  ( ch -> ( abs ` ( ( F ` ( A + ( 1 / j ) ) ) - ( F ` z ) ) ) <_ ( x / 2 ) )
391 241 390 eqbrtrd 
 |-  ( ch -> ( abs ` ( ( S ` j ) - ( F ` z ) ) ) <_ ( x / 2 ) )
392 239 391 eqbrtrd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( S ` j ) ) ) <_ ( x / 2 ) )
393 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
394 201 393 syl 
 |-  ( ch -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
395 232 234 238 238 392 394 leltaddd 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) < ( ( x / 2 ) + ( x / 2 ) ) )
396 343 2halvesd 
 |-  ( ch -> ( ( x / 2 ) + ( x / 2 ) ) = x )
397 395 396 breqtrd 
 |-  ( ch -> ( ( abs ` ( ( F ` z ) - ( S ` j ) ) ) + ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) ) < x )
398 230 235 236 237 397 lelttrd 
 |-  ( ch -> ( abs ` ( ( ( F ` z ) - ( S ` j ) ) + ( ( S ` j ) - ( limsup ` S ) ) ) ) < x )
399 224 398 eqbrtrd 
 |-  ( ch -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
400 12 399 sylbir 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
401 400 adantrl 
 |-  ( ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x )
402 401 ex 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) -> ( ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
403 402 ralrimiva 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
404 brimralrspcev 
 |-  ( ( ( 1 / j ) e. RR+ /\ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
405 200 403 404 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
406 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> b <_ N )
407 406 iftrued 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> if ( b <_ N , N , b ) = N )
408 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
409 184 408 syl 
 |-  ( ( ph /\ x e. RR+ ) -> N e. ( ZZ>= ` N ) )
410 409 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> N e. ( ZZ>= ` N ) )
411 407 410 eqeltrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
412 411 adantlr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
413 iffalse 
 |-  ( -. b <_ N -> if ( b <_ N , N , b ) = b )
414 413 adantl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> if ( b <_ N , N , b ) = b )
415 184 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N e. ZZ )
416 simplr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. ZZ )
417 415 zred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N e. RR )
418 416 zred 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. RR )
419 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> -. b <_ N )
420 417 418 ltnled 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> ( N < b <-> -. b <_ N ) )
421 419 420 mpbird 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N < b )
422 417 418 421 ltled 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> N <_ b )
423 eluz2 
 |-  ( b e. ( ZZ>= ` N ) <-> ( N e. ZZ /\ b e. ZZ /\ N <_ b ) )
424 415 416 422 423 syl3anbrc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> b e. ( ZZ>= ` N ) )
425 414 424 eqeltrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ -. b <_ N ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
426 412 425 pm2.61dan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
427 426 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` N ) )
428 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
429 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b e. ZZ )
430 184 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> N e. ZZ )
431 430 429 ifcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ZZ )
432 429 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b e. RR )
433 430 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> N e. RR )
434 max1 
 |-  ( ( b e. RR /\ N e. RR ) -> b <_ if ( b <_ N , N , b ) )
435 432 433 434 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> b <_ if ( b <_ N , N , b ) )
436 eluz2 
 |-  ( if ( b <_ N , N , b ) e. ( ZZ>= ` b ) <-> ( b e. ZZ /\ if ( b <_ N , N , b ) e. ZZ /\ b <_ if ( b <_ N , N , b ) ) )
437 429 431 435 436 syl3anbrc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` b ) )
438 437 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> if ( b <_ N , N , b ) e. ( ZZ>= ` b ) )
439 fveq2 
 |-  ( c = if ( b <_ N , N , b ) -> ( S ` c ) = ( S ` if ( b <_ N , N , b ) ) )
440 439 eleq1d 
 |-  ( c = if ( b <_ N , N , b ) -> ( ( S ` c ) e. CC <-> ( S ` if ( b <_ N , N , b ) ) e. CC ) )
441 439 fvoveq1d 
 |-  ( c = if ( b <_ N , N , b ) -> ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) = ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) )
442 441 breq1d 
 |-  ( c = if ( b <_ N , N , b ) -> ( ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) <-> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
443 440 442 anbi12d 
 |-  ( c = if ( b <_ N , N , b ) -> ( ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) <-> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
444 443 rspccva 
 |-  ( ( A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ if ( b <_ N , N , b ) e. ( ZZ>= ` b ) ) -> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
445 428 438 444 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> ( ( S ` if ( b <_ N , N , b ) ) e. CC /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
446 445 simprd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) )
447 fveq2 
 |-  ( j = if ( b <_ N , N , b ) -> ( S ` j ) = ( S ` if ( b <_ N , N , b ) ) )
448 447 fvoveq1d 
 |-  ( j = if ( b <_ N , N , b ) -> ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) = ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) )
449 448 breq1d 
 |-  ( j = if ( b <_ N , N , b ) -> ( ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) <-> ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
450 449 rspcev 
 |-  ( ( if ( b <_ N , N , b ) e. ( ZZ>= ` N ) /\ ( abs ` ( ( S ` if ( b <_ N , N , b ) ) - ( limsup ` S ) ) ) < ( x / 2 ) ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
451 427 446 450 syl2anc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ b e. ZZ ) /\ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
452 ax-resscn 
 |-  RR C_ CC
453 452 a1i 
 |-  ( ph -> RR C_ CC )
454 4 453 fssd 
 |-  ( ph -> F : ( A (,) B ) --> CC )
455 dvcn 
 |-  ( ( ( RR C_ CC /\ F : ( A (,) B ) --> CC /\ ( A (,) B ) C_ RR ) /\ dom ( RR _D F ) = ( A (,) B ) ) -> F e. ( ( A (,) B ) -cn-> CC ) )
456 453 454 155 5 455 syl31anc 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> CC ) )
457 cncffvrn 
 |-  ( ( RR C_ CC /\ F e. ( ( A (,) B ) -cn-> CC ) ) -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
458 453 456 457 syl2anc 
 |-  ( ph -> ( F e. ( ( A (,) B ) -cn-> RR ) <-> F : ( A (,) B ) --> RR ) )
459 4 458 mpbird 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
460 112 10 fmptd 
 |-  ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
461 eqid 
 |-  ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )
462 climrel 
 |-  Rel ~~>
463 462 a1i 
 |-  ( ph -> Rel ~~> )
464 fvex 
 |-  ( ZZ>= ` M ) e. _V
465 464 mptex 
 |-  ( j e. ( ZZ>= ` M ) |-> A ) e. _V
466 465 a1i 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> A ) e. _V )
467 eqidd 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) |-> A ) = ( j e. ( ZZ>= ` M ) |-> A ) )
468 eqidd 
 |-  ( ( ( ph /\ m e. ( ZZ>= ` M ) ) /\ j = m ) -> A = A )
469 simpr 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> m e. ( ZZ>= ` M ) )
470 1 adantr 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> A e. RR )
471 467 468 469 470 fvmptd 
 |-  ( ( ph /\ m e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> A ) ` m ) = A )
472 31 145 466 105 471 climconst 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> A ) ~~> A )
473 464 mptex 
 |-  ( j e. ( ZZ>= ` M ) |-> ( A + ( 1 / j ) ) ) e. _V
474 10 473 eqeltri 
 |-  R e. _V
475 474 a1i 
 |-  ( ph -> R e. _V )
476 1cnd 
 |-  ( ph -> 1 e. CC )
477 elnnnn0b 
 |-  ( M e. NN <-> ( M e. NN0 /\ 0 < M ) )
478 29 74 477 sylanbrc 
 |-  ( ph -> M e. NN )
479 divcnvg 
 |-  ( ( 1 e. CC /\ M e. NN ) -> ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ~~> 0 )
480 476 478 479 syl2anc 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ~~> 0 )
481 eqidd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) |-> A ) = ( j e. ( ZZ>= ` M ) |-> A ) )
482 eqidd 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` M ) ) /\ j = i ) -> A = A )
483 simpr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. ( ZZ>= ` M ) )
484 1 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A e. RR )
485 481 482 483 484 fvmptd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> A ) ` i ) = A )
486 105 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> A e. CC )
487 485 486 eqeltrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> A ) ` i ) e. CC )
488 eqidd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) = ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) )
489 oveq2 
 |-  ( j = i -> ( 1 / j ) = ( 1 / i ) )
490 489 adantl 
 |-  ( ( ( ph /\ i e. ( ZZ>= ` M ) ) /\ j = i ) -> ( 1 / j ) = ( 1 / i ) )
491 15 483 sselid 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. RR )
492 0red 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 e. RR )
493 69 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M e. RR )
494 74 adantr 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 < M )
495 eluzle 
 |-  ( i e. ( ZZ>= ` M ) -> M <_ i )
496 495 adantl 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> M <_ i )
497 492 493 491 494 496 ltletrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> 0 < i )
498 497 gt0ne0d 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i =/= 0 )
499 491 498 rereccld 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( 1 / i ) e. RR )
500 488 490 483 499 fvmptd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) = ( 1 / i ) )
501 491 recnd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> i e. CC )
502 501 498 reccld 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( 1 / i ) e. CC )
503 500 502 eqeltrd 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) e. CC )
504 489 oveq2d 
 |-  ( j = i -> ( A + ( 1 / j ) ) = ( A + ( 1 / i ) ) )
505 484 499 readdcld 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( A + ( 1 / i ) ) e. RR )
506 10 504 483 505 fvmptd3 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( R ` i ) = ( A + ( 1 / i ) ) )
507 485 500 oveq12d 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( ( ( j e. ( ZZ>= ` M ) |-> A ) ` i ) + ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) ) = ( A + ( 1 / i ) ) )
508 506 507 eqtr4d 
 |-  ( ( ph /\ i e. ( ZZ>= ` M ) ) -> ( R ` i ) = ( ( ( j e. ( ZZ>= ` M ) |-> A ) ` i ) + ( ( j e. ( ZZ>= ` M ) |-> ( 1 / j ) ) ` i ) ) )
509 31 145 472 475 480 487 503 508 climadd 
 |-  ( ph -> R ~~> ( A + 0 ) )
510 105 addid1d 
 |-  ( ph -> ( A + 0 ) = A )
511 509 510 breqtrd 
 |-  ( ph -> R ~~> A )
512 releldm 
 |-  ( ( Rel ~~> /\ R ~~> A ) -> R e. dom ~~> )
513 463 511 512 syl2anc 
 |-  ( ph -> R e. dom ~~> )
514 fveq2 
 |-  ( l = k -> ( ZZ>= ` l ) = ( ZZ>= ` k ) )
515 fveq2 
 |-  ( l = k -> ( R ` l ) = ( R ` k ) )
516 515 oveq2d 
 |-  ( l = k -> ( ( R ` h ) - ( R ` l ) ) = ( ( R ` h ) - ( R ` k ) ) )
517 516 fveq2d 
 |-  ( l = k -> ( abs ` ( ( R ` h ) - ( R ` l ) ) ) = ( abs ` ( ( R ` h ) - ( R ` k ) ) ) )
518 517 breq1d 
 |-  ( l = k -> ( ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
519 514 518 raleqbidv 
 |-  ( l = k -> ( A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
520 519 cbvrabv 
 |-  { l e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
521 fveq2 
 |-  ( h = i -> ( R ` h ) = ( R ` i ) )
522 521 fvoveq1d 
 |-  ( h = i -> ( abs ` ( ( R ` h ) - ( R ` k ) ) ) = ( abs ` ( ( R ` i ) - ( R ` k ) ) ) )
523 522 breq1d 
 |-  ( h = i -> ( ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
524 523 cbvralvw 
 |-  ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
525 524 rgenw 
 |-  A. k e. ( ZZ>= ` M ) ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
526 rabbi 
 |-  ( A. k e. ( ZZ>= ` M ) ( A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) <-> A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) <-> { k e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } )
527 525 526 mpbi 
 |-  { k e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` k ) ( abs ` ( ( R ` h ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
528 520 527 eqtri 
 |-  { l e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } = { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) }
529 528 infeq1i 
 |-  inf ( { l e. ( ZZ>= ` M ) | A. h e. ( ZZ>= ` l ) ( abs ` ( ( R ` h ) - ( R ` l ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < ) = inf ( { k e. ( ZZ>= ` M ) | A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) } , RR , < )
530 1 2 3 459 5 6 30 460 461 513 529 ioodvbdlimc1lem1 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) ~~> ( limsup ` ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) ) )
531 10 fvmpt2 
 |-  ( ( j e. ( ZZ>= ` M ) /\ ( A + ( 1 / j ) ) e. RR ) -> ( R ` j ) = ( A + ( 1 / j ) ) )
532 117 65 531 syl2anc 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( R ` j ) = ( A + ( 1 / j ) ) )
533 532 eqcomd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( A + ( 1 / j ) ) = ( R ` j ) )
534 533 fveq2d 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( A + ( 1 / j ) ) ) = ( F ` ( R ` j ) ) )
535 534 mpteq2dva 
 |-  ( ph -> ( j e. ( ZZ>= ` M ) |-> ( F ` ( A + ( 1 / j ) ) ) ) = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) )
536 9 535 syl5eq 
 |-  ( ph -> S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) )
537 536 fveq2d 
 |-  ( ph -> ( limsup ` S ) = ( limsup ` ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) ) ) )
538 530 536 537 3brtr4d 
 |-  ( ph -> S ~~> ( limsup ` S ) )
539 464 mptex 
 |-  ( j e. ( ZZ>= ` M ) |-> ( F ` ( A + ( 1 / j ) ) ) ) e. _V
540 9 539 eqeltri 
 |-  S e. _V
541 540 a1i 
 |-  ( ph -> S e. _V )
542 eqidd 
 |-  ( ( ph /\ c e. ZZ ) -> ( S ` c ) = ( S ` c ) )
543 541 542 clim 
 |-  ( ph -> ( S ~~> ( limsup ` S ) <-> ( ( limsup ` S ) e. CC /\ A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) ) ) )
544 538 543 mpbid 
 |-  ( ph -> ( ( limsup ` S ) e. CC /\ A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) ) )
545 544 simprd 
 |-  ( ph -> A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) )
546 545 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) )
547 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
548 547 rphalfcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
549 breq2 
 |-  ( a = ( x / 2 ) -> ( ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a <-> ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
550 549 anbi2d 
 |-  ( a = ( x / 2 ) -> ( ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) <-> ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
551 550 rexralbidv 
 |-  ( a = ( x / 2 ) -> ( E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) <-> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) ) )
552 551 rspccva 
 |-  ( ( A. a e. RR+ E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < a ) /\ ( x / 2 ) e. RR+ ) -> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
553 546 548 552 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. b e. ZZ A. c e. ( ZZ>= ` b ) ( ( S ` c ) e. CC /\ ( abs ` ( ( S ` c ) - ( limsup ` S ) ) ) < ( x / 2 ) ) )
554 451 553 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. ( ZZ>= ` N ) ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
555 405 554 r19.29a 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
556 555 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) )
557 ioosscn 
 |-  ( A (,) B ) C_ CC
558 557 a1i 
 |-  ( ph -> ( A (,) B ) C_ CC )
559 454 558 105 ellimc3 
 |-  ( ph -> ( ( limsup ` S ) e. ( F limCC A ) <-> ( ( limsup ` S ) e. CC /\ A. x e. RR+ E. y e. RR+ A. z e. ( A (,) B ) ( ( z =/= A /\ ( abs ` ( z - A ) ) < y ) -> ( abs ` ( ( F ` z ) - ( limsup ` S ) ) ) < x ) ) ) )
560 140 556 559 mpbir2and 
 |-  ( ph -> ( limsup ` S ) e. ( F limCC A ) )