Step | Hyp | Ref
| Expression |
1 | | serf0.4 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
2 | | serf0.2 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | caucvgb.1 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | caucvgb 14258 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
5 | 2, 1, 4 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
6 | 1, 5 | mpbid 221 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)) |
7 | 3 | cau3 13943 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥)) |
8 | 6, 7 | sylib 207 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥)) |
9 | 3 | peano2uzs 11618 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑍 → (𝑗 + 1) ∈ 𝑍) |
10 | 9 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + 1) ∈ 𝑍) |
11 | | eluzelz 11573 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → 𝑚 ∈ ℤ) |
12 | | uzid 11578 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
(ℤ≥‘𝑚)) |
13 | | peano2uz 11617 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑚) → (𝑚 + 1) ∈
(ℤ≥‘𝑚)) |
14 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘𝑘) = (seq𝑀( + , 𝐹)‘(𝑚 + 1))) |
15 | 14 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘)) = ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑚 + 1) → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) = (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1))))) |
17 | 16 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑚 + 1) → ((abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥 ↔ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥)) |
18 | 17 | rspcv 3278 |
. . . . . . . . . 10
⊢ ((𝑚 + 1) ∈
(ℤ≥‘𝑚) → (∀𝑘 ∈ (ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥)) |
19 | 11, 12, 13, 18 | 4syl 19 |
. . . . . . . . 9
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (∀𝑘 ∈ (ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥)) |
20 | 19 | adantld 482 |
. . . . . . . 8
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥)) |
21 | 20 | ralimia 2934 |
. . . . . . 7
⊢
(∀𝑚 ∈
(ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥) |
22 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
23 | 22, 3 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
24 | | eluzelz 11573 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ ℤ) |
26 | | eluzp1m1 11587 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈
(ℤ≥‘𝑗)) |
27 | 25, 26 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈
(ℤ≥‘𝑗)) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 1) → (seq𝑀( + , 𝐹)‘𝑚) = (seq𝑀( + , 𝐹)‘(𝑘 − 1))) |
29 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (𝑘 − 1) → (𝑚 + 1) = ((𝑘 − 1) + 1)) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 1) → (seq𝑀( + , 𝐹)‘(𝑚 + 1)) = (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1))) |
31 | 28, 30 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 − 1) → ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) |
32 | 31 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 − 1) → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1))))) |
33 | 32 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 1) → ((abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 ↔ (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥)) |
34 | 33 | rspcv 3278 |
. . . . . . . . . 10
⊢ ((𝑘 − 1) ∈
(ℤ≥‘𝑗) → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥)) |
35 | 27, 34 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥)) |
36 | | serf0.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
37 | 3, 2, 36 | serf 12691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
38 | 37 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
39 | 3 | uztrn2 11581 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ 𝑍 ∧ (𝑘 − 1) ∈
(ℤ≥‘𝑗)) → (𝑘 − 1) ∈ 𝑍) |
40 | 22, 39 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ (𝑘 − 1) ∈
(ℤ≥‘𝑗)) → (𝑘 − 1) ∈ 𝑍) |
41 | 27, 40 | syldan 486 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈ 𝑍) |
42 | 38, 41 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘(𝑘 − 1)) ∈ ℂ) |
43 | 3 | uztrn2 11581 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ 𝑍) |
44 | 10, 43 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ 𝑍) |
45 | 38, 44 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘𝑘) ∈ ℂ) |
46 | 42, 45 | abssubd 14040 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘𝑘))) = (abs‘((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))))) |
47 | | eluzelz 11573 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘(𝑗 + 1)) → 𝑘 ∈ ℤ) |
48 | 47 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
ℤ) |
49 | 48 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
ℂ) |
50 | | ax-1cn 9873 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
51 | | npcan 10169 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 −
1) + 1) = 𝑘) |
52 | 49, 50, 51 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((𝑘 − 1) + 1) = 𝑘) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)) = (seq𝑀( + , 𝐹)‘𝑘)) |
54 | 53 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘𝑘))) |
55 | 54 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘𝑘)))) |
56 | 2 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑀 ∈ ℤ) |
57 | | eluzp1p1 11589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
58 | 23, 57 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
59 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘(𝑀 + 1)) =
(ℤ≥‘(𝑀 + 1)) |
60 | 59 | uztrn2 11581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) |
61 | 58, 60 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) |
62 | | seqm1 12680 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑘) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘))) |
63 | 56, 61, 62 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘𝑘) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘))) |
64 | 63 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))) = (((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘)) − (seq𝑀( + , 𝐹)‘(𝑘 − 1)))) |
65 | 36 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
66 | 44, 65 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
67 | 42, 66 | pncan2d 10273 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘)) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))) = (𝐹‘𝑘)) |
68 | 64, 67 | eqtr2d 2645 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝐹‘𝑘) = ((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1)))) |
69 | 68 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (abs‘(𝐹‘𝑘)) = (abs‘((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))))) |
70 | 46, 55, 69 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) = (abs‘(𝐹‘𝑘))) |
71 | 70 | breq1d 4593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
((abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥 ↔ (abs‘(𝐹‘𝑘)) < 𝑥)) |
72 | 35, 71 | sylibd 228 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → (abs‘(𝐹‘𝑘)) < 𝑥)) |
73 | 72 | ralrimdva 2952 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
74 | 21, 73 | syl5 33 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
75 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑛 = (𝑗 + 1) →
(ℤ≥‘𝑛) = (ℤ≥‘(𝑗 + 1))) |
76 | 75 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑛 = (𝑗 + 1) → (∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
77 | 76 | rspcev 3282 |
. . . . . 6
⊢ (((𝑗 + 1) ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥) |
78 | 10, 74, 77 | syl6an 566 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
79 | 78 | rexlimdva 3013 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
80 | 79 | ralimdv 2946 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
81 | 8, 80 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥) |
82 | | serf0.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
83 | | eqidd 2611 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
84 | 3, 2, 82, 83, 36 | clim0c 14086 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
85 | 81, 84 | mpbird 246 |
1
⊢ (𝜑 → 𝐹 ⇝ 0) |