Step | Hyp | Ref
| Expression |
1 | | iseralt.1 |
. 2
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | | seqex 13010 |
. . 3
⊢ seq𝑀( + , 𝐹) ∈ V |
3 | 2 | a1i 11 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ V) |
4 | | iseralt.5 |
. . . 4
⊢ (𝜑 → 𝐺 ⇝ 0) |
5 | | iseralt.2 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℤ) |
6 | | climrel 14431 |
. . . . . . 7
⊢ Rel
⇝ |
7 | 6 | brrelexi 5298 |
. . . . . 6
⊢ (𝐺 ⇝ 0 → 𝐺 ∈ V) |
8 | 4, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ V) |
9 | | eqidd 2772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) = (𝐺‘𝑛)) |
10 | | iseralt.3 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑍⟶ℝ) |
11 | 10 | ffvelrnda 6502 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ ℝ) |
12 | 11 | recnd 10270 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → (𝐺‘𝑛) ∈ ℂ) |
13 | 1, 5, 8, 9, 12 | clim0c 14446 |
. . . 4
⊢ (𝜑 → (𝐺 ⇝ 0 ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥)) |
14 | 4, 13 | mpbid 222 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥) |
15 | | simpr 471 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ 𝑍) |
16 | 15, 1 | syl6eleq 2860 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑀)) |
17 | | eluzelz 11898 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑗 ∈ ℤ) |
18 | | uzid 11903 |
. . . . . . . 8
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → 𝑗 ∈ (ℤ≥‘𝑗)) |
20 | | peano2uz 11943 |
. . . . . . 7
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (𝑗 + 1) ∈
(ℤ≥‘𝑗)) |
21 | | fveq2 6332 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑗 + 1) → (𝐺‘𝑛) = (𝐺‘(𝑗 + 1))) |
22 | 21 | fveq2d 6336 |
. . . . . . . . 9
⊢ (𝑛 = (𝑗 + 1) → (abs‘(𝐺‘𝑛)) = (abs‘(𝐺‘(𝑗 + 1)))) |
23 | 22 | breq1d 4796 |
. . . . . . . 8
⊢ (𝑛 = (𝑗 + 1) → ((abs‘(𝐺‘𝑛)) < 𝑥 ↔ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥)) |
24 | 23 | rspcv 3456 |
. . . . . . 7
⊢ ((𝑗 + 1) ∈
(ℤ≥‘𝑗) → (∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥)) |
25 | 19, 20, 24 | 3syl 18 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → (abs‘(𝐺‘(𝑗 + 1))) < 𝑥)) |
26 | | eluzelz 11898 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(ℤ≥‘𝑗) → 𝑛 ∈ ℤ) |
27 | 26 | ad2antll 700 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑛 ∈ ℤ) |
28 | 27 | zcnd 11685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑛 ∈ ℂ) |
29 | 17, 1 | eleq2s 2868 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
30 | 29 | ad2antrl 699 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ ℤ) |
31 | 30 | zcnd 11685 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ ℂ) |
32 | 28, 31 | subcld 10594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℂ) |
33 | | 2cnd 11295 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 2 ∈
ℂ) |
34 | | 2ne0 11315 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ≠
0 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 2 ≠
0) |
36 | 32, 33, 35 | divcan2d 11005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (2 · ((𝑛 − 𝑗) / 2)) = (𝑛 − 𝑗)) |
37 | 36 | oveq2d 6809 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗 + (2 · ((𝑛 − 𝑗) / 2))) = (𝑗 + (𝑛 − 𝑗))) |
38 | 31, 28 | pncan3d 10597 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗 + (𝑛 − 𝑗)) = 𝑛) |
39 | 37, 38 | eqtr2d 2806 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑛 = (𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) |
40 | 39 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 𝑛 = (𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) |
41 | 40 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2))))) |
42 | 41 | fvoveq1d 6815 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) →
(abs‘((seq𝑀( + ,
𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗)))) |
43 | | simpll 742 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 𝜑) |
44 | | simpl 468 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑗 ∈ 𝑍) |
45 | 44 | ad2antlr 698 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 𝑗 ∈ 𝑍) |
46 | | simpr 471 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → ((𝑛 − 𝑗) / 2) ∈ ℤ) |
47 | 27, 30 | zsubcld 11689 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℤ) |
48 | 47 | zred 11684 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑛 − 𝑗) ∈ ℝ) |
49 | | 2rp 12040 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℝ+ |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 2 ∈
ℝ+) |
51 | | eluzle 11901 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈
(ℤ≥‘𝑗) → 𝑗 ≤ 𝑛) |
52 | 51 | ad2antll 700 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ≤ 𝑛) |
53 | 27 | zred 11684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑛 ∈ ℝ) |
54 | 30 | zred 11684 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑗 ∈ ℝ) |
55 | 53, 54 | subge0d 10819 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (0 ≤ (𝑛 − 𝑗) ↔ 𝑗 ≤ 𝑛)) |
56 | 52, 55 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 0 ≤ (𝑛 − 𝑗)) |
57 | 48, 50, 56 | divge0d 12115 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 0 ≤ ((𝑛 − 𝑗) / 2)) |
58 | 57 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → 0 ≤ ((𝑛 − 𝑗) / 2)) |
59 | | elnn0z 11592 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 − 𝑗) / 2) ∈ ℕ0 ↔
(((𝑛 − 𝑗) / 2) ∈ ℤ ∧ 0
≤ ((𝑛 − 𝑗) / 2))) |
60 | 46, 58, 59 | sylanbrc 564 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) → ((𝑛 − 𝑗) / 2) ∈
ℕ0) |
61 | | iseralt.4 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘(𝑘 + 1)) ≤ (𝐺‘𝑘)) |
62 | | iseralt.6 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = ((-1↑𝑘) · (𝐺‘𝑘))) |
63 | 1, 5, 10, 61, 4, 62 | iseraltlem3 14622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((𝑛 − 𝑗) / 2) ∈ ℕ0) →
((abs‘((seq𝑀( + ,
𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((𝑛 − 𝑗) / 2))) + 1)) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))) |
64 | 63 | simpld 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((𝑛 − 𝑗) / 2) ∈ ℕ0) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
65 | 43, 45, 60, 64 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) →
(abs‘((seq𝑀( + ,
𝐹)‘(𝑗 + (2 · ((𝑛 − 𝑗) / 2)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
66 | 42, 65 | eqbrtrd 4808 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ ((𝑛 − 𝑗) / 2) ∈ ℤ) →
(abs‘((seq𝑀( + ,
𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
67 | | 2div2e1 11352 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (2 / 2) =
1 |
68 | 67 | oveq2i 6804 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑛 − 𝑗) + 1) / 2) − (2 / 2)) = ((((𝑛 − 𝑗) + 1) / 2) − 1) |
69 | | peano2cn 10410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 − 𝑗) ∈ ℂ → ((𝑛 − 𝑗) + 1) ∈ ℂ) |
70 | 32, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑛 − 𝑗) + 1) ∈ ℂ) |
71 | 70, 33, 33, 35 | divsubdird 11042 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) − 2) / 2) = ((((𝑛 − 𝑗) + 1) / 2) − (2 /
2))) |
72 | | df-2 11281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ 2 = (1 +
1) |
73 | 72 | oveq2i 6804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑛 − 𝑗) + 1) − 2) = (((𝑛 − 𝑗) + 1) − (1 + 1)) |
74 | | ax-1cn 10196 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 1 ∈
ℂ |
75 | 74 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 1 ∈
ℂ) |
76 | 32, 75, 75 | pnpcan2d 10632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (((𝑛 − 𝑗) + 1) − (1 + 1)) = ((𝑛 − 𝑗) − 1)) |
77 | 73, 76 | syl5eq 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (((𝑛 − 𝑗) + 1) − 2) = ((𝑛 − 𝑗) − 1)) |
78 | 77 | oveq1d 6808 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) − 2) / 2) = (((𝑛 − 𝑗) − 1) / 2)) |
79 | 71, 78 | eqtr3d 2807 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) / 2) − (2 / 2)) = (((𝑛 − 𝑗) − 1) / 2)) |
80 | 68, 79 | syl5eqr 2819 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((((𝑛 − 𝑗) + 1) / 2) − 1) = (((𝑛 − 𝑗) − 1) / 2)) |
81 | 80 | oveq2d 6809 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1)) = (2 ·
(((𝑛 − 𝑗) − 1) /
2))) |
82 | | subcl 10482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑛 − 𝑗) ∈ ℂ ∧ 1 ∈ ℂ)
→ ((𝑛 − 𝑗) − 1) ∈
ℂ) |
83 | 32, 74, 82 | sylancl 566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑛 − 𝑗) − 1) ∈ ℂ) |
84 | 83, 33, 35 | divcan2d 11005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (2 · (((𝑛 − 𝑗) − 1) / 2)) = ((𝑛 − 𝑗) − 1)) |
85 | 28, 31, 75 | sub32d 10626 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑛 − 𝑗) − 1) = ((𝑛 − 1) − 𝑗)) |
86 | 81, 84, 85 | 3eqtrd 2809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1)) = ((𝑛 − 1) − 𝑗)) |
87 | 86 | oveq2d 6809 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) = (𝑗 + ((𝑛 − 1) − 𝑗))) |
88 | | subcl 10482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑛 −
1) ∈ ℂ) |
89 | 28, 74, 88 | sylancl 566 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑛 − 1) ∈ ℂ) |
90 | 31, 89 | pncan3d 10597 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗 + ((𝑛 − 1) − 𝑗)) = (𝑛 − 1)) |
91 | 87, 90 | eqtrd 2805 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) = (𝑛 − 1)) |
92 | 91 | oveq1d 6808 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1) = ((𝑛 − 1) +
1)) |
93 | | npcan 10492 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑛 −
1) + 1) = 𝑛) |
94 | 28, 74, 93 | sylancl 566 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑛 − 1) + 1) = 𝑛) |
95 | 92, 94 | eqtr2d 2806 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑛 = ((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) +
1)) |
96 | 95 | adantr 466 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 𝑛 = ((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) +
1)) |
97 | 96 | fveq2d 6336 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (seq𝑀( + , 𝐹)‘𝑛) = (seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) +
1))) |
98 | 97 | fvoveq1d 6815 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) →
(abs‘((seq𝑀( + ,
𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) = (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) −
(seq𝑀( + , 𝐹)‘𝑗)))) |
99 | | simpll 742 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 𝜑) |
100 | 44 | ad2antlr 698 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 𝑗 ∈ 𝑍) |
101 | | simpr 471 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) |
102 | | uznn0sub 11921 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈
(ℤ≥‘𝑗) → (𝑛 − 𝑗) ∈
ℕ0) |
103 | 102 | ad2antll 700 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝑛 − 𝑗) ∈
ℕ0) |
104 | | nn0p1nn 11534 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 − 𝑗) ∈ ℕ0 → ((𝑛 − 𝑗) + 1) ∈ ℕ) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑛 − 𝑗) + 1) ∈ ℕ) |
106 | 105 | nnrpd 12073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((𝑛 − 𝑗) + 1) ∈
ℝ+) |
107 | 106 | rphalfcld 12087 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (((𝑛 − 𝑗) + 1) / 2) ∈
ℝ+) |
108 | 107 | rpgt0d 12078 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 0 < (((𝑛 − 𝑗) + 1) / 2)) |
109 | 108 | adantr 466 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → 0 <
(((𝑛 − 𝑗) + 1) / 2)) |
110 | | elnnz 11589 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑛 − 𝑗) + 1) / 2) ∈ ℕ ↔ ((((𝑛 − 𝑗) + 1) / 2) ∈ ℤ ∧ 0 <
(((𝑛 − 𝑗) + 1) / 2))) |
111 | 101, 109,
110 | sylanbrc 564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → (((𝑛 − 𝑗) + 1) / 2) ∈ ℕ) |
112 | | nnm1nn0 11536 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑛 − 𝑗) + 1) / 2) ∈ ℕ → ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈
ℕ0) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) → ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈
ℕ0) |
114 | 1, 5, 10, 61, 4, 62 | iseraltlem3 14622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈
ℕ0) → ((abs‘((seq𝑀( + , 𝐹)‘(𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1)))) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)) ∧ (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) −
(seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1)))) |
115 | 114 | simprd 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ ((((𝑛 − 𝑗) + 1) / 2) − 1) ∈
ℕ0) → (abs‘((seq𝑀( + , 𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) −
(seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
116 | 99, 100, 113, 115 | syl3anc 1476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) →
(abs‘((seq𝑀( + ,
𝐹)‘((𝑗 + (2 · ((((𝑛 − 𝑗) + 1) / 2) − 1))) + 1)) −
(seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
117 | 98, 116 | eqbrtrd 4808 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) ∧ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ) →
(abs‘((seq𝑀( + ,
𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
118 | | zeo 11665 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 − 𝑗) ∈ ℤ → (((𝑛 − 𝑗) / 2) ∈ ℤ ∨ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ)) |
119 | 47, 118 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (((𝑛 − 𝑗) / 2) ∈ ℤ ∨ (((𝑛 − 𝑗) + 1) / 2) ∈ ℤ)) |
120 | 66, 117, 119 | mpjaodan 962 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (𝐺‘(𝑗 + 1))) |
121 | 1 | peano2uzs 11944 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ 𝑍 → (𝑗 + 1) ∈ 𝑍) |
122 | 121 | adantr 466 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → (𝑗 + 1) ∈ 𝑍) |
123 | | ffvelrn 6500 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:𝑍⟶ℝ ∧ (𝑗 + 1) ∈ 𝑍) → (𝐺‘(𝑗 + 1)) ∈ ℝ) |
124 | 10, 122, 123 | syl2an 575 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (𝐺‘(𝑗 + 1)) ∈ ℝ) |
125 | 1, 5, 10, 61, 4 | iseraltlem1 14620 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ 𝑍) → 0 ≤ (𝐺‘(𝑗 + 1))) |
126 | 122, 125 | sylan2 572 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 0 ≤ (𝐺‘(𝑗 + 1))) |
127 | 124, 126 | absidd 14369 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) = (𝐺‘(𝑗 + 1))) |
128 | 120, 127 | breqtrrd 4814 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1)))) |
129 | 128 | adantlr 686 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1)))) |
130 | | neg1rr 11327 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -1 ∈
ℝ |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -1 ∈ ℝ) |
132 | | neg1ne0 11328 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ -1 ≠
0 |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → -1 ≠ 0) |
134 | | eluzelz 11898 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
135 | 134, 1 | eleq2s 2868 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
136 | 135 | adantl 467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
137 | 131, 133,
136 | reexpclzd 13241 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (-1↑𝑘) ∈ ℝ) |
138 | 10 | ffvelrnda 6502 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ ℝ) |
139 | 137, 138 | remulcld 10272 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((-1↑𝑘) · (𝐺‘𝑘)) ∈ ℝ) |
140 | 62, 139 | eqeltrd 2850 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ ℝ) |
141 | 1, 5, 140 | serfre 13037 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
142 | 1 | uztrn2 11906 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → 𝑛 ∈ 𝑍) |
143 | | ffvelrn 6500 |
. . . . . . . . . . . . . . . 16
⊢
((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑛 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ) |
144 | 141, 142,
143 | syl2an 575 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ) |
145 | | ffvelrn 6500 |
. . . . . . . . . . . . . . . 16
⊢
((seq𝑀( + , 𝐹):𝑍⟶ℝ ∧ 𝑗 ∈ 𝑍) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ) |
146 | 141, 44, 145 | syl2an 575 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (seq𝑀( + , 𝐹)‘𝑗) ∈ ℝ) |
147 | 144, 146 | resubcld 10660 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℝ) |
148 | 147 | recnd 10270 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗)) ∈ ℂ) |
149 | 148 | abscld 14383 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ) |
150 | 149 | adantlr 686 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ) |
151 | 127, 124 | eqeltrd 2850 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ) |
152 | 151 | adantlr 686 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ) |
153 | | rpre 12042 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
154 | 153 | ad2antlr 698 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → 𝑥 ∈ ℝ) |
155 | | lelttr 10330 |
. . . . . . . . . . 11
⊢
(((abs‘((seq𝑀(
+ , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ∈ ℝ ∧ (abs‘(𝐺‘(𝑗 + 1))) ∈ ℝ ∧ 𝑥 ∈ ℝ) →
(((abs‘((seq𝑀( + ,
𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)) |
156 | 150, 152,
154, 155 | syl3anc 1476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) →
(((abs‘((seq𝑀( + ,
𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) ≤ (abs‘(𝐺‘(𝑗 + 1))) ∧ (abs‘(𝐺‘(𝑗 + 1))) < 𝑥) → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)) |
157 | 129, 156 | mpand 667 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)) |
158 | 141 | adantr 466 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → seq𝑀( + , 𝐹):𝑍⟶ℝ) |
159 | 158, 142,
143 | syl2an 575 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → (seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ) |
160 | 157, 159 | jctild 509 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (ℤ≥‘𝑗))) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
161 | 160 | anassrs 458 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑛 ∈ (ℤ≥‘𝑗)) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
162 | 161 | ralrimdva 3118 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → ((abs‘(𝐺‘(𝑗 + 1))) < 𝑥 → ∀𝑛 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
163 | 25, 162 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) → (∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → ∀𝑛 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
164 | 163 | reximdva 3165 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
165 | 164 | ralimdva 3111 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ ℝ+
∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)(abs‘(𝐺‘𝑛)) < 𝑥 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥))) |
166 | 14, 165 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑛 ∈ (ℤ≥‘𝑗)((seq𝑀( + , 𝐹)‘𝑛) ∈ ℝ ∧ (abs‘((seq𝑀( + , 𝐹)‘𝑛) − (seq𝑀( + , 𝐹)‘𝑗))) < 𝑥)) |
167 | 1, 3, 166 | caurcvg2 14616 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |