This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ioodvbdlimc1lem1

Description: If F has bounded derivative on ( A (,) B ) then a sequence of points in its image converges to its limsup . (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses ioodvbdlimc1lem1.a 
|- ( ph -> A e. RR )
ioodvbdlimc1lem1.b 
|- ( ph -> B e. RR )
ioodvbdlimc1lem1.altb 
|- ( ph -> A < B )
ioodvbdlimc1lem1.f 
|- ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
ioodvbdlimc1lem1.dmdv 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
ioodvbdlimc1lem1.dvbd 
|- ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
ioodvbdlimc1lem1.m 
|- ( ph -> M e. ZZ )
ioodvbdlimc1lem1.r 
|- ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
ioodvbdlimc1lem1.s 
|- S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )
ioodvbdlimc1lem1.rcnv 
|- ( ph -> R e. dom ~~> )
ioodvbdlimc1lem1.k 
|- K = 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 , < )
Assertion ioodvbdlimc1lem1 
|- ( ph -> S ~~> ( limsup ` S ) )

Proof

Step Hyp Ref Expression
1 ioodvbdlimc1lem1.a 
 |-  ( ph -> A e. RR )
2 ioodvbdlimc1lem1.b 
 |-  ( ph -> B e. RR )
3 ioodvbdlimc1lem1.altb 
 |-  ( ph -> A < B )
4 ioodvbdlimc1lem1.f 
 |-  ( ph -> F e. ( ( A (,) B ) -cn-> RR ) )
5 ioodvbdlimc1lem1.dmdv 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6 ioodvbdlimc1lem1.dvbd 
 |-  ( ph -> E. y e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ y )
7 ioodvbdlimc1lem1.m 
 |-  ( ph -> M e. ZZ )
8 ioodvbdlimc1lem1.r 
 |-  ( ph -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
9 ioodvbdlimc1lem1.s 
 |-  S = ( j e. ( ZZ>= ` M ) |-> ( F ` ( R ` j ) ) )
10 ioodvbdlimc1lem1.rcnv 
 |-  ( ph -> R e. dom ~~> )
11 ioodvbdlimc1lem1.k 
 |-  K = 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 , < )
12 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
13 cncff 
 |-  ( F e. ( ( A (,) B ) -cn-> RR ) -> F : ( A (,) B ) --> RR )
14 4 13 syl 
 |-  ( ph -> F : ( A (,) B ) --> RR )
15 14 adantr 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> F : ( A (,) B ) --> RR )
16 8 ffvelcdmda 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( R ` j ) e. ( A (,) B ) )
17 15 16 ffvelcdmd 
 |-  ( ( ph /\ j e. ( ZZ>= ` M ) ) -> ( F ` ( R ` j ) ) e. RR )
18 17 9 fmptd 
 |-  ( ph -> S : ( ZZ>= ` M ) --> RR )
19 ssrab2 
 |-  { 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 ) ) } C_ ( ZZ>= ` M )
20 rpre 
 |-  ( x e. RR+ -> x e. RR )
21 20 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
22 2fveq3 
 |-  ( z = x -> ( abs ` ( ( RR _D F ) ` z ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
23 22 cbvmptv 
 |-  ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) = ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
24 23 rneqi 
 |-  ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) = ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
25 24 supeq1i 
 |-  sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < )
26 ioomidp 
 |-  ( ( A e. RR /\ B e. RR /\ A < B ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
27 1 2 3 26 syl3anc 
 |-  ( ph -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
28 27 ne0d 
 |-  ( ph -> ( A (,) B ) =/= (/) )
29 ioossre 
 |-  ( A (,) B ) C_ RR
30 29 a1i 
 |-  ( ph -> ( A (,) B ) C_ RR )
31 dvfre 
 |-  ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
32 14 30 31 syl2anc 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
33 5 feq2d 
 |-  ( ph -> ( ( RR _D F ) : dom ( RR _D F ) --> RR <-> ( RR _D F ) : ( A (,) B ) --> RR ) )
34 32 33 mpbid 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> RR )
35 ax-resscn 
 |-  RR C_ CC
36 35 a1i 
 |-  ( ph -> RR C_ CC )
37 34 36 fssd 
 |-  ( ph -> ( RR _D F ) : ( A (,) B ) --> CC )
38 37 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( RR _D F ) ` x ) e. CC )
39 38 abscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` x ) ) e. RR )
40 eqid 
 |-  ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) = ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) )
41 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 , < )
42 28 39 6 40 41 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 , < ) ) )
43 42 simpld 
 |-  ( ph -> sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) e. RR )
44 25 43 eqeltrid 
 |-  ( ph -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
45 44 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
46 peano2re 
 |-  ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
47 45 46 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
48 0red 
 |-  ( ph -> 0 e. RR )
49 1red 
 |-  ( ph -> 1 e. RR )
50 48 49 readdcld 
 |-  ( ph -> ( 0 + 1 ) e. RR )
51 44 46 syl 
 |-  ( ph -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
52 48 ltp1d 
 |-  ( ph -> 0 < ( 0 + 1 ) )
53 37 27 ffvelcdmd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. CC )
54 53 abscld 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) e. RR )
55 53 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
56 42 simprd 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
57 2fveq3 
 |-  ( y = x -> ( abs ` ( ( RR _D F ) ` y ) ) = ( abs ` ( ( RR _D F ) ` x ) ) )
58 25 a1i 
 |-  ( y = x -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) = sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
59 57 58 breq12d 
 |-  ( y = x -> ( ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) ) )
60 59 cbvralvw 
 |-  ( A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) <-> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ sup ( ran ( x e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` x ) ) ) , RR , < ) )
61 56 60 sylibr 
 |-  ( ph -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
62 2fveq3 
 |-  ( y = ( ( A + B ) / 2 ) -> ( abs ` ( ( RR _D F ) ` y ) ) = ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
63 62 breq1d 
 |-  ( y = ( ( A + B ) / 2 ) -> ( ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) <-> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) ) )
64 63 rspcva 
 |-  ( ( ( ( A + B ) / 2 ) e. ( A (,) B ) /\ A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) ) -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
65 27 61 64 syl2anc 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
66 48 54 44 55 65 letrd 
 |-  ( ph -> 0 <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
67 48 44 49 66 leadd1dd 
 |-  ( ph -> ( 0 + 1 ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
68 48 50 51 52 67 ltletrd 
 |-  ( ph -> 0 < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
69 68 gt0ne0d 
 |-  ( ph -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) =/= 0 )
70 69 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) =/= 0 )
71 21 47 70 redivcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR )
72 rpgt0 
 |-  ( x e. RR+ -> 0 < x )
73 72 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> 0 < x )
74 68 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> 0 < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
75 21 47 73 74 divgt0d 
 |-  ( ( ph /\ x e. RR+ ) -> 0 < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
76 71 75 elrpd 
 |-  ( ( ph /\ x e. RR+ ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR+ )
77 7 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> M e. ZZ )
78 10 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> R e. dom ~~> )
79 12 climcau 
 |-  ( ( M e. ZZ /\ R e. dom ~~> ) -> A. w e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w )
80 77 78 79 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> A. w e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w )
81 breq2 
 |-  ( w = ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) -> ( ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w <-> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
82 81 rexralbidv 
 |-  ( w = ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) -> ( E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w <-> E. 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 ) ) ) )
83 82 rspcva 
 |-  ( ( ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR+ /\ A. w e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( R ` k ) ) ) < w ) -> E. 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 ) ) )
84 76 80 83 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. 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 ) ) )
85 rabn0 
 |-  ( { 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 ) ) } =/= (/) <-> E. 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 ) ) )
86 84 85 sylibr 
 |-  ( ( ph /\ x e. RR+ ) -> { 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 ) ) } =/= (/) )
87 infssuzcl 
 |-  ( ( { 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 ) ) } C_ ( ZZ>= ` M ) /\ { 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 ) ) } =/= (/) ) -> 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 , < ) e. { 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 ) ) } )
88 19 86 87 sylancr 
 |-  ( ( ph /\ x e. 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 , < ) e. { 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 ) ) } )
89 11 88 eqeltrid 
 |-  ( ( ph /\ x e. RR+ ) -> K e. { 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 ) ) } )
90 19 89 sselid 
 |-  ( ( ph /\ x e. RR+ ) -> K e. ( ZZ>= ` M ) )
