Metamath Proof Explorer

Theorem caucvgrlem

Description: Lemma for caurcvgr . (Contributed by Mario Carneiro, 15-Feb-2014) (Revised by AV, 12-Sep-2020)

Ref Expression
Hypotheses caurcvgr.1 
|- ( ph -> A C_ RR )
caurcvgr.2 
|- ( ph -> F : A --> RR )
caurcvgr.3 
|- ( ph -> sup ( A , RR* , < ) = +oo )
caurcvgr.4 
|- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
caucvgrlem.4 
|- ( ph -> R e. RR+ )
Assertion caucvgrlem 
|- ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )

Proof

Step Hyp Ref Expression
1 caurcvgr.1 
 |-  ( ph -> A C_ RR )
2 caurcvgr.2 
 |-  ( ph -> F : A --> RR )
3 caurcvgr.3 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
4 caurcvgr.4 
 |-  ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
5 caucvgrlem.4 
 |-  ( ph -> R e. RR+ )
6 reex 
 |-  RR e. _V
7 6 ssex 
 |-  ( A C_ RR -> A e. _V )
8 1 7 syl 
 |-  ( ph -> A e. _V )
9 6 a1i 
 |-  ( ph -> RR e. _V )
10 fex2 
 |-  ( ( F : A --> RR /\ A e. _V /\ RR e. _V ) -> F e. _V )
11 2 8 9 10 syl3anc 
 |-  ( ph -> F e. _V )
12 limsupcl 
 |-  ( F e. _V -> ( limsup ` F ) e. RR* )
13 11 12 syl 
 |-  ( ph -> ( limsup ` F ) e. RR* )
14 13 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( limsup ` F ) e. RR* )
15 2 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> F : A --> RR )
16 simprl 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> j e. A )
17 15 16 ffvelrnd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( F ` j ) e. RR )
18 5 rpred 
 |-  ( ph -> R e. RR )
19 18 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> R e. RR )
20 17 19 readdcld 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( ( F ` j ) + R ) e. RR )
21 mnfxr 
 |-  -oo e. RR*
22 21 a1i 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> -oo e. RR* )
23 17 19 resubcld 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( ( F ` j ) - R ) e. RR )
24 23 rexrd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( ( F ` j ) - R ) e. RR* )
25 23 mnfltd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> -oo < ( ( F ` j ) - R ) )
26 1 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A C_ RR )
27 ressxr 
 |-  RR C_ RR*
28 fss 
 |-  ( ( F : A --> RR /\ RR C_ RR* ) -> F : A --> RR* )
29 2 27 28 sylancl 
 |-  ( ph -> F : A --> RR* )
30 29 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> F : A --> RR* )
31 3 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> sup ( A , RR* , < ) = +oo )
32 26 16 sseldd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> j e. RR )
33 simprr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) )
34 breq2 
 |-  ( k = m -> ( j <_ k <-> j <_ m ) )
35 34 imbrov2fvoveq 
 |-  ( k = m -> ( ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) <-> ( j <_ m -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R ) ) )
36 35 cbvralvw 
 |-  ( A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) <-> A. m e. A ( j <_ m -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R ) )
37 33 36 sylib 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A. m e. A ( j <_ m -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R ) )
38 15 ffvelrnda 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( F ` m ) e. RR )
39 17 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( F ` j ) e. RR )
40 38 39 resubcld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( F ` m ) - ( F ` j ) ) e. RR )
41 40 recnd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( F ` m ) - ( F ` j ) ) e. CC )
42 41 abscld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) e. RR )
43 19 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> R e. RR )
44 ltle 
 |-  ( ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) e. RR /\ R e. RR ) -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) <_ R ) )
45 42 43 44 syl2anc 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) <_ R ) )
46 38 39 43 absdifled 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) <_ R <-> ( ( ( F ` j ) - R ) <_ ( F ` m ) /\ ( F ` m ) <_ ( ( F ` j ) + R ) ) ) )
47 45 46 sylibd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R -> ( ( ( F ` j ) - R ) <_ ( F ` m ) /\ ( F ` m ) <_ ( ( F ` j ) + R ) ) ) )
48 simpl 
 |-  ( ( ( ( F ` j ) - R ) <_ ( F ` m ) /\ ( F ` m ) <_ ( ( F ` j ) + R ) ) -> ( ( F ` j ) - R ) <_ ( F ` m ) )
49 47 48 syl6 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R -> ( ( F ` j ) - R ) <_ ( F ` m ) ) )
50 49 imim2d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( ( j <_ m -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R ) -> ( j <_ m -> ( ( F ` j ) - R ) <_ ( F ` m ) ) ) )
51 50 ralimdva 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( A. m e. A ( j <_ m -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R ) -> A. m e. A ( j <_ m -> ( ( F ` j ) - R ) <_ ( F ` m ) ) ) )
52 37 51 mpd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A. m e. A ( j <_ m -> ( ( F ` j ) - R ) <_ ( F ` m ) ) )
53 breq1 
 |-  ( n = j -> ( n <_ m <-> j <_ m ) )
54 53 rspceaimv 
 |-  ( ( j e. RR /\ A. m e. A ( j <_ m -> ( ( F ` j ) - R ) <_ ( F ` m ) ) ) -> E. n e. RR A. m e. A ( n <_ m -> ( ( F ` j ) - R ) <_ ( F ` m ) ) )
55 32 52 54 syl2anc 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> E. n e. RR A. m e. A ( n <_ m -> ( ( F ` j ) - R ) <_ ( F ` m ) ) )
56 26 30 24 31 55 limsupbnd2 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( ( F ` j ) - R ) <_ ( limsup ` F ) )
57 22 24 14 25 56 xrltletrd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> -oo < ( limsup ` F ) )
58 20 rexrd 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( ( F ` j ) + R ) e. RR* )
59 42 adantrr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) e. RR )
60 19 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> R e. RR )
61 simprr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> j <_ m )
62 simplrr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) )
63 simprl 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> m e. A )
64 35 62 63 rspcdva 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( j <_ m -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R ) )
65 61 64 mpd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < R )
66 59 60 65 ltled 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) <_ R )
67 38 adantrr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( F ` m ) e. RR )
68 17 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( F ` j ) e. RR )
69 67 68 60 absdifled 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) <_ R <-> ( ( ( F ` j ) - R ) <_ ( F ` m ) /\ ( F ` m ) <_ ( ( F ` j ) + R ) ) ) )
70 66 69 mpbid 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` j ) - R ) <_ ( F ` m ) /\ ( F ` m ) <_ ( ( F ` j ) + R ) ) )
71 70 simprd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( F ` m ) <_ ( ( F ` j ) + R ) )
72 71 expr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( j <_ m -> ( F ` m ) <_ ( ( F ` j ) + R ) ) )
73 72 ralrimiva 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A. m e. A ( j <_ m -> ( F ` m ) <_ ( ( F ` j ) + R ) ) )
74 53 rspceaimv 
 |-  ( ( j e. RR /\ A. m e. A ( j <_ m -> ( F ` m ) <_ ( ( F ` j ) + R ) ) ) -> E. n e. RR A. m e. A ( n <_ m -> ( F ` m ) <_ ( ( F ` j ) + R ) ) )
75 32 73 74 syl2anc 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> E. n e. RR A. m e. A ( n <_ m -> ( F ` m ) <_ ( ( F ` j ) + R ) ) )
76 26 30 58 75 limsupbnd1 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( limsup ` F ) <_ ( ( F ` j ) + R ) )
77 xrre 
 |-  ( ( ( ( limsup ` F ) e. RR* /\ ( ( F ` j ) + R ) e. RR ) /\ ( -oo < ( limsup ` F ) /\ ( limsup ` F ) <_ ( ( F ` j ) + R ) ) ) -> ( limsup ` F ) e. RR )
78 14 20 57 76 77 syl22anc 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( limsup ` F ) e. RR )
79 78 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( limsup ` F ) e. RR )
80 67 79 resubcld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( limsup ` F ) ) e. RR )
81 80 recnd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( limsup ` F ) ) e. CC )
82 81 abscld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) e. RR )
83 2re 
 |-  2 e. RR
84 remulcl 
 |-  ( ( 2 e. RR /\ R e. RR ) -> ( 2 x. R ) e. RR )
85 83 60 84 sylancr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( 2 x. R ) e. RR )
86 3re 
 |-  3 e. RR
87 remulcl 
 |-  ( ( 3 e. RR /\ R e. RR ) -> ( 3 x. R ) e. RR )
88 86 60 87 sylancr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( 3 x. R ) e. RR )
89 67 recnd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( F ` m ) e. CC )
90 79 recnd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( limsup ` F ) e. CC )
91 89 90 abssubd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) = ( abs ` ( ( limsup ` F ) - ( F ` m ) ) ) )
92 67 85 resubcld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( 2 x. R ) ) e. RR )
93 23 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` j ) - R ) e. RR )
94 60 recnd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> R e. CC )
95 94 2timesd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( 2 x. R ) = ( R + R ) )
96 95 oveq2d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( 2 x. R ) ) = ( ( F ` m ) - ( R + R ) ) )
97 89 94 94 subsub4d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` m ) - R ) - R ) = ( ( F ` m ) - ( R + R ) ) )
98 96 97 eqtr4d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( 2 x. R ) ) = ( ( ( F ` m ) - R ) - R ) )
99 67 60 resubcld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - R ) e. RR )
100 67 60 68 lesubaddd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` m ) - R ) <_ ( F ` j ) <-> ( F ` m ) <_ ( ( F ` j ) + R ) ) )
101 71 100 mpbird 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - R ) <_ ( F ` j ) )
102 99 68 60 101 lesub1dd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` m ) - R ) - R ) <_ ( ( F ` j ) - R ) )
103 98 102 eqbrtrd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( 2 x. R ) ) <_ ( ( F ` j ) - R ) )
104 56 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` j ) - R ) <_ ( limsup ` F ) )
105 92 93 79 103 104 letrd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) - ( 2 x. R ) ) <_ ( limsup ` F ) )
106 20 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` j ) + R ) e. RR )
107 67 85 readdcld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) + ( 2 x. R ) ) e. RR )
108 76 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( limsup ` F ) <_ ( ( F ` j ) + R ) )
109 67 60 readdcld 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) + R ) e. RR )
110 70 48 syl 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` j ) - R ) <_ ( F ` m ) )
111 68 60 67 lesubaddd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` j ) - R ) <_ ( F ` m ) <-> ( F ` j ) <_ ( ( F ` m ) + R ) ) )
112 110 111 mpbid 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( F ` j ) <_ ( ( F ` m ) + R ) )
113 68 109 60 112 leadd1dd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` j ) + R ) <_ ( ( ( F ` m ) + R ) + R ) )
114 89 94 94 addassd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` m ) + R ) + R ) = ( ( F ` m ) + ( R + R ) ) )
115 95 oveq2d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` m ) + ( 2 x. R ) ) = ( ( F ` m ) + ( R + R ) ) )
116 114 115 eqtr4d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( ( F ` m ) + R ) + R ) = ( ( F ` m ) + ( 2 x. R ) ) )
117 113 116 breqtrd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( F ` j ) + R ) <_ ( ( F ` m ) + ( 2 x. R ) ) )
118 79 106 107 108 117 letrd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( limsup ` F ) <_ ( ( F ` m ) + ( 2 x. R ) ) )
119 79 67 85 absdifled 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( ( abs ` ( ( limsup ` F ) - ( F ` m ) ) ) <_ ( 2 x. R ) <-> ( ( ( F ` m ) - ( 2 x. R ) ) <_ ( limsup ` F ) /\ ( limsup ` F ) <_ ( ( F ` m ) + ( 2 x. R ) ) ) ) )
120 105 118 119 mpbir2and 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( limsup ` F ) - ( F ` m ) ) ) <_ ( 2 x. R ) )
121 91 120 eqbrtrd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) <_ ( 2 x. R ) )
122 2lt3 
 |-  2 < 3
123 83 a1i 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> 2 e. RR )
124 86 a1i 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> 3 e. RR )
125 5 adantr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> R e. RR+ )
126 125 adantr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> R e. RR+ )
127 123 124 126 ltmul1d 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( 2 < 3 <-> ( 2 x. R ) < ( 3 x. R ) ) )
128 122 127 mpbii 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( 2 x. R ) < ( 3 x. R ) )
129 82 85 88 121 128 lelttrd 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ ( m e. A /\ j <_ m ) ) -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) < ( 3 x. R ) )
130 129 expr 
 |-  ( ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) /\ m e. A ) -> ( j <_ m -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) )
131 130 ralrimiva 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A. m e. A ( j <_ m -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) )
132 34 imbrov2fvoveq 
 |-  ( k = m -> ( ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) <-> ( j <_ m -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )
133 132 cbvralvw 
 |-  ( A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) <-> A. m e. A ( j <_ m -> ( abs ` ( ( F ` m ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) )
134 131 133 sylibr 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) )
135 78 134 jca 
 |-  ( ( ph /\ ( j e. A /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) ) -> ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )
136 breq2 
 |-  ( x = R -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) )
137 136 imbi2d 
 |-  ( x = R -> ( ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) )
138 137 rexralbidv 
 |-  ( x = R -> ( E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) ) )
139 138 4 5 rspcdva 
 |-  ( ph -> E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < R ) )
140 135 139 reximddv 
 |-  ( ph -> E. j e. A ( ( limsup ` F ) e. RR /\ A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( limsup ` F ) ) ) < ( 3 x. R ) ) ) )