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 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐴 ↦ ( 𝐻 ‘ ( 𝐹 ‘ 𝑛 ) ) ) ⇝𝑟 ( ⇝𝑟 ‘ ( 𝐻 ∘ 𝐹 ) ) )