91 2fveq3 
 |-  ( j = i -> ( F ` ( R ` j ) ) = ( F ` ( R ` i ) ) )
92 uzss 
 |-  ( K e. ( ZZ>= ` M ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
93 90 92 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ZZ>= ` K ) C_ ( ZZ>= ` M ) )
94 93 sselda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> i e. ( ZZ>= ` M ) )
95 14 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> F : ( A (,) B ) --> RR )
96 8 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
97 96 94 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. ( A (,) B ) )
98 95 97 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` i ) ) e. RR )
99 9 91 94 98 fvmptd3 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( S ` i ) = ( F ` ( R ` i ) ) )
100 2fveq3 
 |-  ( j = K -> ( F ` ( R ` j ) ) = ( F ` ( R ` K ) ) )
101 90 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> K e. ( ZZ>= ` M ) )
102 96 101 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` K ) e. ( A (,) B ) )
103 95 102 ffvelcdmd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` K ) ) e. RR )
104 9 100 101 103 fvmptd3 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( S ` K ) = ( F ` ( R ` K ) ) )
105 99 104 oveq12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( S ` i ) - ( S ` K ) ) = ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) )
106 105 fveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( S ` i ) - ( S ` K ) ) ) = ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) )
107 98 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` i ) ) e. CC )
108 103 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( F ` ( R ` K ) ) e. CC )
109 107 108 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) e. CC )
110 109 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) e. RR )
111 110 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) e. RR )
112 44 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
113 112 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
114 8 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> R : ( ZZ>= ` M ) --> ( A (,) B ) )
115 114 90 ffvelcdmd 
 |-  ( ( ph /\ x e. RR+ ) -> ( R ` K ) e. ( A (,) B ) )
116 29 115 sselid 
 |-  ( ( ph /\ x e. RR+ ) -> ( R ` K ) e. RR )
117 116 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) e. RR )
118 29 97 sselid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. RR )
119 118 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. RR )
120 117 119 resubcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) e. RR )
121 113 120 remulcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) e. RR )
122 20 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> x e. RR )
123 107 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( F ` ( R ` i ) ) e. CC )
124 108 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( F ` ( R ` K ) ) e. CC )
125 123 124 abssubd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) = ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) )
126 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> A e. RR )
127 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> B e. RR )
128 95 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> F : ( A (,) B ) --> RR )
129 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> dom ( RR _D F ) = ( A (,) B ) )
130 61 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
131 97 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. ( A (,) B ) )
132 118 rexrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. RR* )
133 132 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. RR* )
134 2 rexrd 
 |-  ( ph -> B e. RR* )
135 134 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> B e. RR* )
136 135 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> B e. RR* )
137 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) < ( R ` K ) )
138 1 rexrd 
 |-  ( ph -> A e. RR* )
139 138 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> A e. RR* )
140 134 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> B e. RR* )
141 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( R ` K ) e. ( A (,) B ) ) -> ( R ` K ) < B )
142 139 140 115 141 syl3anc 
 |-  ( ( ph /\ x e. RR+ ) -> ( R ` K ) < B )
143 142 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) < B )
144 133 136 117 137 143 eliood 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) e. ( ( R ` i ) (,) B ) )
145 126 127 128 129 113 130 131 144 dvbdfbdioolem1 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) /\ ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( B - A ) ) ) )
146 145 simpld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` K ) ) - ( F ` ( R ` i ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) )
147 125 146 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) )
148 113 46 syl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
149 148 120 remulcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) e. RR )
150 119 117 posdifd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` i ) < ( R ` K ) <-> 0 < ( ( R ` K ) - ( R ` i ) ) ) )
151 137 150 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> 0 < ( ( R ` K ) - ( R ` i ) ) )
152 120 151 elrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) e. RR+ )
153 113 ltp1d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
154 113 148 152 153 ltmul1dd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) < ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) )
155 29 102 sselid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` K ) e. RR )
156 118 155 resubcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( R ` i ) - ( R ` K ) ) e. RR )
157 156 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( R ` i ) - ( R ` K ) ) e. CC )
158 157 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) e. RR )
159 158 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) e. RR )
160 71 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR )
161 120 leabsd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) <_ ( abs ` ( ( R ` K ) - ( R ` i ) ) ) )
162 117 recnd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` K ) e. CC )
163 118 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) e. CC )
164 163 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( R ` i ) e. CC )
165 162 164 abssubd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( R ` K ) - ( R ` i ) ) ) = ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
166 161 165 breqtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) <_ ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
167 fveq2 
 |-  ( k = K -> ( ZZ>= ` k ) = ( ZZ>= ` K ) )
