Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11266 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → 0 ∈
ℤ) |
3 | | id 22 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ+) |
4 | | abelth.3 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
5 | | abelth.4 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑀) |
6 | 4, 5 | ge0p1rpd 11778 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈
ℝ+) |
7 | | rpdivcl 11732 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ (𝑀 + 1) ∈
ℝ+) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
8 | 3, 6, 7 | syl2anr 494 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
9 | | eqidd 2611 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0)
→ (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑘)) |
10 | | abelth.7 |
. . . 4
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) |
11 | 10 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → seq0( +
, 𝐴) ⇝
0) |
12 | 1, 2, 8, 9, 11 | climi0 14091 |
. 2
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) →
∃𝑗 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1))) |
13 | 8 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
14 | | fzfid 12634 |
. . . . . . 7
⊢ (𝜑 → (0...(𝑗 − 1)) ∈ Fin) |
15 | | 0zd 11266 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
16 | | abelth.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
17 | 16 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ0) → (𝐴‘𝑤) ∈ ℂ) |
18 | 1, 15, 17 | serf 12691 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) |
19 | | elfznn0 12302 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0...(𝑗 − 1)) → 𝑖 ∈ ℕ0) |
20 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ ((seq0( +
, 𝐴):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ) |
21 | 18, 19, 20 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ) |
22 | 21 | abscld 14023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (abs‘(seq0( + ,
𝐴)‘𝑖)) ∈ ℝ) |
23 | 14, 22 | fsumrecl 14312 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ) |
24 | 23 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ) |
25 | 21 | absge0d 14031 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → 0 ≤ (abs‘(seq0(
+ , 𝐴)‘𝑖))) |
26 | 14, 22, 25 | fsumge0 14368 |
. . . . . 6
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖))) |
27 | 26 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → 0 ≤ Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖))) |
28 | 24, 27 | ge0p1rpd 11778 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1) ∈
ℝ+) |
29 | 13, 28 | rpdivcld 11765 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) ∈
ℝ+) |
30 | | abelth.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝
) |
31 | | abelth.5 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} |
32 | 16, 30, 4, 5, 31 | abelthlem2 23990 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
33 | 32 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈ 𝑆) |
34 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 1 → (𝑥↑𝑛) = (1↑𝑛)) |
35 | | nn0z 11277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
36 | | 1exp 12751 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
→ (1↑𝑛) =
1) |
38 | 34, 37 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → (𝑥↑𝑛) = 1) |
39 | 38 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑛) · 1)) |
40 | 39 | sumeq2dv 14281 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1)) |
41 | | abelth.6 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) |
42 | | sumex 14266 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · 1) ∈ V |
43 | 40, 41, 42 | fvmpt 6191 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
𝑆 → (𝐹‘1) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1)) |
44 | 33, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘1) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1)) |
45 | 16 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) |
46 | 45 | mulid1d 9936 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · 1) = (𝐴‘𝑛)) |
47 | 46 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) = ((𝐴‘𝑛) · 1)) |
48 | 46, 45 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · 1) ∈
ℂ) |
49 | 1, 15, 47, 48, 10 | isumclim 14330 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1) = 0) |
50 | 44, 49 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘1) = 0) |
51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘1) = 0) |
52 | 51 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1) − (𝐹‘𝑦)) = (0 − (𝐹‘𝑦))) |
53 | | df-neg 10148 |
. . . . . . . . . . 11
⊢ -(𝐹‘𝑦) = (0 − (𝐹‘𝑦)) |
54 | 52, 53 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1) − (𝐹‘𝑦)) = -(𝐹‘𝑦)) |
55 | 54 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘-(𝐹‘𝑦))) |
56 | 16, 30, 4, 5, 31, 41 | abelthlem4 23992 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
57 | 56 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘𝑦) ∈ ℂ) |
58 | 57 | absnegd 14036 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘-(𝐹‘𝑦)) = (abs‘(𝐹‘𝑦))) |
59 | 55, 58 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘(𝐹‘𝑦))) |
60 | 59 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘(𝐹‘𝑦))) |
61 | 60 | ad2ant2r 779 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘(𝐹‘𝑦))) |
62 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → 𝜑) |
63 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (𝐹‘𝑦) = (𝐹‘1)) |
64 | 63, 50 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = 1) → (𝐹‘𝑦) = 0) |
65 | 64 | abs00bd 13879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 1) → (abs‘(𝐹‘𝑦)) = 0) |
66 | 62, 65 | sylan 487 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 = 1) → (abs‘(𝐹‘𝑦)) = 0) |
67 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → 𝑅 ∈
ℝ+) |
68 | 67 | rpgt0d 11751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → 0 < 𝑅) |
69 | 68 | adantr 480 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 = 1) → 0 < 𝑅) |
70 | 66, 69 | eqbrtrd 4605 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 = 1) → (abs‘(𝐹‘𝑦)) < 𝑅) |
71 | 16 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝐴:ℕ0⟶ℂ) |
72 | 30 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → seq0( + , 𝐴) ∈ dom ⇝ ) |
73 | 4 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑀 ∈ ℝ) |
74 | 5 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 0 ≤ 𝑀) |
75 | 10 | ad3antrrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → seq0( + , 𝐴) ⇝ 0) |
76 | | simprll 798 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑦 ∈ 𝑆) |
77 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑦 ≠ 1) |
78 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) |
79 | 76, 77, 78 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑦 ∈ (𝑆 ∖ {1})) |
80 | 8 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
81 | | simplrl 796 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑗 ∈ ℕ0) |
82 | | simplrr 797 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1))) |
83 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑚)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑚))) |
85 | 84 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)) ↔ (abs‘(seq0( + , 𝐴)‘𝑚)) < (𝑅 / (𝑀 + 1)))) |
86 | 85 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < (𝑅 / (𝑀 + 1))) |
87 | 82, 86 | sylib 207 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < (𝑅 / (𝑀 + 1))) |
88 | | simprlr 799 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) |
89 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → (seq0( + , 𝐴)‘𝑖) = (seq0( + , 𝐴)‘𝑛)) |
90 | 89 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑖)) = (abs‘(seq0( + , 𝐴)‘𝑛))) |
91 | 90 | cbvsumv 14274 |
. . . . . . . . . . . . 13
⊢
Σ𝑖 ∈
(0...(𝑗 −
1))(abs‘(seq0( + , 𝐴)‘𝑖)) = Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) |
92 | 91 | oveq1i 6559 |
. . . . . . . . . . . 12
⊢
(Σ𝑖 ∈
(0...(𝑗 −
1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1) = (Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) |
93 | 92 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) = ((𝑅 / (𝑀 + 1)) / (Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
94 | 88, 93 | syl6breq 4624 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
95 | 71, 72, 73, 74, 31, 41, 75, 79, 80, 81, 87, 94 | abelthlem7 23996 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(𝐹‘𝑦)) < ((𝑀 + 1) · (𝑅 / (𝑀 + 1)))) |
96 | | rpcn 11717 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
97 | 96 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → 𝑅 ∈
ℂ) |
98 | 6 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑀 + 1) ∈
ℝ+) |
99 | 98 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑀 + 1) ∈
ℂ) |
100 | 98 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑀 + 1) ≠ 0) |
101 | 97, 99, 100 | divcan2d 10682 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ((𝑀 + 1) · (𝑅 / (𝑀 + 1))) = 𝑅) |
102 | 101 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → ((𝑀 + 1) · (𝑅 / (𝑀 + 1))) = 𝑅) |
103 | 95, 102 | breqtrd 4609 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(𝐹‘𝑦)) < 𝑅) |
104 | 103 | anassrs 678 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 ≠ 1) → (abs‘(𝐹‘𝑦)) < 𝑅) |
105 | 70, 104 | pm2.61dane 2869 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → (abs‘(𝐹‘𝑦)) < 𝑅) |
106 | 61, 105 | eqbrtrd 4605 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅) |
107 | 106 | expr 641 |
. . . 4
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ 𝑦 ∈ 𝑆) → ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
108 | 107 | ralrimiva 2949 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
109 | | breq2 4587 |
. . . . . 6
⊢ (𝑤 = ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → ((abs‘(1 − 𝑦)) < 𝑤 ↔ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) |
110 | 109 | imbi1d 330 |
. . . . 5
⊢ (𝑤 = ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅) ↔ ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))) |
111 | 110 | ralbidv 2969 |
. . . 4
⊢ (𝑤 = ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅) ↔ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))) |
112 | 111 | rspcev 3282 |
. . 3
⊢ ((((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) ∈ ℝ+ ∧
∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
113 | 29, 108, 112 | syl2anc 691 |
. 2
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
114 | 12, 113 | rexlimddv 3017 |
1
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |