Step | Hyp | Ref
| Expression |
1 | | serf0.4 |
. . . . 5
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
2 | | serf0.2 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | caucvgb.1 |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | 3 | caucvgb 15141 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ seq𝑀( + , 𝐹) ∈ dom ⇝ ) → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
5 | 2, 1, 4 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (seq𝑀( + , 𝐹) ∈ dom ⇝ ↔ ∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
6 | 1, 5 | mpbid 235 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)) |
7 | 3 | cau3 14817 |
. . . 4
⊢
(∀𝑥 ∈
ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥)) |
8 | 6, 7 | sylib 221 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥)) |
9 | 3 | peano2uzs 12396 |
. . . . . . 7
⊢ (𝑗 ∈ 𝑍 → (𝑗 + 1) ∈ 𝑍) |
10 | 9 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + 1) ∈ 𝑍) |
11 | | eluzelz 12346 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → 𝑚 ∈ ℤ) |
12 | | uzid 12351 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℤ → 𝑚 ∈
(ℤ≥‘𝑚)) |
13 | | peano2uz 12395 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘𝑚) → (𝑚 + 1) ∈
(ℤ≥‘𝑚)) |
14 | | fveq2 6686 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑚 + 1) → (seq𝑀( + , 𝐹)‘𝑘) = (seq𝑀( + , 𝐹)‘(𝑚 + 1))) |
15 | 14 | oveq2d 7198 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑚 + 1) → ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘)) = ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) |
16 | 15 | fveq2d 6690 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑚 + 1) → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) = (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1))))) |
17 | 16 | breq1d 5050 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑚 + 1) → ((abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥 ↔ (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥)) |
18 | 17 | rspcv 3524 |
. . . . . . . . . 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 494 |
. . . . . . . 8
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → (((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥)) |
21 | 20 | ralimia 3074 |
. . . . . . 7
⊢
(∀𝑚 ∈
(ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥) |
22 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
23 | 22, 3 | eleqtrdi 2844 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
24 | | eluzelz 12346 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ ℤ) |
26 | | eluzp1m1 12362 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈
(ℤ≥‘𝑗)) |
27 | 25, 26 | sylan 583 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈
(ℤ≥‘𝑗)) |
28 | | fveq2 6686 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 1) → (seq𝑀( + , 𝐹)‘𝑚) = (seq𝑀( + , 𝐹)‘(𝑘 − 1))) |
29 | | fvoveq1 7205 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = (𝑘 − 1) → (seq𝑀( + , 𝐹)‘(𝑚 + 1)) = (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1))) |
30 | 28, 29 | oveq12d 7200 |
. . . . . . . . . . . . 13
⊢ (𝑚 = (𝑘 − 1) → ((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1))) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) |
31 | 30 | fveq2d 6690 |
. . . . . . . . . . . 12
⊢ (𝑚 = (𝑘 − 1) → (abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1))))) |
32 | 31 | breq1d 5050 |
. . . . . . . . . . 11
⊢ (𝑚 = (𝑘 − 1) → ((abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 ↔ (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥)) |
33 | 32 | rspcv 3524 |
. . . . . . . . . 10
⊢ ((𝑘 − 1) ∈
(ℤ≥‘𝑗) → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥)) |
34 | 27, 33 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥)) |
35 | | serf0.5 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
36 | 3, 2, 35 | serf 13502 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
37 | 36 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → seq𝑀( + , 𝐹):𝑍⟶ℂ) |
38 | 3 | uztrn2 12355 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑍 ∧ (𝑘 − 1) ∈
(ℤ≥‘𝑗)) → (𝑘 − 1) ∈ 𝑍) |
39 | 22, 27, 38 | syl2an2r 685 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝑘 − 1) ∈ 𝑍) |
40 | 37, 39 | ffvelrnd 6874 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘(𝑘 − 1)) ∈ ℂ) |
41 | 3 | uztrn2 12355 |
. . . . . . . . . . . . . 14
⊢ (((𝑗 + 1) ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ 𝑍) |
42 | 10, 41 | sylan 583 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈ 𝑍) |
43 | 37, 42 | ffvelrnd 6874 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘𝑘) ∈ ℂ) |
44 | 40, 43 | abssubd 14915 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘𝑘))) = (abs‘((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))))) |
45 | | eluzelz 12346 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘(𝑗 + 1)) → 𝑘 ∈ ℤ) |
46 | 45 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
ℤ) |
47 | 46 | zcnd 12181 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
ℂ) |
48 | | ax-1cn 10685 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
49 | | npcan 10985 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 −
1) + 1) = 𝑘) |
50 | 47, 48, 49 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((𝑘 − 1) + 1) = 𝑘) |
51 | 50 | fveq2d 6690 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)) = (seq𝑀( + , 𝐹)‘𝑘)) |
52 | 51 | oveq2d 7198 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1))) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘𝑘))) |
53 | 52 | fveq2d 6690 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘𝑘)))) |
54 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑀 ∈ ℤ) |
55 | | eluzp1p1 12364 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → (𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
56 | 23, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1))) |
57 | | eqid 2739 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘(𝑀 + 1)) =
(ℤ≥‘(𝑀 + 1)) |
58 | 57 | uztrn2 12355 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑗 + 1) ∈
(ℤ≥‘(𝑀 + 1)) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) |
59 | 56, 58 | sylan 583 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) |
60 | | seqm1 13491 |
. . . . . . . . . . . . . . 15
⊢ ((𝑀 ∈ ℤ ∧ 𝑘 ∈
(ℤ≥‘(𝑀 + 1))) → (seq𝑀( + , 𝐹)‘𝑘) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘))) |
61 | 54, 59, 60 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (seq𝑀( + , 𝐹)‘𝑘) = ((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘))) |
62 | 61 | oveq1d 7197 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → ((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))) = (((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘)) − (seq𝑀( + , 𝐹)‘(𝑘 − 1)))) |
63 | 35 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℂ) |
64 | 42, 63 | syldan 594 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝐹‘𝑘) ∈ ℂ) |
65 | 40, 64 | pncan2d 11089 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (((seq𝑀( + , 𝐹)‘(𝑘 − 1)) + (𝐹‘𝑘)) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))) = (𝐹‘𝑘)) |
66 | 62, 65 | eqtr2d 2775 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (𝐹‘𝑘) = ((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1)))) |
67 | 66 | fveq2d 6690 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (abs‘(𝐹‘𝑘)) = (abs‘((seq𝑀( + , 𝐹)‘𝑘) − (seq𝑀( + , 𝐹)‘(𝑘 − 1))))) |
68 | 44, 53, 67 | 3eqtr4d 2784 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) = (abs‘(𝐹‘𝑘))) |
69 | 68 | breq1d 5050 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) →
((abs‘((seq𝑀( + ,
𝐹)‘(𝑘 − 1)) − (seq𝑀( + , 𝐹)‘((𝑘 − 1) + 1)))) < 𝑥 ↔ (abs‘(𝐹‘𝑘)) < 𝑥)) |
70 | 34, 69 | sylibd 242 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘(𝑗 + 1))) → (∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → (abs‘(𝐹‘𝑘)) < 𝑥)) |
71 | 70 | ralrimdva 3102 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘(𝑚 + 1)))) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
72 | 21, 71 | syl5 34 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
73 | | fveq2 6686 |
. . . . . . . 8
⊢ (𝑛 = (𝑗 + 1) →
(ℤ≥‘𝑛) = (ℤ≥‘(𝑗 + 1))) |
74 | 73 | raleqdv 3317 |
. . . . . . 7
⊢ (𝑛 = (𝑗 + 1) → (∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥 ↔ ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥)) |
75 | 74 | rspcev 3529 |
. . . . . 6
⊢ (((𝑗 + 1) ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘(𝑗 + 1))(abs‘(𝐹‘𝑘)) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥) |
76 | 10, 72, 75 | syl6an 684 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
77 | 76 | rexlimdva 3195 |
. . . 4
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
78 | 77 | ralimdv 3093 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑚 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑚) ∈ ℂ ∧ ∀𝑘 ∈
(ℤ≥‘𝑚)(abs‘((seq𝑀( + , 𝐹)‘𝑚) − (seq𝑀( + , 𝐹)‘𝑘))) < 𝑥) → ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
79 | 8, 78 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥) |
80 | | serf0.3 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑉) |
81 | | eqidd 2740 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = (𝐹‘𝑘)) |
82 | 3, 2, 80, 81, 35 | clim0c 14966 |
. 2
⊢ (𝜑 → (𝐹 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑛 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑛)(abs‘(𝐹‘𝑘)) < 𝑥)) |
83 | 79, 82 | mpbird 260 |
1
⊢ (𝜑 → 𝐹 ⇝ 0) |