Metamath Proof Explorer


Theorem ioodvbdlimc2lem

Description: Limit at the upper 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 ioodvbdlimc2lem.a
|- ( ph -> A e. RR )
ioodvbdlimc2lem.b
|- ( ph -> B e. RR )
ioodvbdlimc2lem.altb
|- ( ph -> A < B )
ioodvbdlimc2lem.f
|- ( ph -> F : ( A (,) B ) --> RR )
ioodvbdlimc2lem.dmdv
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
ioodvbdlimc2lem.dvbd
|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
ioodvbdlimc2lem.y
|- Y = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
ioodvbdlimc2lem.m
|- M = ( ( |_ ` ( 1 / ( B - A ) ) ) + 1 )
ioodvbdlimc2lem.s
|- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( B - ( 1 / j ) ) ) )
ioodvbdlimc2lem.r
|- R = ( j e. ( ZZ>= ` M ) |-> ( B - ( 1 / j ) ) )
ioodvbdlimc2lem.n
|- N = if ( M <_ ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , ( ( |_ ` ( Y / ( x / 2 ) ) ) + 1 ) , M )
ioodvbdlimc2lem.ch
|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ ) /\ j e. ( ZZ>= ` N ) ) /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) ) /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - B ) ) < ( 1 / j ) ) )
Assertion ioodvbdlimc2lem
|- ( ph -> ( limsup ` S ) e. ( F limCC B ) )

Proof

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