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 24625 |
. . . 4
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
8 | | abelthlem6.1 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) |
9 | 8 | eldifad 3804 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
10 | 7, 9 | ffvelrnd 6624 |
. . 3
⊢ (𝜑 → (𝐹‘𝑋) ∈ ℂ) |
11 | 10 | abscld 14583 |
. 2
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ∈ ℝ) |
12 | | ax-1cn 10330 |
. . . . . 6
⊢ 1 ∈
ℂ |
13 | | abelth.7 |
. . . . . . . 8
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) |
14 | 1, 2, 3, 4, 5, 6, 13, 8 | abelthlem7a 24628 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 −
𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))) |
15 | 14 | simpld 490 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ ℂ) |
16 | | subcl 10621 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ 𝑋
∈ ℂ) → (1 − 𝑋) ∈ ℂ) |
17 | 12, 15, 16 | sylancr 581 |
. . . . 5
⊢ (𝜑 → (1 − 𝑋) ∈
ℂ) |
18 | | fzfid 13091 |
. . . . . 6
⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin) |
19 | | elfznn0 12751 |
. . . . . . 7
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0) |
20 | | nn0uz 12028 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
21 | | 0zd 11740 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℤ) |
22 | 1 | ffvelrnda 6623 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) |
23 | 20, 21, 22 | serf 13147 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) |
24 | 23 | ffvelrnda 6623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑛) ∈
ℂ) |
25 | | expcl 13196 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑋↑𝑛) ∈
ℂ) |
26 | 15, 25 | sylan 575 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑋↑𝑛) ∈ ℂ) |
27 | 24, 26 | mulcld 10397 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
28 | 19, 27 | sylan2 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
29 | 18, 28 | fsumcl 14871 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
30 | 17, 29 | mulcld 10397 |
. . . 4
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
31 | 30 | abscld 14583 |
. . 3
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ∈ ℝ) |
32 | | eqid 2778 |
. . . . . 6
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
33 | | abelthlem7.3 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
34 | 33 | nn0zd 11832 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
35 | | eluznn0 12064 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0) |
36 | 33, 35 | sylan 575 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0) |
37 | | fveq2 6446 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛)) |
38 | | oveq2 6930 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (𝑋↑𝑘) = (𝑋↑𝑛)) |
39 | 37, 38 | oveq12d 6940 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
40 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))) |
41 | | ovex 6954 |
. . . . . . . 8
⊢ ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ V |
42 | 39, 40, 41 | fvmpt 6542 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
43 | 36, 42 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
44 | 36, 27 | syldan 585 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
45 | 1, 2, 3, 4, 5 | abelthlem2 24623 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
46 | 45 | simprd 491 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) |
47 | 46, 8 | sseldd 3822 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) |
48 | 1, 2, 3, 4, 5, 6, 13 | abelthlem5 24626 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , (𝑘
∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
49 | 47, 48 | mpdan 677 |
. . . . . . 7
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
50 | 42 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
51 | 50, 27 | eqeltrd 2859 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
52 | 20, 33, 51 | iserex 14795 |
. . . . . . 7
⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ )) |
53 | 49, 52 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
54 | 32, 34, 43, 44, 53 | isumcl 14897 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
55 | 17, 54 | mulcld 10397 |
. . . 4
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
56 | 55 | abscld 14583 |
. . 3
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ∈ ℝ) |
57 | 31, 56 | readdcld 10406 |
. 2
⊢ (𝜑 → ((abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) ∈ ℝ) |
58 | | peano2re 10549 |
. . . 4
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
59 | 3, 58 | syl 17 |
. . 3
⊢ (𝜑 → (𝑀 + 1) ∈ ℝ) |
60 | | abelthlem7.2 |
. . . 4
⊢ (𝜑 → 𝑅 ∈
ℝ+) |
61 | 60 | rpred 12181 |
. . 3
⊢ (𝜑 → 𝑅 ∈ ℝ) |
62 | 59, 61 | remulcld 10407 |
. 2
⊢ (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ) |
63 | 1, 2, 3, 4, 5, 6, 13, 8 | abelthlem6 24627 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
64 | 20, 32, 33, 50, 27, 49 | isumsplit 14976 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
65 | 64 | oveq2d 6938 |
. . . . 5
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
66 | 17, 29, 54 | adddid 10401 |
. . . . 5
⊢ (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) + Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
67 | 63, 65, 66 | 3eqtrd 2818 |
. . . 4
⊢ (𝜑 → (𝐹‘𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
68 | 67 | fveq2d 6450 |
. . 3
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))) |
69 | 30, 55 | abstrid 14603 |
. . 3
⊢ (𝜑 → (abs‘(((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))) |
70 | 68, 69 | eqbrtrd 4908 |
. 2
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))))) |
71 | 3, 61 | remulcld 10407 |
. . . 4
⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℝ) |
72 | 17 | abscld 14583 |
. . . . . 6
⊢ (𝜑 → (abs‘(1 −
𝑋)) ∈
ℝ) |
73 | 24 | abscld 14583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ) |
74 | 19, 73 | sylan2 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + ,
𝐴)‘𝑛)) ∈ ℝ) |
75 | 18, 74 | fsumrecl 14872 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ) |
76 | | peano2re 10549 |
. . . . . . 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 10407 |
. . . . 5
⊢ (𝜑 → ((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ) |
79 | 17, 29 | absmuld 14601 |
. . . . . 6
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = ((abs‘(1 − 𝑋)) ·
(abs‘Σ𝑛 ∈
(0...(𝑁 − 1))((seq0(
+ , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
80 | 29 | abscld 14583 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
81 | 17 | absge0d 14591 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (abs‘(1
− 𝑋))) |
82 | 27 | abscld 14583 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
83 | 19, 82 | sylan2 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
84 | 18, 83 | fsumrecl 14872 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
85 | 18, 28 | fsumabs 14937 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
86 | 15 | abscld 14583 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
87 | | reexpcl 13195 |
. . . . . . . . . . . . . . 15
⊢
(((abs‘𝑋)
∈ ℝ ∧ 𝑛
∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ) |
88 | 86, 87 | sylan 575 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘𝑋)↑𝑛) ∈
ℝ) |
89 | | 1red 10377 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 1 ∈
ℝ) |
90 | 24 | absge0d 14591 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(abs‘(seq0( + , 𝐴)‘𝑛))) |
91 | 86 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘𝑋) ∈
ℝ) |
92 | 15 | absge0d 14591 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ (abs‘𝑋)) |
93 | 92 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 0 ≤
(abs‘𝑋)) |
94 | | 0cn 10368 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ∈
ℂ |
95 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) = (abs ∘ − ) |
96 | 95 | cnmetdval 22982 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑋 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑋(abs
∘ − )0) = (abs‘(𝑋 − 0))) |
97 | 15, 94, 96 | sylancl 580 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0))) |
98 | 15 | subid1d 10723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑋 − 0) = 𝑋) |
99 | 98 | fveq2d 6450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋)) |
100 | 97, 99 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋)) |
101 | | cnxmet 22984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
102 | | 1rp 12141 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℝ+ |
103 | | rpxr 12148 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ* |
105 | | elbl3 22605 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) |
106 | 101, 104,
105 | mpanl12 692 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℂ ∧ 𝑋
∈ ℂ) → (𝑋
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) <
1)) |
107 | 94, 15, 106 | sylancr 581 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) |
108 | 47, 107 | mpbid 224 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋(abs ∘ − )0) <
1) |
109 | 100, 108 | eqbrtrrd 4910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (abs‘𝑋) < 1) |
110 | | 1re 10376 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℝ |
111 | | ltle 10465 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1)) |
112 | 86, 110, 111 | sylancl 580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1)) |
113 | 109, 112 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (abs‘𝑋) ≤ 1) |
114 | 113 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘𝑋) ≤
1) |
115 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
116 | | exple1 13238 |
. . . . . . . . . . . . . . 15
⊢
((((abs‘𝑋)
∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) →
((abs‘𝑋)↑𝑛) ≤ 1) |
117 | 91, 93, 114, 115, 116 | syl31anc 1441 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘𝑋)↑𝑛) ≤ 1) |
118 | 88, 89, 73, 90, 117 | lemul2ad 11318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1)) |
119 | 24, 26 | absmuld 14601 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋↑𝑛)))) |
120 | | absexp 14451 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (abs‘(𝑋↑𝑛)) = ((abs‘𝑋)↑𝑛)) |
121 | 15, 120 | sylan 575 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘(𝑋↑𝑛)) = ((abs‘𝑋)↑𝑛)) |
122 | 121 | oveq2d 6938 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛))) |
123 | 119, 122 | eqtr2d 2815 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
124 | 73 | recnd 10405 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ) |
125 | 124 | mulid1d 10394 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛))) |
126 | 118, 123,
125 | 3brtr3d 4917 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛))) |
127 | 19, 126 | sylan2 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛))) |
128 | 18, 83, 74, 127 | fsumle 14935 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛))) |
129 | 80, 84, 75, 85, 128 | letrd 10533 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛))) |
130 | 75 | ltp1d 11308 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
131 | 80, 75, 77, 129, 130 | lelttrd 10534 |
. . . . . . . 8
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
132 | 80, 77, 131 | ltled 10524 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
133 | 80, 77, 72, 81, 132 | lemul2ad 11318 |
. . . . . 6
⊢ (𝜑 → ((abs‘(1 −
𝑋)) ·
(abs‘Σ𝑛 ∈
(0...(𝑁 − 1))((seq0(
+ , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
134 | 79, 133 | eqbrtrd 4908 |
. . . . 5
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
135 | | abelthlem7.5 |
. . . . . 6
⊢ (𝜑 → (abs‘(1 −
𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) |
136 | | 0red 10380 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
137 | 19, 90 | sylan2 586 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤
(abs‘(seq0( + , 𝐴)‘𝑛))) |
138 | 18, 74, 137 | fsumge0 14931 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛))) |
139 | 136, 75, 77, 138, 130 | lelttrd 10534 |
. . . . . . 7
⊢ (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) |
140 | | ltmuldiv 11250 |
. . . . . . 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)))) |
141 | 72, 61, 77, 139, 140 | syl112anc 1442 |
. . . . . 6
⊢ (𝜑 → (((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))) |
142 | 135, 141 | mpbird 249 |
. . . . 5
⊢ (𝜑 → ((abs‘(1 −
𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅) |
143 | 31, 78, 61, 134, 142 | lelttrd 10534 |
. . . 4
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) < 𝑅) |
144 | 17, 54 | absmuld 14601 |
. . . . 5
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = ((abs‘(1 − 𝑋)) ·
(abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
145 | 54 | abscld 14583 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
146 | 39 | fveq2d 6450 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
147 | | eqid 2778 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) = (𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) |
148 | | fvex 6459 |
. . . . . . . . . 10
⊢
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ V |
149 | 146, 147,
148 | fvmpt 6542 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
150 | 36, 149 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
151 | 44 | abscld 14583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
152 | | uzid 12007 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
153 | 34, 152 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑁)) |
154 | | oveq2 6930 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛)) |
155 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘)) |
156 | | ovex 6954 |
. . . . . . . . . . . 12
⊢
((abs‘𝑋)↑𝑛) ∈ V |
157 | 154, 155,
156 | fvmpt 6542 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛)) |
158 | 36, 157 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛)) |
159 | 36, 88 | syldan 585 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ) |
160 | 158, 159 | eqeltrd 2859 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ) |
161 | 151 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
162 | 150, 161 | eqeltrd 2859 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) ∈ ℂ) |
163 | 86 | recnd 10405 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑋) ∈
ℂ) |
164 | | absidm 14470 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℂ →
(abs‘(abs‘𝑋)) =
(abs‘𝑋)) |
165 | 15, 164 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(abs‘(abs‘𝑋)) =
(abs‘𝑋)) |
166 | 165, 109 | eqbrtrd 4908 |
. . . . . . . . . . 11
⊢ (𝜑 →
(abs‘(abs‘𝑋))
< 1) |
167 | 163, 166,
33, 158 | geolim2 15006 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) |
168 | | seqex 13121 |
. . . . . . . . . . 11
⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ∈ V |
169 | | ovex 6954 |
. . . . . . . . . . 11
⊢
(((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V |
170 | 168, 169 | breldm 5574 |
. . . . . . . . . 10
⊢ (seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ∈ dom ⇝
) |
171 | 167, 170 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))) ∈ dom ⇝
) |
172 | 119, 122 | eqtrd 2814 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛))) |
173 | 36, 172 | syldan 585 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛))) |
174 | 36, 73 | syldan 585 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) ∈ ℝ) |
175 | 61 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 𝑅 ∈ ℝ) |
176 | 86 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘𝑋) ∈
ℝ) |
177 | 92 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤
(abs‘𝑋)) |
178 | 176, 36, 177 | expge0d 13345 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → 0 ≤
((abs‘𝑋)↑𝑛)) |
179 | | abelthlem7.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ (ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅) |
180 | 37 | fveq2d 6450 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛))) |
181 | 180 | breq1d 4896 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)) |
182 | 181 | rspccva 3510 |
. . . . . . . . . . . . . 14
⊢
((∀𝑘 ∈
(ℤ≥‘𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) < 𝑅) |
183 | 179, 182 | sylan 575 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) < 𝑅) |
184 | 174, 175,
183 | ltled 10524 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘(seq0( + ,
𝐴)‘𝑛)) ≤ 𝑅) |
185 | 174, 175,
159, 178, 184 | lemul1ad 11317 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((abs‘(seq0( + ,
𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛))) |
186 | 173, 185 | eqbrtrd 4908 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((seq0( + ,
𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛))) |
187 | 150 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
188 | | absidm 14470 |
. . . . . . . . . . . 12
⊢ (((seq0(
+ , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ →
(abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
189 | 44, 188 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) →
(abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
190 | 187, 189 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
191 | 158 | oveq2d 6938 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
192 | 186, 190,
191 | 3brtr4d 4918 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛))) |
193 | 32, 153, 160, 162, 171, 61, 192 | cvgcmpce 14954 |
. . . . . . . 8
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ∈ dom ⇝ ) |
194 | 32, 34, 150, 151, 193 | isumrecl 14901 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℝ) |
195 | | eldifsni 4553 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1) |
196 | 8, 195 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ≠ 1) |
197 | 196 | necomd 3024 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≠ 𝑋) |
198 | | subeq0 10649 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝑋
∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋)) |
199 | 198 | necon3bid 3013 |
. . . . . . . . . . 11
⊢ ((1
∈ ℂ ∧ 𝑋
∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋)) |
200 | 12, 15, 199 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋)) |
201 | 197, 200 | mpbird 249 |
. . . . . . . . 9
⊢ (𝜑 → (1 − 𝑋) ≠ 0) |
202 | 17, 201 | absrpcld 14595 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(1 −
𝑋)) ∈
ℝ+) |
203 | 71, 202 | rerpdivcld 12212 |
. . . . . . 7
⊢ (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ) |
204 | 32, 34, 43, 44, 53 | isumclim2 14894 |
. . . . . . . 8
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))) ⇝ Σ𝑛 ∈ (ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
205 | 32, 34, 150, 161, 193 | isumclim2 14894 |
. . . . . . . 8
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
206 | 36, 51 | syldan 585 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
207 | 43 | fveq2d 6450 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (abs‘((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
208 | 150, 207 | eqtr4d 2817 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
(abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛))) |
209 | 32, 204, 205, 34, 206, 208 | iserabs 14951 |
. . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
210 | 86, 33 | reexpcld 13344 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ) |
211 | | difrp 12177 |
. . . . . . . . . . . 12
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈
ℝ+)) |
212 | 86, 110, 211 | sylancl 580 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝑋) < 1 ↔ (1 −
(abs‘𝑋)) ∈
ℝ+)) |
213 | 109, 212 | mpbid 224 |
. . . . . . . . . 10
⊢ (𝜑 → (1 −
(abs‘𝑋)) ∈
ℝ+) |
214 | 210, 213 | rerpdivcld 12212 |
. . . . . . . . 9
⊢ (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ) |
215 | 61, 214 | remulcld 10407 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ) |
216 | 154 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
217 | | eqid 2778 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
↦ (𝑅 ·
((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) |
218 | | ovex 6954 |
. . . . . . . . . . . 12
⊢ (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V |
219 | 216, 217,
218 | fvmpt 6542 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
220 | 36, 219 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛))) |
221 | 175, 159 | remulcld 10407 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ) |
222 | 60 | rpcnd 12183 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑅 ∈ ℂ) |
223 | 160 | recnd 10405 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ) |
224 | 220, 191 | eqtr4d 2817 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑘))‘𝑛))) |
225 | 32, 34, 222, 167, 223, 224 | isermulc2 14796 |
. . . . . . . . . . 11
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))) |
226 | | seqex 13121 |
. . . . . . . . . . . 12
⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V |
227 | | ovex 6954 |
. . . . . . . . . . . 12
⊢ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V |
228 | 226, 227 | breldm 5574 |
. . . . . . . . . . 11
⊢ (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ ) |
229 | 225, 228 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ ) |
230 | 32, 34, 150, 151, 220, 221, 186, 193, 229 | isumle 14980 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ Σ𝑛 ∈ (ℤ≥‘𝑁)(𝑅 · ((abs‘𝑋)↑𝑛))) |
231 | 221 | recnd 10405 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ) |
232 | 32, 34, 220, 231, 225 | isumclim 14893 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))) |
233 | 230, 232 | breqtrd 4912 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))) |
234 | 60, 213 | rpdivcld 12198 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈
ℝ+) |
235 | 234 | rpred 12181 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ) |
236 | 210 | recnd 10405 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ) |
237 | 213 | rpcnd 12183 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 −
(abs‘𝑋)) ∈
ℂ) |
238 | 213 | rpne0d 12186 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 −
(abs‘𝑋)) ≠
0) |
239 | 222, 236,
237, 238 | div12d 11187 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋))))) |
240 | | 1red 10377 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℝ) |
241 | 234 | rpge0d 12185 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋)))) |
242 | | exple1 13238 |
. . . . . . . . . . . . 13
⊢
((((abs‘𝑋)
∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) →
((abs‘𝑋)↑𝑁) ≤ 1) |
243 | 86, 92, 113, 33, 242 | syl31anc 1441 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1) |
244 | 210, 240,
235, 241, 243 | lemul1ad 11317 |
. . . . . . . . . . 11
⊢ (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋))))) |
245 | 234 | rpcnd 12183 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ) |
246 | 245 | mulid2d 10395 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋)))) |
247 | 244, 246 | breqtrd 4912 |
. . . . . . . . . 10
⊢ (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋)))) |
248 | 239, 247 | eqbrtrd 4908 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋)))) |
249 | 14 | simprd 491 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (abs‘(1 −
𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))) |
250 | | resubcl 10687 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 −
(abs‘𝑋)) ∈
ℝ) |
251 | 110, 86, 250 | sylancr 581 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1 −
(abs‘𝑋)) ∈
ℝ) |
252 | 3, 251 | remulcld 10407 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈
ℝ) |
253 | 72, 252, 60 | lemul2d 12225 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((abs‘(1 −
𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))) |
254 | 249, 253 | mpbid 224 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))) |
255 | 3 | recnd 10405 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℂ) |
256 | 222, 255,
237 | mul12d 10585 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋))))) |
257 | 222, 237 | mulcomd 10398 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 −
(abs‘𝑋)) ·
𝑅)) |
258 | 257 | oveq2d 6938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅))) |
259 | 255, 237,
222 | mul12d 10585 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅))) |
260 | 256, 258,
259 | 3eqtrd 2818 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅))) |
261 | 254, 260 | breqtrd 4912 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅))) |
262 | 251, 71 | remulcld 10407 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅)) ∈
ℝ) |
263 | 61, 262, 202 | lemuldivd 12230 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))) |
264 | 261, 263 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))) |
265 | 71 | recnd 10405 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 · 𝑅) ∈ ℂ) |
266 | 72 | recnd 10405 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(1 −
𝑋)) ∈
ℂ) |
267 | 202 | rpne0d 12186 |
. . . . . . . . . . . 12
⊢ (𝜑 → (abs‘(1 −
𝑋)) ≠
0) |
268 | 237, 265,
266, 267 | divassd 11186 |
. . . . . . . . . . 11
⊢ (𝜑 → (((1 −
(abs‘𝑋)) ·
(𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 −
(abs‘𝑋)) ·
((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))) |
269 | 264, 268 | breqtrd 4912 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))) |
270 | | posdif 10868 |
. . . . . . . . . . . . 13
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 −
(abs‘𝑋)))) |
271 | 86, 110, 270 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1
− (abs‘𝑋)))) |
272 | 109, 271 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (1 −
(abs‘𝑋))) |
273 | | ledivmul 11253 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 −
(abs‘𝑋)) ∈
ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))) |
274 | 61, 203, 251, 272, 273 | syl112anc 1442 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))) |
275 | 269, 274 | mpbird 249 |
. . . . . . . . 9
⊢ (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
276 | 215, 235,
203, 248, 275 | letrd 10533 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
277 | 194, 215,
203, 233, 276 | letrd 10533 |
. . . . . . 7
⊢ (𝜑 → Σ𝑛 ∈ (ℤ≥‘𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
278 | 145, 194,
203, 209, 277 | letrd 10533 |
. . . . . 6
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))) |
279 | 145, 71, 202 | lemuldiv2d 12231 |
. . . . . 6
⊢ (𝜑 → (((abs‘(1 −
𝑋)) ·
(abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))) |
280 | 278, 279 | mpbird 249 |
. . . . 5
⊢ (𝜑 → ((abs‘(1 −
𝑋)) ·
(abs‘Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅)) |
281 | 144, 280 | eqbrtrd 4908 |
. . . 4
⊢ (𝜑 → (abs‘((1 −
𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) ≤ (𝑀 · 𝑅)) |
282 | 31, 56, 61, 71, 143, 281 | ltleaddd 10996 |
. . 3
⊢ (𝜑 → ((abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) < (𝑅 + (𝑀 · 𝑅))) |
283 | | 1cnd 10371 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
284 | 255, 283,
222 | adddird 10402 |
. . . 4
⊢ (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅))) |
285 | 222 | mulid2d 10395 |
. . . . 5
⊢ (𝜑 → (1 · 𝑅) = 𝑅) |
286 | 285 | oveq2d 6938 |
. . . 4
⊢ (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅)) |
287 | 265, 222 | addcomd 10578 |
. . . 4
⊢ (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅))) |
288 | 284, 286,
287 | 3eqtrd 2818 |
. . 3
⊢ (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅))) |
289 | 282, 288 | breqtrrd 4914 |
. 2
⊢ (𝜑 → ((abs‘((1 −
𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈
(ℤ≥‘𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) < ((𝑀 + 1) · 𝑅)) |
290 | 11, 57, 62, 70, 289 | lelttrd 10534 |
1
⊢ (𝜑 → (abs‘(𝐹‘𝑋)) < ((𝑀 + 1) · 𝑅)) |