Metamath Proof Explorer

Theorem caucvgrlem2

Description: Lemma for caucvgr . (Contributed by NM, 4-Apr-2005) (Proof shortened by Mario Carneiro, 8-May-2016)

Ref Expression
Hypotheses caucvgr.1 
|- ( ph -> A C_ RR )
caucvgr.2 
|- ( ph -> F : A --> CC )
caucvgr.3 
|- ( ph -> sup ( A , RR* , < ) = +oo )
caucvgr.4 
|- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
caucvgrlem2.5 
|- H : CC --> RR
caucvgrlem2.6 
|- ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
Assertion caucvgrlem2 
|- ( ph -> ( n e. A |-> ( H ` ( F ` n ) ) ) ~~>r ( ~~>r ` ( H o. F ) ) )

Proof

Step Hyp Ref Expression
1 caucvgr.1 
 |-  ( ph -> A C_ RR )
2 caucvgr.2 
 |-  ( ph -> F : A --> CC )
3 caucvgr.3 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
4 caucvgr.4 
 |-  ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
5 caucvgrlem2.5 
 |-  H : CC --> RR
6 caucvgrlem2.6 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
7 fcompt 
 |-  ( ( H : CC --> RR /\ F : A --> CC ) -> ( H o. F ) = ( n e. A |-> ( H ` ( F ` n ) ) ) )
8 5 2 7 sylancr 
 |-  ( ph -> ( H o. F ) = ( n e. A |-> ( H ` ( F ` n ) ) ) )
9 fco 
 |-  ( ( H : CC --> RR /\ F : A --> CC ) -> ( H o. F ) : A --> RR )
10 5 2 9 sylancr 
 |-  ( ph -> ( H o. F ) : A --> RR )
11 2 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> F : A --> CC )
12 simprr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> k e. A )
13 11 12 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( F ` k ) e. CC )
14 simprl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> j e. A )
15 11 14 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( F ` j ) e. CC )
16 13 15 6 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
17 5 ffvelrni 
 |-  ( ( F ` k ) e. CC -> ( H ` ( F ` k ) ) e. RR )
18 13 17 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( H ` ( F ` k ) ) e. RR )
19 5 ffvelrni 
 |-  ( ( F ` j ) e. CC -> ( H ` ( F ` j ) ) e. RR )
20 15 19 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( H ` ( F ` j ) ) e. RR )
21 18 20 resubcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) e. RR )
22 21 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) e. CC )
23 22 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) e. RR )
24 13 15 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( F ` k ) - ( F ` j ) ) e. CC )
25 24 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) e. RR )
26 rpre 
 |-  ( x e. RR+ -> x e. RR )
27 26 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> x e. RR )
28 lelttr 
 |-  ( ( ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) e. RR /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) e. RR /\ x e. RR ) -> ( ( ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) < x ) )
29 23 25 27 28 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) < x ) )
30 16 29 mpand 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) < x ) )
31 fvco3 
 |-  ( ( F : A --> CC /\ k e. A ) -> ( ( H o. F ) ` k ) = ( H ` ( F ` k ) ) )
32 11 12 31 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( H o. F ) ` k ) = ( H ` ( F ` k ) ) )
33 fvco3 
 |-  ( ( F : A --> CC /\ j e. A ) -> ( ( H o. F ) ` j ) = ( H ` ( F ` j ) ) )
34 11 14 33 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( H o. F ) ` j ) = ( H ` ( F ` j ) ) )
35 32 34 oveq12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) = ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) )
36 35 fveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) = ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) )
37 36 breq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x <-> ( abs ` ( ( H ` ( F ` k ) ) - ( H ` ( F ` j ) ) ) ) < x ) )
38 30 37 sylibrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) )
39 38 imim2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ ( j e. A /\ k e. A ) ) -> ( ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( j <_ k -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) ) )
40 39 anassrs 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ j e. A ) /\ k e. A ) -> ( ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( j <_ k -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) ) )
41 40 ralimdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ j e. A ) -> ( A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. k e. A ( j <_ k -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) ) )
42 41 reximdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( 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 ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) ) )
43 42 ralimdva 
 |-  ( ph -> ( A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) ) )
44 4 43 mpd 
 |-  ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( ( H o. F ) ` k ) - ( ( H o. F ) ` j ) ) ) < x ) )
45 1 10 3 44 caurcvgr 
 |-  ( ph -> ( H o. F ) ~~>r ( limsup ` ( H o. F ) ) )
46 rlimrel 
 |-  Rel ~~>r
47 46 releldmi 
 |-  ( ( H o. F ) ~~>r ( limsup ` ( H o. F ) ) -> ( H o. F ) e. dom ~~>r )
48 45 47 syl 
 |-  ( ph -> ( H o. F ) e. dom ~~>r )
49 ax-resscn 
 |-  RR C_ CC
50 fss 
 |-  ( ( ( H o. F ) : A --> RR /\ RR C_ CC ) -> ( H o. F ) : A --> CC )
51 10 49 50 sylancl 
 |-  ( ph -> ( H o. F ) : A --> CC )
52 51 3 rlimdm 
 |-  ( ph -> ( ( H o. F ) e. dom ~~>r <-> ( H o. F ) ~~>r ( ~~>r ` ( H o. F ) ) ) )
53 48 52 mpbid 
 |-  ( ph -> ( H o. F ) ~~>r ( ~~>r ` ( H o. F ) ) )
54 8 53 eqbrtrrd 
 |-  ( ph -> ( n e. A |-> ( H ` ( F ` n ) ) ) ~~>r ( ~~>r ` ( H o. F ) ) )