Step | Hyp | Ref
| Expression |
1 | | serif0.2 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
2 | | serif0.4 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝
) |
3 | | climcauc.1 |
. . . . . 6
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | climcaucn 10188 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ seq𝑀( + , 𝐹, ℂ) ∈ dom ⇝ ) →
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑗))) < 𝑥)) |
5 | 1, 2, 4 | syl2anc 403 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑗))) < 𝑥)) |
6 | 3 | cau3 10001 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥)) |
7 | 5, 6 | sylib 120 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥)) |
8 | 3 | peano2uzs 8672 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑍 → (𝑗 + 1) ∈ 𝑍) |
9 | 8 | adantl 271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + 1) ∈ 𝑍) |
10 | | eluzelz 8628 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → 𝑚 ∈ ℤ) |
11 | | uzid 8633 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
(ℤ≥‘𝑚)) |
12 | | peano2uz 8671 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑚) → (𝑚 + 1) ∈
(ℤ≥‘𝑚)) |
13 | | fveq2 5198 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑚 + 1) → (seq𝑀( + , 𝐹, ℂ)‘𝑘) = (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1))) |
14 | 13 | oveq2d 5548 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑚 + 1) → ((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘)) = ((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) |
15 | 14 | fveq2d 5202 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑚 + 1) → (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) = (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1))))) |
16 | 15 | breq1d 3795 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑚 + 1) → ((abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥 ↔ (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥)) |
17 | 16 | rspcv 2697 |
. . . . . . . . . 10
⊢ ((𝑚 + 1) ∈
(ℤ≥‘𝑚) → (∀𝑘 ∈ (ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥)) |
18 | 10, 11, 12, 17 | 4syl 18 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥)) |
19 | 18 | adantld 272 |
. . . . . . . 8
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥)) |
20 | 19 | ralimia 2424 |
. . . . . . 7
⊢
(∀𝑚 ∈
(ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥) |
21 | | simpr 108 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
22 | 21, 3 | syl6eleq 2171 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
23 | | eluzelz 8628 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
24 | 22, 23 | syl 14 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ ℤ) |
25 | | eluzp1m1 8642 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈
(ℤ≥‘𝑗)) |
26 | 24, 25 | sylan 277 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈
(ℤ≥‘𝑗)) |
27 | | fveq2 5198 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 1) → (seq𝑀( + , 𝐹, ℂ)‘𝑚) = (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1))) |
28 | | oveq1 5539 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑘 − 1) → (𝑚 + 1) = ((𝑘 − 1) + 1)) |
29 | 28 | fveq2d 5202 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 1) → (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)) = (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1))) |
30 | 27, 29 | oveq12d 5550 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 − 1) → ((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) |
31 | 30 | fveq2d 5202 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 − 1) → (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) = (abs‘((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1))))) |
32 | 31 | breq1d 3795 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 1) → ((abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥 ↔ (abs‘((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) < 𝑥)) |
33 | 32 | rspcv 2697 |
. . . . . . . . . 10
⊢ ((𝑘 − 1) ∈
(ℤ≥‘𝑗) → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) < 𝑥)) |
34 | 26, 33 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) < 𝑥)) |
35 | | serif0.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
36 | 3, 1, 35 | iserf 9453 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → seq𝑀( + , 𝐹, ℂ):𝑍⟶ℂ) |
37 | 36 | ad2antrr 471 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → seq𝑀( + , 𝐹, ℂ):𝑍⟶ℂ) |
38 | 3 | uztrn2 8636 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑍 ∧ (𝑘 − 1) ∈
(ℤ≥‘𝑗)) → (𝑘 − 1) ∈ 𝑍) |
39 | 21, 38 | sylan 277 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝑘 − 1) ∈
(ℤ≥‘𝑗)) → (𝑘 − 1) ∈ 𝑍) |
40 | 26, 39 | syldan 276 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈ 𝑍) |
41 | 37, 40 | ffvelrnd 5324 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) ∈ ℂ) |
42 | 3 | uztrn2 8636 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ 𝑍) |
43 | 9, 42 | sylan 277 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ 𝑍) |
44 | 37, 43 | ffvelrnd 5324 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘𝑘) ∈ ℂ) |
45 | 41, 44 | abssubd 10079 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) = (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑘) − (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1))))) |
46 | | eluzelz 8628 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘(𝑗 + 1)) → 𝑘 ∈ ℤ) |
47 | 46 | adantl 271 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
ℤ) |
48 | 47 | zcnd 8470 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
ℂ) |
49 | | ax-1cn 7069 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
50 | | npcan 7317 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 −
1) + 1) = 𝑘) |
51 | 48, 49, 50 | sylancl 404 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((𝑘 − 1) + 1) = 𝑘) |
52 | 51 | fveq2d 5202 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)) = (seq𝑀( + , 𝐹, ℂ)‘𝑘)) |
53 | 52 | oveq2d 5548 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1))) = ((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) |
54 | 53 | fveq2d 5202 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) = (abs‘((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘𝑘)))) |
55 | 1 | ad2antrr 471 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑀 ∈ ℤ) |
56 | | eluzp1p1 8644 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
57 | 22, 56 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
58 | | eqid 2081 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘(𝑀 + 1)) =
(ℤ≥‘(𝑀 + 1)) |
59 | 58 | uztrn2 8636 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) |
60 | 57, 59 | sylan 277 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) |
61 | | cnex 7097 |
. . . . . . . . . . . . . . . 16
⊢ ℂ
∈ V |
62 | 61 | a1i 9 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ℂ ∈
V) |
63 | | simpr 108 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) ∧ 𝑎 ∈ (ℤ≥‘𝑀)) → 𝑎 ∈ (ℤ≥‘𝑀)) |
64 | 63, 3 | syl6eleqr 2172 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) ∧ 𝑎 ∈ (ℤ≥‘𝑀)) → 𝑎 ∈ 𝑍) |
65 | 35 | ralrimiva 2434 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) |
66 | 65 | ad3antrrr 475 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) ∧ 𝑎 ∈ (ℤ≥‘𝑀)) → ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) |
67 | | fveq2 5198 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑎 → (𝐹‘𝑘) = (𝐹‘𝑎)) |
68 | 67 | eleq1d 2147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑎 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑎) ∈ ℂ)) |
69 | 68 | rspcva 2699 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝑍 ∧ ∀𝑘 ∈ 𝑍 (𝐹‘𝑘) ∈ ℂ) → (𝐹‘𝑎) ∈ ℂ) |
70 | 64, 66, 69 | syl2anc 403 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) ∧ 𝑎 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑎) ∈ ℂ) |
71 | | addcl 7098 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ) → (𝑎 + 𝑏) ∈ ℂ) |
72 | 71 | adantl 271 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) ∧ (𝑎 ∈ ℂ ∧ 𝑏 ∈ ℂ)) → (𝑎 + 𝑏) ∈ ℂ) |
73 | 55, 60, 62, 70, 72 | iseqm1 9447 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹, ℂ)‘𝑘) = ((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) + (𝐹‘𝑘))) |
74 | 73 | oveq1d 5547 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((seq𝑀( + , 𝐹, ℂ)‘𝑘) − (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1))) = (((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) + (𝐹‘𝑘)) − (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)))) |
75 | 35 | adantlr 460 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
76 | 43, 75 | syldan 276 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
77 | 41, 76 | pncan2d 7421 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (((seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)) + (𝐹‘𝑘)) − (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1))) = (𝐹‘𝑘)) |
78 | 74, 77 | eqtr2d 2114 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝐹‘𝑘) = ((seq𝑀( + , 𝐹, ℂ)‘𝑘) − (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1)))) |
79 | 78 | fveq2d 5202 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (abs‘(𝐹‘𝑘)) = (abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑘) − (seq𝑀( + , 𝐹, ℂ)‘(𝑘 − 1))))) |
80 | 45, 54, 79 | 3eqtr4d 2123 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) = (abs‘(𝐹‘𝑘))) |
81 | 80 | breq1d 3795 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
((abs‘((seq𝑀( + ,
𝐹, ℂ)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹, ℂ)‘((𝑘 − 1) + 1)))) < 𝑥 ↔ (abs‘(𝐹‘𝑘)) < 𝑥)) |
82 | 34, 81 | sylibd 147 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥 → (abs‘(𝐹‘𝑘)) < 𝑥)) |
83 | 82 | ralrimdva 2441 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘(𝑚 + 1)))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
84 | 20, 83 | syl5 32 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
85 | | fveq2 5198 |
. . . . . . . 8
⊢ (𝑛 = (𝑗 + 1) →
(ℤ≥‘𝑛) = (ℤ≥‘(𝑗 + 1))) |
86 | 85 | raleqdv 2555 |
. . . . . . 7
⊢ (𝑛 = (𝑗 + 1) → (∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
87 | 86 | rspcev 2701 |
. . . . . 6
⊢ (((𝑗 + 1) ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥) |
88 | 9, 84, 87 | syl6an 1363 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
89 | 88 | rexlimdva 2477 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
90 | 89 | ralimdv 2430 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹, ℂ)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹, ℂ)‘𝑚) − (seq𝑀( + , 𝐹, ℂ)‘𝑘))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
91 | 7, 90 | mpd 13 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥) |
92 | | serif0.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
93 | | eqidd 2082 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
94 | 3, 1, 92, 93, 35 | clim0c 10125 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
95 | 91, 94 | mpbird 165 |
1
⊢ (𝜑 → 𝐹 ⇝ 0) |