168 fveq2 
 |-  ( k = K -> ( R ` k ) = ( R ` K ) )
169 168 oveq2d 
 |-  ( k = K -> ( ( R ` i ) - ( R ` k ) ) = ( ( R ` i ) - ( R ` K ) ) )
170 169 fveq2d 
 |-  ( k = K -> ( abs ` ( ( R ` i ) - ( R ` k ) ) ) = ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
171 170 breq1d 
 |-  ( k = K -> ( ( abs ` ( ( R ` i ) - ( 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 ) ) ) )
172 167 171 raleqbidv 
 |-  ( k = K -> ( A. i e. ( ZZ>= ` k ) ( abs ` ( ( R ` i ) - ( 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 ) ) ) )
173 172 elrab 
 |-  ( K e. { 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 ) ) } <-> ( 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 ) ) ) )
174 89 173 sylib 
 |-  ( ( ph /\ x e. RR+ ) -> ( 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 ) ) ) )
175 174 simprd 
 |-  ( ( ph /\ x e. RR+ ) -> A. i e. ( ZZ>= ` K ) ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
176 175 r19.21bi 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
177 176 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
178 120 159 160 166 177 lelttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( R ` K ) - ( R ` i ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
179 51 68 elrpd 
 |-  ( ph -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR+ )
180 179 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR+ )
181 120 122 180 ltmuldiv2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) < x <-> ( ( R ` K ) - ( R ` i ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
182 178 181 mpbird 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` K ) - ( R ` i ) ) ) < x )
183 121 149 122 154 182 lttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` K ) - ( R ` i ) ) ) < x )
184 111 121 122 147 183 lelttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
185 fveq2 
 |-  ( ( R ` i ) = ( R ` K ) -> ( F ` ( R ` i ) ) = ( F ` ( R ` K ) ) )
186 185 oveq1d 
 |-  ( ( R ` i ) = ( R ` K ) -> ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) = ( ( F ` ( R ` K ) ) - ( F ` ( R ` K ) ) ) )
187 108 subidd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( ( F ` ( R ` K ) ) - ( F ` ( R ` K ) ) ) = 0 )
188 186 187 sylan9eqr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) = 0 )
189 188 abs00bd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) = 0 )
190 72 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> 0 < x )
191 189 190 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
192 191 adantlr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
193 simpll 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) )
194 155 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` K ) e. RR )
195 118 ad2antrr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` i ) e. RR )
196 id 
 |-  ( ( R ` K ) = ( R ` i ) -> ( R ` K ) = ( R ` i ) )
197 196 eqcomd 
 |-  ( ( R ` K ) = ( R ` i ) -> ( R ` i ) = ( R ` K ) )
198 197 necon3bi 
 |-  ( -. ( R ` i ) = ( R ` K ) -> ( R ` K ) =/= ( R ` i ) )
199 198 adantl 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` K ) =/= ( R ` i ) )
200 simplr 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> -. ( R ` i ) < ( R ` K ) )
201 194 195 199 200 lttri5d 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( R ` K ) < ( R ` i ) )
202 110 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) e. RR )
203 112 156 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) e. RR )
204 203 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) e. RR )
205 20 ad3antlr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> x e. RR )
206 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> A e. RR )
207 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> B e. RR )
208 95 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> F : ( A (,) B ) --> RR )
209 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> dom ( RR _D F ) = ( A (,) B ) )
210 44 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) e. RR )
211 61 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) )
212 102 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) e. ( A (,) B ) )
213 116 rexrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( R ` K ) e. RR* )
214 213 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) e. RR* )
215 207 rexrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> B e. RR* )
216 118 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` i ) e. RR )
217 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) < ( R ` i ) )
218 138 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> A e. RR* )
219 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( R ` i ) e. ( A (,) B ) ) -> ( R ` i ) < B )
220 218 135 97 219 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( R ` i ) < B )
221 220 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` i ) < B )
222 214 215 216 217 221 eliood 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` i ) e. ( ( R ` K ) (,) B ) )
223 206 207 208 209 210 211 212 222 dvbdfbdioolem1 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) /\ ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( B - A ) ) ) )
224 223 simpld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) <_ ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) )
225 1red 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> 1 e. RR )
226 210 225 readdcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
227 155 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( R ` K ) e. RR )
228 216 227 resubcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) e. RR )
229 226 228 remulcld 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) e. RR )
230 210 46 syl 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR )
231 227 216 posdifd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` K ) < ( R ` i ) <-> 0 < ( ( R ` i ) - ( R ` K ) ) ) )
232 217 231 mpbid 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> 0 < ( ( R ` i ) - ( R ` K ) ) )
233 228 232 elrpd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) e. RR+ )
234 210 ltp1d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) < ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) )
235 210 230 233 234 ltmul1dd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) < ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) )
236 158 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) e. RR )
237 71 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) e. RR )
238 228 leabsd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) <_ ( abs ` ( ( R ` i ) - ( R ` K ) ) ) )
239 176 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( R ` i ) - ( R ` K ) ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
240 228 236 237 238 239 lelttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( R ` i ) - ( R ` K ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) )
241 179 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) e. RR+ )
242 228 205 241 ltmuldiv2d 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) < x <-> ( ( R ` i ) - ( R ` K ) ) < ( x / ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) ) ) )
243 240 242 mpbird 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) + 1 ) x. ( ( R ` i ) - ( R ` K ) ) ) < x )
244 204 229 205 235 243 lttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( sup ( ran ( z e. ( A (,) B ) |-> ( abs ` ( ( RR _D F ) ` z ) ) ) , RR , < ) x. ( ( R ` i ) - ( R ` K ) ) ) < x )
245 202 204 205 224 244 lelttrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ ( R ` K ) < ( R ` i ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
246 193 201 245 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) /\ -. ( R ` i ) = ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
247 192 246 pm2.61dan 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) /\ -. ( R ` i ) < ( R ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
248 184 247 pm2.61dan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( F ` ( R ` i ) ) - ( F ` ( R ` K ) ) ) ) < x )
249 106 248 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ i e. ( ZZ>= ` K ) ) -> ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x )
250 249 ralrimiva 
 |-  ( ( ph /\ x e. RR+ ) -> A. i e. ( ZZ>= ` K ) ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x )
251 fveq2 
 |-  ( k = K -> ( S ` k ) = ( S ` K ) )
252 251 oveq2d 
 |-  ( k = K -> ( ( S ` i ) - ( S ` k ) ) = ( ( S ` i ) - ( S ` K ) ) )
253 252 fveq2d 
 |-  ( k = K -> ( abs ` ( ( S ` i ) - ( S ` k ) ) ) = ( abs ` ( ( S ` i ) - ( S ` K ) ) ) )
254 253 breq1d 
 |-  ( k = K -> ( ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x <-> ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x ) )
255 167 254 raleqbidv 
 |-  ( k = K -> ( A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x <-> A. i e. ( ZZ>= ` K ) ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x ) )
256 255 rspcev 
 |-  ( ( K e. ( ZZ>= ` M ) /\ A. i e. ( ZZ>= ` K ) ( abs ` ( ( S ` i ) - ( S ` K ) ) ) < x ) -> E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x )
257 90 250 256 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x )
258 257 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. k e. ( ZZ>= ` M ) A. i e. ( ZZ>= ` k ) ( abs ` ( ( S ` i ) - ( S ` k ) ) ) < x )
259 12 18 258 caurcvg 
 |-  ( ph -> S ~~> ( limsup ` S ) )