Proof of Theorem abelthlem7
Step | Hyp | Ref
| Expression |
1 | | abelth.1 |
. . . . 5
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
2 | | abelth.2 |
. . . . 5
⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝
) |
3 | | abelth.3 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
4 | | abelth.4 |
. . . . 5
⊢ (𝜑 → 0 ≤ 𝑀) |
5 | | abelth.5 |
. . . . 5
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} |
6 | | abelth.6 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) |
7 | 1, 2, 3, 4, 5, 6 | abelthlem4 25591 |
. . . 4
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
8 | | abelthlem6.1 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) |
9 | 8 | eldifad 3904 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
10 | 7, 9 | ffvelrnd 6959 |
. . 3
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℂ) |
11 | 10 | abscld 15146 |
. 2
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ∈ ℝ) |
12 | | ax-1cn 10930 |
. . . . . 6
⊢ 1 ∈
ℂ |
13 | | abelth.7 |
. . . . . . . 8
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) |
14 | 1, 2, 3, 4, 5, 6, 13, 8 | abelthlem7a 25594 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 −
𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))) |
15 | 14 | simpld 495 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℂ) |
16 | | subcl 11220 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ 𝑋
∈ ℂ) → (1 − 𝑋) ∈ ℂ) |
17 | 12, 15, 16 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (1 − 𝑋) ∈
ℂ) |
18 | | fzfid 13691 |
. . . . . 6
⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin) |
19 | | elfznn0 13348 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0) |
20 | | nn0uz 12619 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
21 | | 0zd 12331 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
22 | 1 | ffvelrnda 6958 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) |
23 | 20, 21, 22 | serf 13749 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) |
24 | 23 | ffvelrnda 6958 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑛) ∈
ℂ) |
25 | | expcl 13798 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑋↑𝑛) ∈
ℂ) |
26 | 15, 25 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑋↑𝑛) ∈ ℂ) |
27 | 24, 26 | mulcld 10996 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
28 | 19, 27 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
29 | 18, 28 | fsumcl 15443 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
30 | 17, 29 | mulcld 10996 |
. . . 4
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
31 | 30 | abscld 15146 |
. . 3
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ∈ ℝ) |
32 | | eqid 2740 |
. . . . . 6
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
33 | | abelthlem7.3 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
34 | 33 | nn0zd 12423 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
35 | | eluznn0 12656 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0) |
36 | 33, 35 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0) |
37 | | fveq2 6771 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛)) |
38 | | oveq2 7279 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑋↑𝑘) = (𝑋↑𝑛)) |
39 | 37, 38 | oveq12d 7289 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
40 | | eqid 2740 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))) |
41 | | ovex 7304 |
. . . . . . . 8
⊢ ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ V |
42 | 39, 40, 41 | fvmpt 6872 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
43 | 36, 42 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
44 | 36, 27 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
45 | 1, 2, 3, 4, 5 | abelthlem2 25589 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
46 | 45 | simprd 496 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) |
47 | 46, 8 | sseldd 3927 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) |
48 | 1, 2, 3, 4, 5, 6, 13 | abelthlem5 25592 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , (𝑘
∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
49 | 47, 48 | mpdan 684 |
. . . . . . 7
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
50 | 42 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
51 | 50, 27 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
52 | 20, 33, 51 | iserex 15366 |
. . . . . . 7
⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )) |
53 | 49, 52 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
54 | 32, 34, 43, 44, 53 | isumcl 15471 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
55 | 17, 54 | mulcld 10996 |
. . . 4
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
56 | 55 | abscld 15146 |
. . 3
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ∈ ℝ) |
57 | 31, 56 | readdcld 11005 |
. 2
⊢ (𝜑 → ((abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) ∈ ℝ) |
58 | | peano2re 11148 |
. . . 4
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
59 | 3, 58 | syl 17 |
. . 3
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
60 | | abelthlem7.2 |
. . . 4
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
61 | 60 | rpred 12771 |
. . 3
⊢ (𝜑 → 𝑅 ∈ ℝ) |
62 | 59, 61 | remulcld 11006 |
. 2
⊢ (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ) |
63 | 1, 2, 3, 4, 5, 6, 13, 8 | abelthlem6 25593 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
64 | 20, 32, 33, 50, 27, 49 | isumsplit 15550 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
65 | 64 | oveq2d 7287 |
. . . . 5
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
66 | 17, 29, 54 | adddid 11000 |
. . . . 5
⊢ (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
67 | 63, 65, 66 | 3eqtrd 2784 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
68 | 67 | fveq2d 6775 |
. . 3
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))) |
69 | 30, 55 | abstrid 15166 |
. . 3
⊢ (𝜑 → (abs‘(((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))) |
70 | 68, 69 | eqbrtrd 5101 |
. 2
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))) |
71 | 3, 61 | remulcld 11006 |
. . . 4
⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℝ) |
72 | 17 | abscld 15146 |
. . . . . 6
⊢ (𝜑 → (abs‘(1 −
𝑋)) ∈
ℝ) |
73 | 24 | abscld 15146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ) |
74 | 19, 73 | sylan2 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + ,
𝐴)‘𝑛)) ∈ ℝ) |
75 | 18, 74 | fsumrecl 15444 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ) |
76 | | peano2re 11148 |
. . . . . . 7
⊢
(Σ𝑛 ∈
(0...(𝑁 −
1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ) |
77 | 75, 76 | syl 17 |
. . . . . 6
⊢ (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ) |
78 | 72, 77 | remulcld 11006 |
. . . . 5
⊢ (𝜑 → ((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ) |
79 | 17, 29 | absmuld 15164 |
. . . . . 6
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = ((abs‘(1 − 𝑋)) ·
(abs‘Σ𝑛 ∈
(0...(𝑁 − 1))((seq0(
+ , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
80 | 29 | abscld 15146 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
81 | 17 | absge0d 15154 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (abs‘(1
− 𝑋))) |
82 | 27 | abscld 15146 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
83 | 19, 82 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
84 | 18, 83 | fsumrecl 15444 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
85 | 18, 28 | fsumabs 15511 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
86 | 15 | abscld 15146 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
87 | | reexpcl 13797 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘𝑋)
∈ ℝ ∧ 𝑛
∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ) |
88 | 86, 87 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘𝑋)↑𝑛) ∈
ℝ) |
89 | | 1red 10977 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 1 ∈
ℝ) |
90 | 24 | absge0d 15154 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(abs‘(seq0( + , 𝐴)‘𝑛))) |
91 | 86 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘𝑋) ∈
ℝ) |
92 | 15 | absge0d 15154 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ (abs‘𝑋)) |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(abs‘𝑋)) |
94 | | 0cn 10968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℂ |
95 | | eqid 2740 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) |
96 | 95 | cnmetdval 23932 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑋(abs
∘ − )0) = (abs‘(𝑋 − 0))) |
97 | 15, 94, 96 | sylancl 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0))) |
98 | 15 | subid1d 11321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑋 − 0) = 𝑋) |
99 | 98 | fveq2d 6775 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋)) |
100 | 97, 99 | eqtrd 2780 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋)) |
101 | | cnxmet 23934 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
102 | | 1xr 11035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
103 | | elbl3 23543 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) |
104 | 101, 102,
103 | mpanl12 699 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℂ ∧ 𝑋
∈ ℂ) → (𝑋
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) <
1)) |
105 | 94, 15, 104 | sylancr 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) |
106 | 47, 105 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋(abs ∘ − )0) <
1) |
107 | 100, 106 | eqbrtrrd 5103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝑋) < 1) |
108 | | 1re 10976 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
109 | | ltle 11064 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1)) |
110 | 86, 108, 109 | sylancl 586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1)) |
111 | 107, 110 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝑋) ≤ 1) |
112 | 111 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘𝑋) ≤
1) |
113 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
114 | | exple1 13892 |
. . . . . . . . . . . . . . 15
⊢
((((abs‘𝑋)
∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) →
((abs‘𝑋)↑𝑛) ≤ 1) |
115 | 91, 93, 112, 113, 114 | syl31anc 1372 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘𝑋)↑𝑛) ≤ 1) |
116 | 88, 89, 73, 90, 115 | lemul2ad 11915 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1)) |
117 | 24, 26 | absmuld 15164 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋↑𝑛)))) |
118 | | absexp 15014 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (abs‘(𝑋↑𝑛)) = ((abs‘𝑋)↑𝑛)) |
119 | 15, 118 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘(𝑋↑𝑛)) = ((abs‘𝑋)↑𝑛)) |
120 | 119 | oveq2d 7287 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛))) |
121 | 117, 120 | eqtr2d 2781 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
122 | 73 | recnd 11004 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ) |
123 | 122 | mulid1d 10993 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛))) |
124 | 116, 121,
123 | 3brtr3d 5110 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛))) |
125 | 19, 124 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛))) |
126 | 18, 83, 74, 125 | fsumle 15509 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛))) |
127 | 80, 84, 75, 85, 126 | letrd 11132 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛))) |
128 | 75 | ltp1d 11905 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
129 | 80, 75, 77, 127, 128 | lelttrd 11133 |
. . . . . . . 8
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
130 | 80, 77, 129 | ltled 11123 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
131 | 80, 77, 72, 81, 130 | lemul2ad 11915 |
. . . . . 6
⊢ (𝜑 → ((abs‘(1 −
𝑋)) ·
(abs‘Σ𝑛 ∈
(0...(𝑁 − 1))((seq0(
+ , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
132 | 79, 131 | eqbrtrd 5101 |
. . . . 5
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
133 | | abelthlem7.5 |
. . . . . 6
⊢ (𝜑 → (abs‘(1 −
𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
134 | | 0red 10979 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
135 | 19, 90 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤
(abs‘(seq0( + , 𝐴)‘𝑛))) |
136 | 18, 74, 135 | fsumge0 15505 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛))) |
137 | 134, 75, 77, 136, 128 | lelttrd 11133 |
. . . . . . 7
⊢ (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
138 | | ltmuldiv 11848 |
. . . . . . 7
⊢
(((abs‘(1 − 𝑋)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ ∧ 0 <
(Σ𝑛 ∈
(0...(𝑁 −
1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) → (((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))) |
139 | 72, 61, 77, 137, 138 | syl112anc 1373 |
. . . . . 6
⊢ (𝜑 → (((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))) |
140 | 133, 139 | mpbird 256 |
. . . . 5
⊢ (𝜑 → ((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅) |
141 | 31, 78, 61, 132, 140 | lelttrd 11133 |
. . . 4
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) < 𝑅) |
142 | 17, 54 | absmuld 15164 |
. . . . 5
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = ((abs‘(1 − 𝑋)) ·
(abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
143 | 54 | abscld 15146 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
144 | 39 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
145 | | eqid 2740 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) = (𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) |
146 | | fvex 6784 |
. . . . . . . . . 10
⊢
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ V |
147 | 144, 145,
146 | fvmpt 6872 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
148 | 36, 147 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
149 | 44 | abscld 15146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
150 | | uzid 12596 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
151 | 34, 150 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑁)) |
152 | | oveq2 7279 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛)) |
153 | | eqid 2740 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘)) |
154 | | ovex 7304 |
. . . . . . . . . . . 12
⊢
((abs‘𝑋)↑𝑛) ∈ V |
155 | 152, 153,
154 | fvmpt 6872 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛)) |
156 | 36, 155 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛)) |
157 | 36, 88 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ) |
158 | 156, 157 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ) |
159 | 149 | recnd 11004 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
160 | 148, 159 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) ∈ ℂ) |
161 | 86 | recnd 11004 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑋) ∈
ℂ) |
162 | | absidm 15033 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ →
(abs‘(abs‘𝑋)) =
(abs‘𝑋)) |
163 | 15, 162 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(abs‘(abs‘𝑋)) =
(abs‘𝑋)) |
164 | 163, 107 | eqbrtrd 5101 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(abs‘𝑋))
< 1) |
165 | 161, 164,
33, 156 | geolim2 15581 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) |
166 | | seqex 13721 |
. . . . . . . . . . 11
⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ∈ V |
167 | | ovex 7304 |
. . . . . . . . . . 11
⊢
(((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V |
168 | 166, 167 | breldm 5816 |
. . . . . . . . . 10
⊢ (seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ∈ dom ⇝
) |
169 | 165, 168 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ∈ dom ⇝
) |
170 | 117, 120 | eqtrd 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛))) |
171 | 36, 170 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛))) |
172 | 36, 73 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) ∈ ℝ) |
173 | 61 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑅 ∈ ℝ) |
174 | 86 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘𝑋) ∈
ℝ) |
175 | 92 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤
(abs‘𝑋)) |
176 | 174, 36, 175 | expge0d 13880 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤
((abs‘𝑋)↑𝑛)) |
177 | | abelthlem7.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅) |
178 | 37 | fveq2d 6775 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛))) |
179 | 178 | breq1d 5089 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)) |
180 | 179 | rspccva 3560 |
. . . . . . . . . . . . . 14
⊢
((∀𝑘 ∈
(ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) < 𝑅) |
181 | 177, 180 | sylan 580 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) < 𝑅) |
182 | 172, 173,
181 | ltled 11123 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) ≤ 𝑅) |
183 | 172, 173,
157, 176, 182 | lemul1ad 11914 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((abs‘(seq0( + ,
𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛))) |
184 | 171, 183 | eqbrtrd 5101 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛))) |
185 | 148 | fveq2d 6775 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
186 | | absidm 15033 |
. . . . . . . . . . . 12
⊢ (((seq0(
+ , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ →
(abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
187 | 44, 186 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) →
(abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
188 | 185, 187 | eqtrd 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
189 | 156 | oveq2d 7287 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
190 | 184, 188,
189 | 3brtr4d 5111 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛))) |
191 | 32, 151, 158, 160, 169, 61, 190 | cvgcmpce 15528 |
. . . . . . . 8
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ∈ dom ⇝ ) |
192 | 32, 34, 148, 149, 191 | isumrecl 15475 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
193 | | eldifsni 4729 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1) |
194 | 8, 193 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≠ 1) |
195 | 194 | necomd 3001 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 𝑋) |
196 | | subeq0 11247 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝑋
∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋)) |
197 | 196 | necon3bid 2990 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ 𝑋
∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋)) |
198 | 12, 15, 197 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋)) |
199 | 195, 198 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → (1 − 𝑋) ≠ 0) |
200 | 17, 199 | absrpcld 15158 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(1 −
𝑋)) ∈
ℝ+) |
201 | 71, 200 | rerpdivcld 12802 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ) |
202 | 32, 34, 43, 44, 53 | isumclim2 15468 |
. . . . . . . 8
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))) ⇝ Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
203 | 32, 34, 148, 159, 191 | isumclim2 15468 |
. . . . . . . 8
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
204 | 36, 51 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
205 | 43 | fveq2d 6775 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
206 | 148, 205 | eqtr4d 2783 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛))) |
207 | 32, 202, 203, 34, 204, 206 | iserabs 15525 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
208 | 86, 33 | reexpcld 13879 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ) |
209 | | difrp 12767 |
. . . . . . . . . . . 12
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈
ℝ+)) |
210 | 86, 108, 209 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝑋) < 1 ↔ (1 −
(abs‘𝑋)) ∈
ℝ+)) |
211 | 107, 210 | mpbid 231 |
. . . . . . . . . 10
⊢ (𝜑 → (1 −
(abs‘𝑋)) ∈
ℝ+) |
212 | 208, 211 | rerpdivcld 12802 |
. . . . . . . . 9
⊢ (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ) |
213 | 61, 212 | remulcld 11006 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ) |
214 | 152 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
215 | | eqid 2740 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ (𝑅 ·
((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) |
216 | | ovex 7304 |
. . . . . . . . . . . 12
⊢ (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V |
217 | 214, 215,
216 | fvmpt 6872 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
218 | 36, 217 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
219 | 173, 157 | remulcld 11006 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ) |
220 | 60 | rpcnd 12773 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ ℂ) |
221 | 158 | recnd 11004 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ) |
222 | 218, 189 | eqtr4d 2783 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛))) |
223 | 32, 34, 220, 165, 221, 222 | isermulc2 15367 |
. . . . . . . . . . 11
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))) |
224 | | seqex 13721 |
. . . . . . . . . . . 12
⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V |
225 | | ovex 7304 |
. . . . . . . . . . . 12
⊢ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V |
226 | 224, 225 | breldm 5816 |
. . . . . . . . . . 11
⊢ (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ ) |
227 | 223, 226 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ ) |
228 | 32, 34, 148, 149, 218, 219, 184, 191, 227 | isumle 15554 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(𝑅 · ((abs‘𝑋)↑𝑛))) |
229 | 219 | recnd 11004 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ) |
230 | 32, 34, 218, 229, 223 | isumclim 15467 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))) |
231 | 228, 230 | breqtrd 5105 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))) |
232 | 60, 211 | rpdivcld 12788 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈
ℝ+) |
233 | 232 | rpred 12771 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ) |
234 | 208 | recnd 11004 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ) |
235 | 211 | rpcnd 12773 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 −
(abs‘𝑋)) ∈
ℂ) |
236 | 211 | rpne0d 12776 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 −
(abs‘𝑋)) ≠
0) |
237 | 220, 234,
235, 236 | div12d 11787 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋))))) |
238 | | 1red 10977 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
239 | 232 | rpge0d 12775 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋)))) |
240 | | exple1 13892 |
. . . . . . . . . . . . 13
⊢
((((abs‘𝑋)
∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) →
((abs‘𝑋)↑𝑁) ≤ 1) |
241 | 86, 92, 111, 33, 240 | syl31anc 1372 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1) |
242 | 208, 238,
233, 239, 241 | lemul1ad 11914 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋))))) |
243 | 232 | rpcnd 12773 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ) |
244 | 243 | mulid2d 10994 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋)))) |
245 | 242, 244 | breqtrd 5105 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋)))) |
246 | 237, 245 | eqbrtrd 5101 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋)))) |
247 | 14 | simprd 496 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(1 −
𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))) |
248 | | resubcl 11285 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 −
(abs‘𝑋)) ∈
ℝ) |
249 | 108, 86, 248 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 −
(abs‘𝑋)) ∈
ℝ) |
250 | 3, 249 | remulcld 11006 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈
ℝ) |
251 | 72, 250, 60 | lemul2d 12815 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘(1 −
𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))) |
252 | 247, 251 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))) |
253 | 3 | recnd 11004 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℂ) |
254 | 220, 253,
235 | mul12d 11184 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋))))) |
255 | 220, 235 | mulcomd 10997 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 −
(abs‘𝑋)) ·
𝑅)) |
256 | 255 | oveq2d 7287 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅))) |
257 | 253, 235,
220 | mul12d 11184 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅))) |
258 | 254, 256,
257 | 3eqtrd 2784 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅))) |
259 | 252, 258 | breqtrd 5105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅))) |
260 | 249, 71 | remulcld 11006 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅)) ∈
ℝ) |
261 | 61, 260, 200 | lemuldivd 12820 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))) |
262 | 259, 261 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))) |
263 | 71 | recnd 11004 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℂ) |
264 | 72 | recnd 11004 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(1 −
𝑋)) ∈
ℂ) |
265 | 200 | rpne0d 12776 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(1 −
𝑋)) ≠
0) |
266 | 235, 263,
264, 265 | divassd 11786 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 −
(abs‘𝑋)) ·
((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))) |
267 | 262, 266 | breqtrd 5105 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))) |
268 | | posdif 11468 |
. . . . . . . . . . . . 13
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 −
(abs‘𝑋)))) |
269 | 86, 108, 268 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1
− (abs‘𝑋)))) |
270 | 107, 269 | mpbid 231 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (1 −
(abs‘𝑋))) |
271 | | ledivmul 11851 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 −
(abs‘𝑋)) ∈
ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))) |
272 | 61, 201, 249, 270, 271 | syl112anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))) |
273 | 267, 272 | mpbird 256 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
274 | 213, 233,
201, 246, 273 | letrd 11132 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
275 | 192, 213,
201, 231, 274 | letrd 11132 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
276 | 143, 192,
201, 207, 275 | letrd 11132 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
277 | 143, 71, 200 | lemuldiv2d 12821 |
. . . . . 6
⊢ (𝜑 → (((abs‘(1 −
𝑋)) ·
(abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))) |
278 | 276, 277 | mpbird 256 |
. . . . 5
⊢ (𝜑 → ((abs‘(1 −
𝑋)) ·
(abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅)) |
279 | 142, 278 | eqbrtrd 5101 |
. . . 4
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅)) |
280 | 31, 56, 61, 71, 141, 279 | ltleaddd 11596 |
. . 3
⊢ (𝜑 → ((abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) < (𝑅 + (𝑀 · 𝑅))) |
281 | | 1cnd 10971 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
282 | 253, 281,
220 | adddird 11001 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅))) |
283 | 220 | mulid2d 10994 |
. . . . 5
⊢ (𝜑 → (1 · 𝑅) = 𝑅) |
284 | 283 | oveq2d 7287 |
. . . 4
⊢ (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅)) |
285 | 263, 220 | addcomd 11177 |
. . . 4
⊢ (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅))) |
286 | 282, 284,
285 | 3eqtrd 2784 |
. . 3
⊢ (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅))) |
287 | 280, 286 | breqtrrd 5107 |
. 2
⊢ (𝜑 → ((abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) < ((𝑀 + 1) · 𝑅)) |
288 | 11, 57, 62, 70, 287 | lelttrd 11133 |
1
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) < ((𝑀 + 1) · 𝑅)) |