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