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 ) ) ) )