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 φA
caucvgr.2 φF:A
caucvgr.3 φsupA*<=+∞
caucvgr.4 φx+jAkAjkFkFj<x
caucvgrlem2.5 H:
caucvgrlem2.6 FkFjHFkHFjFkFj
Assertion caucvgrlem2 φnAHFnHF

Proof

Step Hyp Ref Expression
1 caucvgr.1 φA
2 caucvgr.2 φF:A
3 caucvgr.3 φsupA*<=+∞
4 caucvgr.4 φx+jAkAjkFkFj<x
5 caucvgrlem2.5 H:
6 caucvgrlem2.6 FkFjHFkHFjFkFj
7 fcompt H:F:AHF=nAHFn
8 5 2 7 sylancr φHF=nAHFn
9 fco H:F:AHF:A
10 5 2 9 sylancr φHF:A
11 2 ad2antrr φx+jAkAF:A
12 simprr φx+jAkAkA
13 11 12 ffvelrnd φx+jAkAFk
14 simprl φx+jAkAjA
15 11 14 ffvelrnd φx+jAkAFj
16 13 15 6 syl2anc φx+jAkAHFkHFjFkFj
17 5 ffvelrni FkHFk
18 13 17 syl φx+jAkAHFk
19 5 ffvelrni FjHFj
20 15 19 syl φx+jAkAHFj
21 18 20 resubcld φx+jAkAHFkHFj
22 21 recnd φx+jAkAHFkHFj
23 22 abscld φx+jAkAHFkHFj
24 13 15 subcld φx+jAkAFkFj
25 24 abscld φx+jAkAFkFj
26 rpre x+x
27 26 ad2antlr φx+jAkAx
28 lelttr HFkHFjFkFjxHFkHFjFkFjFkFj<xHFkHFj<x
29 23 25 27 28 syl3anc φx+jAkAHFkHFjFkFjFkFj<xHFkHFj<x
30 16 29 mpand φx+jAkAFkFj<xHFkHFj<x
31 fvco3 F:AkAHFk=HFk
32 11 12 31 syl2anc φx+jAkAHFk=HFk
33 fvco3 F:AjAHFj=HFj
34 11 14 33 syl2anc φx+jAkAHFj=HFj
35 32 34 oveq12d φx+jAkAHFkHFj=HFkHFj
36 35 fveq2d φx+jAkAHFkHFj=HFkHFj
37 36 breq1d φx+jAkAHFkHFj<xHFkHFj<x
38 30 37 sylibrd φx+jAkAFkFj<xHFkHFj<x
39 38 imim2d φx+jAkAjkFkFj<xjkHFkHFj<x
40 39 anassrs φx+jAkAjkFkFj<xjkHFkHFj<x
41 40 ralimdva φx+jAkAjkFkFj<xkAjkHFkHFj<x
42 41 reximdva φx+jAkAjkFkFj<xjAkAjkHFkHFj<x
43 42 ralimdva φx+jAkAjkFkFj<xx+jAkAjkHFkHFj<x
44 4 43 mpd φx+jAkAjkHFkHFj<x
45 1 10 3 44 caurcvgr φHFlim supHF
46 rlimrel Rel
47 46 releldmi HFlim supHFHFdom
48 45 47 syl φHFdom
49 ax-resscn
50 fss HF:AHF:A
51 10 49 50 sylancl φHF:A
52 51 3 rlimdm φHFdomHFHF
53 48 52 mpbid φHFHF
54 8 53 eqbrtrrd φnAHFnHF