Step | Hyp | Ref
| Expression |
1 | | nn0uz 11722 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11389 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → 0 ∈
ℤ) |
3 | | id 22 |
. . . 4
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℝ+) |
4 | | abelth.3 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
5 | | abelth.4 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑀) |
6 | 4, 5 | ge0p1rpd 11902 |
. . . 4
⊢ (𝜑 → (𝑀 + 1) ∈
ℝ+) |
7 | | rpdivcl 11856 |
. . . 4
⊢ ((𝑅 ∈ ℝ+
∧ (𝑀 + 1) ∈
ℝ+) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
8 | 3, 6, 7 | syl2anr 495 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
9 | | eqidd 2623 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ 𝑘 ∈ ℕ0)
→ (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑘)) |
10 | | abelth.7 |
. . . 4
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) |
11 | 10 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → seq0( +
, 𝐴) ⇝
0) |
12 | 1, 2, 8, 9, 11 | climi0 14243 |
. 2
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) →
∃𝑗 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1))) |
13 | 8 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
14 | | fzfid 12772 |
. . . . . . 7
⊢ (𝜑 → (0...(𝑗 − 1)) ∈ Fin) |
15 | | 0zd 11389 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
16 | | abelth.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
17 | 16 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ ℕ0) → (𝐴‘𝑤) ∈ ℂ) |
18 | 1, 15, 17 | serf 12829 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) |
19 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝑖 ∈ (0...(𝑗 − 1)) → 𝑖 ∈ ℕ0) |
20 | | ffvelrn 6357 |
. . . . . . . . 9
⊢ ((seq0( +
, 𝐴):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ) |
21 | 18, 19, 20 | syl2an 494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ) |
22 | 21 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → (abs‘(seq0( + ,
𝐴)‘𝑖)) ∈ ℝ) |
23 | 14, 22 | fsumrecl 14465 |
. . . . . 6
⊢ (𝜑 → Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ) |
24 | 23 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ) |
25 | 21 | absge0d 14183 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ (0...(𝑗 − 1))) → 0 ≤ (abs‘(seq0(
+ , 𝐴)‘𝑖))) |
26 | 14, 22, 25 | fsumge0 14527 |
. . . . . 6
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖))) |
27 | 26 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → 0 ≤ Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖))) |
28 | 24, 27 | ge0p1rpd 11902 |
. . . 4
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1) ∈
ℝ+) |
29 | 13, 28 | rpdivcld 11889 |
. . 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 24186 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
33 | 32 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 1 ∈ 𝑆) |
34 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 1 → (𝑥↑𝑛) = (1↑𝑛)) |
35 | | nn0z 11400 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
36 | | 1exp 12889 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ0
→ (1↑𝑛) =
1) |
38 | 34, 37 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → (𝑥↑𝑛) = 1) |
39 | 38 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 1 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑛) · 1)) |
40 | 39 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1)) |
41 | | abelth.6 |
. . . . . . . . . . . . . . . 16
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) |
42 | | sumex 14418 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · 1) ∈ V |
43 | 40, 41, 42 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
𝑆 → (𝐹‘1) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1)) |
44 | 33, 43 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘1) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1)) |
45 | 16 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) |
46 | 45 | mulid1d 10057 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · 1) = (𝐴‘𝑛)) |
47 | 46 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) = ((𝐴‘𝑛) · 1)) |
48 | 46, 45 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · 1) ∈
ℂ) |
49 | 1, 15, 47, 48, 10 | isumclim 14488 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · 1) = 0) |
50 | 44, 49 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘1) = 0) |
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘1) = 0) |
52 | 51 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1) − (𝐹‘𝑦)) = (0 − (𝐹‘𝑦))) |
53 | | df-neg 10269 |
. . . . . . . . . . 11
⊢ -(𝐹‘𝑦) = (0 − (𝐹‘𝑦)) |
54 | 52, 53 | syl6eqr 2674 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1) − (𝐹‘𝑦)) = -(𝐹‘𝑦)) |
55 | 54 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘-(𝐹‘𝑦))) |
56 | 16, 30, 4, 5, 31, 41 | abelthlem4 24188 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
57 | 56 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (𝐹‘𝑦) ∈ ℂ) |
58 | 57 | absnegd 14188 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘-(𝐹‘𝑦)) = (abs‘(𝐹‘𝑦))) |
59 | 55, 58 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘(𝐹‘𝑦))) |
60 | 59 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘(𝐹‘𝑦))) |
61 | 60 | ad2ant2r 783 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) = (abs‘(𝐹‘𝑦))) |
62 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → 𝜑) |
63 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = 1 → (𝐹‘𝑦) = (𝐹‘1)) |
64 | 63, 50 | sylan9eqr 2678 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = 1) → (𝐹‘𝑦) = 0) |
65 | 64 | abs00bd 14031 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = 1) → (abs‘(𝐹‘𝑦)) = 0) |
66 | 62, 65 | sylan 488 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 = 1) → (abs‘(𝐹‘𝑦)) = 0) |
67 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → 𝑅 ∈
ℝ+) |
68 | 67 | rpgt0d 11875 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → 0 < 𝑅) |
69 | 68 | adantr 481 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 = 1) → 0 < 𝑅) |
70 | 66, 69 | eqbrtrd 4675 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 = 1) → (abs‘(𝐹‘𝑦)) < 𝑅) |
71 | 16 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝐴:ℕ0⟶ℂ) |
72 | 30 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → seq0( + , 𝐴) ∈ dom ⇝ ) |
73 | 4 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑀 ∈ ℝ) |
74 | 5 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 0 ≤ 𝑀) |
75 | 10 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → seq0( + , 𝐴) ⇝ 0) |
76 | | simprll 802 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑦 ∈ 𝑆) |
77 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑦 ≠ 1) |
78 | | eldifsn 4317 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) |
79 | 76, 77, 78 | sylanbrc 698 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑦 ∈ (𝑆 ∖ {1})) |
80 | 8 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (𝑅 / (𝑀 + 1)) ∈
ℝ+) |
81 | | simplrl 800 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → 𝑗 ∈ ℕ0) |
82 | | simplrr 801 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1))) |
83 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑚)) |
84 | 83 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑚))) |
85 | 84 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)) ↔ (abs‘(seq0( + , 𝐴)‘𝑚)) < (𝑅 / (𝑀 + 1)))) |
86 | 85 | cbvralv 3171 |
. . . . . . . . . . 11
⊢
(∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < (𝑅 / (𝑀 + 1))) |
87 | 82, 86 | sylib 208 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < (𝑅 / (𝑀 + 1))) |
88 | | simprlr 803 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) |
89 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 𝑛 → (seq0( + , 𝐴)‘𝑖) = (seq0( + , 𝐴)‘𝑛)) |
90 | 89 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑖)) = (abs‘(seq0( + , 𝐴)‘𝑛))) |
91 | 90 | cbvsumv 14426 |
. . . . . . . . . . . . 13
⊢
Σ𝑖 ∈
(0...(𝑗 −
1))(abs‘(seq0( + , 𝐴)‘𝑖)) = Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) |
92 | 91 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢
(Σ𝑖 ∈
(0...(𝑗 −
1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1) = (Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) |
93 | 92 | oveq2i 6661 |
. . . . . . . . . . 11
⊢ ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) = ((𝑅 / (𝑀 + 1)) / (Σ𝑛 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
94 | 88, 93 | syl6breq 4694 |
. . . . . . . . . 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 24192 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(𝐹‘𝑦)) < ((𝑀 + 1) · (𝑅 / (𝑀 + 1)))) |
96 | | rpcn 11841 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ ℝ+
→ 𝑅 ∈
ℂ) |
97 | 96 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → 𝑅 ∈
ℂ) |
98 | 6 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑀 + 1) ∈
ℝ+) |
99 | 98 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑀 + 1) ∈
ℂ) |
100 | 98 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → (𝑀 + 1) ≠ 0) |
101 | 97, 99, 100 | divcan2d 10803 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) → ((𝑀 + 1) · (𝑅 / (𝑀 + 1))) = 𝑅) |
102 | 101 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → ((𝑀 + 1) · (𝑅 / (𝑀 + 1))) = 𝑅) |
103 | 95, 102 | breqtrd 4679 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ ((𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1))) ∧ 𝑦 ≠ 1)) → (abs‘(𝐹‘𝑦)) < 𝑅) |
104 | 103 | anassrs 680 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑅 ∈ ℝ+)
∧ (𝑗 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) ∧ 𝑦 ≠ 1) → (abs‘(𝐹‘𝑦)) < 𝑅) |
105 | 70, 104 | pm2.61dane 2881 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → (abs‘(𝐹‘𝑦)) < 𝑅) |
106 | 61, 105 | eqbrtrd 4675 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ (𝑦 ∈ 𝑆 ∧ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅) |
107 | 106 | expr 643 |
. . . 4
⊢ ((((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) ∧ 𝑦 ∈ 𝑆) → ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
108 | 107 | ralrimiva 2966 |
. . 3
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
109 | | breq2 4657 |
. . . . . 6
⊢ (𝑤 = ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → ((abs‘(1 − 𝑦)) < 𝑤 ↔ (abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)))) |
110 | 109 | imbi1d 331 |
. . . . 5
⊢ (𝑤 = ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅) ↔ ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))) |
111 | 110 | ralbidv 2986 |
. . . 4
⊢ (𝑤 = ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅) ↔ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < ((𝑅 / (𝑀 + 1)) / (Σ𝑖 ∈ (0...(𝑗 − 1))(abs‘(seq0( + , 𝐴)‘𝑖)) + 1)) → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅))) |
112 | 111 | rspcev 3309 |
. . 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 693 |
. 2
⊢ (((𝜑 ∧ 𝑅 ∈ ℝ+) ∧ (𝑗 ∈ ℕ0
∧ ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑘)) < (𝑅 / (𝑀 + 1)))) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |
114 | 12, 113 | rexlimddv 3035 |
1
⊢ ((𝜑 ∧ 𝑅 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑅)) |