Proof of Theorem climcvg1nlem
Step | Hyp | Ref
| Expression |
1 | | nnuz 9522 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 9239 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | climcvg1n.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
4 | 3 | ffvelrnda 5631 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (𝐹‘𝑥) ∈ ℂ) |
5 | 4 | recld 10902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
6 | | climcvg1nlem.g |
. . . . . 6
⊢ 𝐺 = (𝑥 ∈ ℕ ↦ (ℜ‘(𝐹‘𝑥))) |
7 | 5, 6 | fmptd 5650 |
. . . . 5
⊢ (𝜑 → 𝐺:ℕ⟶ℝ) |
8 | | climcvg1n.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
9 | | climcvg1n.cau |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) |
10 | | eluznn 9559 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
11 | 10 | adantll 473 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑘 ∈ ℕ) |
12 | 3 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐹:ℕ⟶ℂ) |
13 | 12, 11 | ffvelrnd 5632 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑘) ∈ ℂ) |
14 | 13 | recld 10902 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℜ‘(𝐹‘𝑘)) ∈ ℝ) |
15 | | fveq2 5496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → (𝐹‘𝑥) = (𝐹‘𝑘)) |
16 | 15 | fveq2d 5500 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑘 → (ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑘))) |
17 | 16, 6 | fvmptg 5572 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℕ ∧
(ℜ‘(𝐹‘𝑘)) ∈ ℝ) → (𝐺‘𝑘) = (ℜ‘(𝐹‘𝑘))) |
18 | 11, 14, 17 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐺‘𝑘) = (ℜ‘(𝐹‘𝑘))) |
19 | | simplr 525 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℕ) |
20 | 12, 19 | ffvelrnd 5632 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑛) ∈ ℂ) |
21 | 20 | recld 10902 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℜ‘(𝐹‘𝑛)) ∈ ℝ) |
22 | | fveq2 5496 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛)) |
23 | 22 | fveq2d 5500 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑛 → (ℜ‘(𝐹‘𝑥)) = (ℜ‘(𝐹‘𝑛))) |
24 | 23, 6 | fvmptg 5572 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ ∧
(ℜ‘(𝐹‘𝑛)) ∈ ℝ) → (𝐺‘𝑛) = (ℜ‘(𝐹‘𝑛))) |
25 | 19, 21, 24 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐺‘𝑛) = (ℜ‘(𝐹‘𝑛))) |
26 | 18, 25 | oveq12d 5871 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐺‘𝑘) − (𝐺‘𝑛)) = ((ℜ‘(𝐹‘𝑘)) − (ℜ‘(𝐹‘𝑛)))) |
27 | 13, 20 | resubd 10925 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛))) = ((ℜ‘(𝐹‘𝑘)) − (ℜ‘(𝐹‘𝑛)))) |
28 | 26, 27 | eqtr4d 2206 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐺‘𝑘) − (𝐺‘𝑛)) = (ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
29 | 28 | fveq2d 5500 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) = (abs‘(ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛))))) |
30 | 13, 20 | subcld 8230 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐹‘𝑘) − (𝐹‘𝑛)) ∈ ℂ) |
31 | | absrele 11047 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑘) − (𝐹‘𝑛)) ∈ ℂ →
(abs‘(ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛)))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
(abs‘(ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛)))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
33 | 29, 32 | eqbrtrd 4011 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
34 | 30 | recld 10902 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∈ ℝ) |
35 | 34 | recnd 7948 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℜ‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∈ ℂ) |
36 | 28, 35 | eqeltrd 2247 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐺‘𝑘) − (𝐺‘𝑛)) ∈ ℂ) |
37 | 36 | abscld 11145 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) ∈ ℝ) |
38 | 30 | abscld 11145 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∈ ℝ) |
39 | 8 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝐶 ∈
ℝ+) |
40 | 19 | nnrpd 9651 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → 𝑛 ∈ ℝ+) |
41 | 39, 40 | rpdivcld 9671 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐶 / 𝑛) ∈
ℝ+) |
42 | 41 | rpred 9653 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐶 / 𝑛) ∈ ℝ) |
43 | | lelttr 8008 |
. . . . . . . . . 10
⊢
(((abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∈ ℝ ∧ (𝐶 / 𝑛) ∈ ℝ) → (((abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) → (abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) < (𝐶 / 𝑛))) |
44 | 37, 38, 42, 43 | syl3anc 1233 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) → (abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) < (𝐶 / 𝑛))) |
45 | 33, 44 | mpand 427 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛) → (abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) < (𝐶 / 𝑛))) |
46 | 45 | ralimdva 2537 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛) → ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) < (𝐶 / 𝑛))) |
47 | 46 | ralimdva 2537 |
. . . . . 6
⊢ (𝜑 → (∀𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛) → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) < (𝐶 / 𝑛))) |
48 | 9, 47 | mpd 13 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐺‘𝑘) − (𝐺‘𝑛))) < (𝐶 / 𝑛)) |
49 | 7, 8, 48 | climrecvg1n 11311 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ dom ⇝ ) |
50 | | climdm 11258 |
. . . 4
⊢ (𝐺 ∈ dom ⇝ ↔ 𝐺 ⇝ ( ⇝ ‘𝐺)) |
51 | 49, 50 | sylib 121 |
. . 3
⊢ (𝜑 → 𝐺 ⇝ ( ⇝ ‘𝐺)) |
52 | | nnex 8884 |
. . . 4
⊢ ℕ
∈ V |
53 | | fex 5725 |
. . . 4
⊢ ((𝐹:ℕ⟶ℂ ∧
ℕ ∈ V) → 𝐹
∈ V) |
54 | 3, 52, 53 | sylancl 411 |
. . 3
⊢ (𝜑 → 𝐹 ∈ V) |
55 | 4 | imcld 10903 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ) → (ℑ‘(𝐹‘𝑥)) ∈ ℝ) |
56 | | climcvg1nlem.h |
. . . . . . 7
⊢ 𝐻 = (𝑥 ∈ ℕ ↦ (ℑ‘(𝐹‘𝑥))) |
57 | 55, 56 | fmptd 5650 |
. . . . . 6
⊢ (𝜑 → 𝐻:ℕ⟶ℝ) |
58 | 13 | imcld 10903 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℑ‘(𝐹‘𝑘)) ∈ ℝ) |
59 | 15 | fveq2d 5500 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑘 → (ℑ‘(𝐹‘𝑥)) = (ℑ‘(𝐹‘𝑘))) |
60 | 59, 56 | fvmptg 5572 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ ∧
(ℑ‘(𝐹‘𝑘)) ∈ ℝ) → (𝐻‘𝑘) = (ℑ‘(𝐹‘𝑘))) |
61 | 11, 58, 60 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐻‘𝑘) = (ℑ‘(𝐹‘𝑘))) |
62 | 20 | imcld 10903 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℑ‘(𝐹‘𝑛)) ∈ ℝ) |
63 | 22 | fveq2d 5500 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑛 → (ℑ‘(𝐹‘𝑥)) = (ℑ‘(𝐹‘𝑛))) |
64 | 63, 56 | fvmptg 5572 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ ∧
(ℑ‘(𝐹‘𝑛)) ∈ ℝ) → (𝐻‘𝑛) = (ℑ‘(𝐹‘𝑛))) |
65 | 19, 62, 64 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐻‘𝑛) = (ℑ‘(𝐹‘𝑛))) |
66 | 61, 65 | oveq12d 5871 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐻‘𝑘) − (𝐻‘𝑛)) = ((ℑ‘(𝐹‘𝑘)) − (ℑ‘(𝐹‘𝑛)))) |
67 | 13, 20 | imsubd 10926 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (ℑ‘((𝐹‘𝑘) − (𝐹‘𝑛))) = ((ℑ‘(𝐹‘𝑘)) − (ℑ‘(𝐹‘𝑛)))) |
68 | 66, 67 | eqtr4d 2206 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐻‘𝑘) − (𝐻‘𝑛)) = (ℑ‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
69 | 68 | fveq2d 5500 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) = (abs‘(ℑ‘((𝐹‘𝑘) − (𝐹‘𝑛))))) |
70 | | absimle 11048 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑘) − (𝐹‘𝑛)) ∈ ℂ →
(abs‘(ℑ‘((𝐹‘𝑘) − (𝐹‘𝑛)))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
71 | 30, 70 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) →
(abs‘(ℑ‘((𝐹‘𝑘) − (𝐹‘𝑛)))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
72 | 69, 71 | eqbrtrd 4011 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛)))) |
73 | 61, 58 | eqeltrd 2247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐻‘𝑘) ∈ ℝ) |
74 | 65, 62 | eqeltrd 2247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (𝐻‘𝑛) ∈ ℝ) |
75 | 73, 74 | resubcld 8300 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐻‘𝑘) − (𝐻‘𝑛)) ∈ ℝ) |
76 | 75 | recnd 7948 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((𝐻‘𝑘) − (𝐻‘𝑛)) ∈ ℂ) |
77 | 76 | abscld 11145 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) ∈ ℝ) |
78 | | lelttr 8008 |
. . . . . . . . . . 11
⊢
(((abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) ∈ ℝ ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∈ ℝ ∧ (𝐶 / 𝑛) ∈ ℝ) → (((abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) → (abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) < (𝐶 / 𝑛))) |
79 | 77, 38, 42, 78 | syl3anc 1233 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → (((abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) ≤ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) ∧ (abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛)) → (abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) < (𝐶 / 𝑛))) |
80 | 72, 79 | mpand 427 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛) → (abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) < (𝐶 / 𝑛))) |
81 | 80 | ralimdva 2537 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛) → ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) < (𝐶 / 𝑛))) |
82 | 81 | ralimdva 2537 |
. . . . . . 7
⊢ (𝜑 → (∀𝑛 ∈ ℕ ∀𝑘 ∈
(ℤ≥‘𝑛)(abs‘((𝐹‘𝑘) − (𝐹‘𝑛))) < (𝐶 / 𝑛) → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) < (𝐶 / 𝑛))) |
83 | 9, 82 | mpd 13 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘((𝐻‘𝑘) − (𝐻‘𝑛))) < (𝐶 / 𝑛)) |
84 | 57, 8, 83 | climrecvg1n 11311 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ dom ⇝ ) |
85 | | climdm 11258 |
. . . . 5
⊢ (𝐻 ∈ dom ⇝ ↔ 𝐻 ⇝ ( ⇝ ‘𝐻)) |
86 | 84, 85 | sylib 121 |
. . . 4
⊢ (𝜑 → 𝐻 ⇝ ( ⇝ ‘𝐻)) |
87 | | ax-icn 7869 |
. . . . 5
⊢ i ∈
ℂ |
88 | 87 | a1i 9 |
. . . 4
⊢ (𝜑 → i ∈
ℂ) |
89 | | climcvg1nlem.j |
. . . . . 6
⊢ 𝐽 = (𝑥 ∈ ℕ ↦ (i · (𝐻‘𝑥))) |
90 | 52 | mptex 5722 |
. . . . . 6
⊢ (𝑥 ∈ ℕ ↦ (i
· (𝐻‘𝑥))) ∈ V |
91 | 89, 90 | eqeltri 2243 |
. . . . 5
⊢ 𝐽 ∈ V |
92 | 91 | a1i 9 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ V) |
93 | | ax-resscn 7866 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
94 | 93 | a1i 9 |
. . . . . 6
⊢ (𝜑 → ℝ ⊆
ℂ) |
95 | 57, 94 | fssd 5360 |
. . . . 5
⊢ (𝜑 → 𝐻:ℕ⟶ℂ) |
96 | 95 | ffvelrnda 5631 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) ∈ ℂ) |
97 | 89 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐽 = (𝑥 ∈ ℕ ↦ (i · (𝐻‘𝑥)))) |
98 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐻‘𝑥) = (𝐻‘𝑘)) |
99 | 98 | oveq2d 5869 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (i · (𝐻‘𝑥)) = (i · (𝐻‘𝑘))) |
100 | 99 | adantl 275 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑥 = 𝑘) → (i · (𝐻‘𝑥)) = (i · (𝐻‘𝑘))) |
101 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ) |
102 | 87 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → i ∈
ℂ) |
103 | 102, 96 | mulcld 7940 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (i · (𝐻‘𝑘)) ∈ ℂ) |
104 | 97, 100, 101, 103 | fvmptd 5577 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) = (i · (𝐻‘𝑘))) |
105 | 1, 2, 86, 88, 92, 96, 104 | climmulc2 11294 |
. . 3
⊢ (𝜑 → 𝐽 ⇝ (i · ( ⇝ ‘𝐻))) |
106 | 7 | ffvelrnda 5631 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
107 | 106 | recnd 7948 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℂ) |
108 | 104, 103 | eqeltrd 2247 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) ∈ ℂ) |
109 | 3 | ffvelrnda 5631 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
110 | 109 | replimd 10905 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((ℜ‘(𝐹‘𝑘)) + (i · (ℑ‘(𝐹‘𝑘))))) |
111 | 109 | recld 10902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℜ‘(𝐹‘𝑘)) ∈ ℝ) |
112 | 101, 111,
17 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = (ℜ‘(𝐹‘𝑘))) |
113 | 109 | imcld 10903 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (ℑ‘(𝐹‘𝑘)) ∈ ℝ) |
114 | 101, 113,
60 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = (ℑ‘(𝐹‘𝑘))) |
115 | 114 | oveq2d 5869 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (i · (𝐻‘𝑘)) = (i · (ℑ‘(𝐹‘𝑘)))) |
116 | 104, 115 | eqtrd 2203 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐽‘𝑘) = (i · (ℑ‘(𝐹‘𝑘)))) |
117 | 112, 116 | oveq12d 5871 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐺‘𝑘) + (𝐽‘𝑘)) = ((ℜ‘(𝐹‘𝑘)) + (i · (ℑ‘(𝐹‘𝑘))))) |
118 | 110, 117 | eqtr4d 2206 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = ((𝐺‘𝑘) + (𝐽‘𝑘))) |
119 | 1, 2, 51, 54, 105, 107, 108, 118 | climadd 11289 |
. 2
⊢ (𝜑 → 𝐹 ⇝ (( ⇝ ‘𝐺) + (i · ( ⇝ ‘𝐻)))) |
120 | | climrel 11243 |
. . 3
⊢ Rel
⇝ |
121 | 120 | releldmi 4850 |
. 2
⊢ (𝐹 ⇝ (( ⇝ ‘𝐺) + (i · ( ⇝
‘𝐻))) → 𝐹 ∈ dom ⇝
) |
122 | 119, 121 | syl 14 |
1
⊢ (𝜑 → 𝐹 ∈ dom ⇝ ) |