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 ( 𝜑𝐴 ⊆ ℝ )
caucvgr.2 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
caucvgr.3 ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
caucvgr.4 ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
caucvgrlem2.5 𝐻 : ℂ ⟶ ℝ
caucvgrlem2.6 ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( 𝐹𝑗 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) )
Assertion caucvgrlem2 ( 𝜑 → ( 𝑛𝐴 ↦ ( 𝐻 ‘ ( 𝐹𝑛 ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝐻𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 caucvgr.1 ( 𝜑𝐴 ⊆ ℝ )
2 caucvgr.2 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
3 caucvgr.3 ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
4 caucvgr.4 ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) )
5 caucvgrlem2.5 𝐻 : ℂ ⟶ ℝ
6 caucvgrlem2.6 ( ( ( 𝐹𝑘 ) ∈ ℂ ∧ ( 𝐹𝑗 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) )
7 fcompt ( ( 𝐻 : ℂ ⟶ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐻𝐹 ) = ( 𝑛𝐴 ↦ ( 𝐻 ‘ ( 𝐹𝑛 ) ) ) )
8 5 2 7 sylancr ( 𝜑 → ( 𝐻𝐹 ) = ( 𝑛𝐴 ↦ ( 𝐻 ‘ ( 𝐹𝑛 ) ) ) )
9 fco ( ( 𝐻 : ℂ ⟶ ℝ ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐻𝐹 ) : 𝐴 ⟶ ℝ )
10 5 2 9 sylancr ( 𝜑 → ( 𝐻𝐹 ) : 𝐴 ⟶ ℝ )
11 2 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
12 simprr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → 𝑘𝐴 )
13 11 12 ffvelrnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
14 simprl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → 𝑗𝐴 )
15 11 14 ffvelrnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( 𝐹𝑗 ) ∈ ℂ )
16 13 15 6 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) )
17 5 ffvelrni ( ( 𝐹𝑘 ) ∈ ℂ → ( 𝐻 ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
18 13 17 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( 𝐻 ‘ ( 𝐹𝑘 ) ) ∈ ℝ )
19 5 ffvelrni ( ( 𝐹𝑗 ) ∈ ℂ → ( 𝐻 ‘ ( 𝐹𝑗 ) ) ∈ ℝ )
20 15 19 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( 𝐻 ‘ ( 𝐹𝑗 ) ) ∈ ℝ )
21 18 20 resubcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ∈ ℝ )
22 21 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ∈ ℂ )
23 22 abscld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ∈ ℝ )
24 13 15 subcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ∈ ℂ )
25 24 abscld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) ∈ ℝ )
26 rpre ( 𝑥 ∈ ℝ+𝑥 ∈ ℝ )
27 26 ad2antlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → 𝑥 ∈ ℝ )
28 lelttr ( ( ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ∈ ℝ ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) < 𝑥 ) )
29 23 25 27 28 syl3anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) ≤ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) ∧ ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) < 𝑥 ) )
30 16 29 mpand ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 → ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) < 𝑥 ) )
31 fvco3 ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑘𝐴 ) → ( ( 𝐻𝐹 ) ‘ 𝑘 ) = ( 𝐻 ‘ ( 𝐹𝑘 ) ) )
32 11 12 31 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( 𝐻𝐹 ) ‘ 𝑘 ) = ( 𝐻 ‘ ( 𝐹𝑘 ) ) )
33 fvco3 ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝑗𝐴 ) → ( ( 𝐻𝐹 ) ‘ 𝑗 ) = ( 𝐻 ‘ ( 𝐹𝑗 ) ) )
34 11 14 33 syl2anc ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( 𝐻𝐹 ) ‘ 𝑗 ) = ( 𝐻 ‘ ( 𝐹𝑗 ) ) )
35 32 34 oveq12d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) = ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) )
36 35 fveq2d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) = ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) )
37 36 breq1d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐻 ‘ ( 𝐹𝑘 ) ) − ( 𝐻 ‘ ( 𝐹𝑗 ) ) ) ) < 𝑥 ) )
38 30 37 sylibrd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
39 38 imim2d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑗𝐴𝑘𝐴 ) ) → ( ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( 𝑗𝑘 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
40 39 anassrs ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗𝐴 ) ∧ 𝑘𝐴 ) → ( ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ( 𝑗𝑘 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
41 40 ralimdva ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑗𝐴 ) → ( ∀ 𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
42 41 reximdva ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ∃ 𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∃ 𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
43 42 ralimdva ( 𝜑 → ( ∀ 𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( 𝐹𝑘 ) − ( 𝐹𝑗 ) ) ) < 𝑥 ) → ∀ 𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) ) )
44 4 43 mpd ( 𝜑 → ∀ 𝑥 ∈ ℝ+𝑗𝐴𝑘𝐴 ( 𝑗𝑘 → ( abs ‘ ( ( ( 𝐻𝐹 ) ‘ 𝑘 ) − ( ( 𝐻𝐹 ) ‘ 𝑗 ) ) ) < 𝑥 ) )
45 1 10 3 44 caurcvgr ( 𝜑 → ( 𝐻𝐹 ) ⇝𝑟 ( lim sup ‘ ( 𝐻𝐹 ) ) )
46 rlimrel Rel ⇝𝑟
47 46 releldmi ( ( 𝐻𝐹 ) ⇝𝑟 ( lim sup ‘ ( 𝐻𝐹 ) ) → ( 𝐻𝐹 ) ∈ dom ⇝𝑟 )
48 45 47 syl ( 𝜑 → ( 𝐻𝐹 ) ∈ dom ⇝𝑟 )
49 ax-resscn ℝ ⊆ ℂ
50 fss ( ( ( 𝐻𝐹 ) : 𝐴 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ( 𝐻𝐹 ) : 𝐴 ⟶ ℂ )
51 10 49 50 sylancl ( 𝜑 → ( 𝐻𝐹 ) : 𝐴 ⟶ ℂ )
52 51 3 rlimdm ( 𝜑 → ( ( 𝐻𝐹 ) ∈ dom ⇝𝑟 ↔ ( 𝐻𝐹 ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝐻𝐹 ) ) ) )
53 48 52 mpbid ( 𝜑 → ( 𝐻𝐹 ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝐻𝐹 ) ) )
54 8 53 eqbrtrrd ( 𝜑 → ( 𝑛𝐴 ↦ ( 𝐻 ‘ ( 𝐹𝑛 ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝐻𝐹 ) ) )