Step |
Hyp |
Ref |
Expression |
1 |
|
abelth.1 |
⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ ) |
2 |
|
abelth.2 |
⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ ) |
3 |
|
abelth.3 |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
4 |
|
abelth.4 |
⊢ ( 𝜑 → 0 ≤ 𝑀 ) |
5 |
|
abelth.5 |
⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) } |
6 |
|
abelth.6 |
⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) |
7 |
|
abelth.7 |
⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ⇝ 0 ) |
8 |
|
abelthlem6.1 |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝑆 ∖ { 1 } ) ) |
9 |
|
abelthlem7.2 |
⊢ ( 𝜑 → 𝑅 ∈ ℝ+ ) |
10 |
|
abelthlem7.3 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ0 ) |
11 |
|
abelthlem7.4 |
⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅 ) |
12 |
|
abelthlem7.5 |
⊢ ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) |
13 |
1 2 3 4 5 6
|
abelthlem4 |
⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ ) |
14 |
8
|
eldifad |
⊢ ( 𝜑 → 𝑋 ∈ 𝑆 ) |
15 |
13 14
|
ffvelrnd |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℂ ) |
16 |
15
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ ) |
17 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
18 |
1 2 3 4 5 6 7 8
|
abelthlem7a |
⊢ ( 𝜑 → ( 𝑋 ∈ ℂ ∧ ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
19 |
18
|
simpld |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
20 |
|
subcl |
⊢ ( ( 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 1 − 𝑋 ) ∈ ℂ ) |
21 |
17 19 20
|
sylancr |
⊢ ( 𝜑 → ( 1 − 𝑋 ) ∈ ℂ ) |
22 |
|
fzfid |
⊢ ( 𝜑 → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin ) |
23 |
|
elfznn0 |
⊢ ( 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑛 ∈ ℕ0 ) |
24 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
25 |
|
0zd |
⊢ ( 𝜑 → 0 ∈ ℤ ) |
26 |
1
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑛 ) ∈ ℂ ) |
27 |
24 25 26
|
serf |
⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) : ℕ0 ⟶ ℂ ) |
28 |
27
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ∈ ℂ ) |
29 |
|
expcl |
⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑛 ) ∈ ℂ ) |
30 |
19 29
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( 𝑋 ↑ 𝑛 ) ∈ ℂ ) |
31 |
28 30
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ ) |
32 |
23 31
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ ) |
33 |
22 32
|
fsumcl |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ ) |
34 |
21 33
|
mulcld |
⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℂ ) |
35 |
34
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ∈ ℝ ) |
36 |
|
eqid |
⊢ ( ℤ≥ ‘ 𝑁 ) = ( ℤ≥ ‘ 𝑁 ) |
37 |
10
|
nn0zd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
38 |
|
eluznn0 |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℕ0 ) |
39 |
10 38
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑛 ∈ ℕ0 ) |
40 |
|
fveq2 |
⊢ ( 𝑘 = 𝑛 → ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) = ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) |
41 |
|
oveq2 |
⊢ ( 𝑘 = 𝑛 → ( 𝑋 ↑ 𝑘 ) = ( 𝑋 ↑ 𝑛 ) ) |
42 |
40 41
|
oveq12d |
⊢ ( 𝑘 = 𝑛 → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) |
43 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) |
44 |
|
ovex |
⊢ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ V |
45 |
42 43 44
|
fvmpt |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) |
46 |
39 45
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) |
47 |
39 31
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ ) |
48 |
1 2 3 4 5
|
abelthlem2 |
⊢ ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) ) |
49 |
48
|
simprd |
⊢ ( 𝜑 → ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) |
50 |
49 8
|
sseldd |
⊢ ( 𝜑 → 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) |
51 |
1 2 3 4 5 6 7
|
abelthlem5 |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ) |
52 |
50 51
|
mpdan |
⊢ ( 𝜑 → seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ) |
53 |
45
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) |
54 |
53 31
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ ) |
55 |
24 10 54
|
iserex |
⊢ ( 𝜑 → ( seq 0 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ↔ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ) ) |
56 |
52 55
|
mpbid |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ) |
57 |
36 37 46 47 56
|
isumcl |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ ) |
58 |
21 57
|
mulcld |
⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℂ ) |
59 |
58
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ∈ ℝ ) |
60 |
35 59
|
readdcld |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) ∈ ℝ ) |
61 |
|
peano2re |
⊢ ( 𝑀 ∈ ℝ → ( 𝑀 + 1 ) ∈ ℝ ) |
62 |
3 61
|
syl |
⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℝ ) |
63 |
9
|
rpred |
⊢ ( 𝜑 → 𝑅 ∈ ℝ ) |
64 |
62 63
|
remulcld |
⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑅 ) ∈ ℝ ) |
65 |
1 2 3 4 5 6 7 8
|
abelthlem6 |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
66 |
24 36 10 53 31 52
|
isumsplit |
⊢ ( 𝜑 → Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
67 |
66
|
oveq2d |
⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ℕ0 ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = ( ( 1 − 𝑋 ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) |
68 |
21 33 57
|
adddid |
⊢ ( 𝜑 → ( ( 1 − 𝑋 ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) + Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) = ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) |
69 |
65 67 68
|
3eqtrd |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) |
70 |
69
|
fveq2d |
⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) = ( abs ‘ ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) ) |
71 |
34 58
|
abstrid |
⊢ ( 𝜑 → ( abs ‘ ( ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) + ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) ≤ ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) ) |
72 |
70 71
|
eqbrtrd |
⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) ) |
73 |
3 63
|
remulcld |
⊢ ( 𝜑 → ( 𝑀 · 𝑅 ) ∈ ℝ ) |
74 |
21
|
abscld |
⊢ ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℝ ) |
75 |
28
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ ) |
76 |
23 75
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ ) |
77 |
22 76
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ ) |
78 |
|
peano2re |
⊢ ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ → ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ∈ ℝ ) |
79 |
77 78
|
syl |
⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ∈ ℝ ) |
80 |
74 79
|
remulcld |
⊢ ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ∈ ℝ ) |
81 |
21 33
|
absmuld |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) = ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) |
82 |
33
|
abscld |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
83 |
21
|
absge0d |
⊢ ( 𝜑 → 0 ≤ ( abs ‘ ( 1 − 𝑋 ) ) ) |
84 |
31
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
85 |
23 84
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
86 |
22 85
|
fsumrecl |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
87 |
22 32
|
fsumabs |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
88 |
19
|
abscld |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℝ ) |
89 |
|
reexpcl |
⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ ℝ ) |
90 |
88 89
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ ℝ ) |
91 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 1 ∈ ℝ ) |
92 |
28
|
absge0d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
93 |
88
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ 𝑋 ) ∈ ℝ ) |
94 |
19
|
absge0d |
⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝑋 ) ) |
95 |
94
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 0 ≤ ( abs ‘ 𝑋 ) ) |
96 |
|
0cn |
⊢ 0 ∈ ℂ |
97 |
|
eqid |
⊢ ( abs ∘ − ) = ( abs ∘ − ) |
98 |
97
|
cnmetdval |
⊢ ( ( 𝑋 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑋 − 0 ) ) ) |
99 |
19 96 98
|
sylancl |
⊢ ( 𝜑 → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑋 − 0 ) ) ) |
100 |
19
|
subid1d |
⊢ ( 𝜑 → ( 𝑋 − 0 ) = 𝑋 ) |
101 |
100
|
fveq2d |
⊢ ( 𝜑 → ( abs ‘ ( 𝑋 − 0 ) ) = ( abs ‘ 𝑋 ) ) |
102 |
99 101
|
eqtrd |
⊢ ( 𝜑 → ( 𝑋 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑋 ) ) |
103 |
|
cnxmet |
⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) |
104 |
|
1xr |
⊢ 1 ∈ ℝ* |
105 |
|
elbl3 |
⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ ℝ* ) ∧ ( 0 ∈ ℂ ∧ 𝑋 ∈ ℂ ) ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) ) |
106 |
103 104 105
|
mpanl12 |
⊢ ( ( 0 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) ) |
107 |
96 19 106
|
sylancr |
⊢ ( 𝜑 → ( 𝑋 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) ) |
108 |
50 107
|
mpbid |
⊢ ( 𝜑 → ( 𝑋 ( abs ∘ − ) 0 ) < 1 ) |
109 |
102 108
|
eqbrtrrd |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) < 1 ) |
110 |
|
1re |
⊢ 1 ∈ ℝ |
111 |
|
ltle |
⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 1 → ( abs ‘ 𝑋 ) ≤ 1 ) ) |
112 |
88 110 111
|
sylancl |
⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) < 1 → ( abs ‘ 𝑋 ) ≤ 1 ) ) |
113 |
109 112
|
mpd |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ≤ 1 ) |
114 |
113
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ 𝑋 ) ≤ 1 ) |
115 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 ) |
116 |
|
exple1 |
⊢ ( ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑋 ) ∧ ( abs ‘ 𝑋 ) ≤ 1 ) ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ≤ 1 ) |
117 |
93 95 114 115 116
|
syl31anc |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ≤ 1 ) |
118 |
90 91 75 92 117
|
lemul2ad |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ≤ ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · 1 ) ) |
119 |
28 30
|
absmuld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( abs ‘ ( 𝑋 ↑ 𝑛 ) ) ) ) |
120 |
|
absexp |
⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( 𝑋 ↑ 𝑛 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) |
121 |
19 120
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( 𝑋 ↑ 𝑛 ) ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) |
122 |
121
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( abs ‘ ( 𝑋 ↑ 𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
123 |
119 122
|
eqtr2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
124 |
75
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℂ ) |
125 |
124
|
mulid1d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · 1 ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
126 |
118 123 125
|
3brtr3d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
127 |
23 126
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
128 |
22 85 76 127
|
fsumle |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
129 |
82 86 77 87 128
|
letrd |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
130 |
77
|
ltp1d |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) |
131 |
82 77 79 129 130
|
lelttrd |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) |
132 |
82 79 131
|
ltled |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) |
133 |
82 79 74 83 132
|
lemul2ad |
⊢ ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ≤ ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) |
134 |
81 133
|
eqbrtrd |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ≤ ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) |
135 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
136 |
23 92
|
sylan2 |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 0 ≤ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
137 |
22 76 136
|
fsumge0 |
⊢ ( 𝜑 → 0 ≤ Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
138 |
135 77 79 137 130
|
lelttrd |
⊢ ( 𝜑 → 0 < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) |
139 |
|
ltmuldiv |
⊢ ( ( ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ( ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ∈ ℝ ∧ 0 < ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) → ( ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) < 𝑅 ↔ ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) ) |
140 |
74 63 79 138 139
|
syl112anc |
⊢ ( 𝜑 → ( ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) < 𝑅 ↔ ( abs ‘ ( 1 − 𝑋 ) ) < ( 𝑅 / ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) ) ) |
141 |
12 140
|
mpbird |
⊢ ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) + 1 ) ) < 𝑅 ) |
142 |
35 80 63 134 141
|
lelttrd |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) < 𝑅 ) |
143 |
21 57
|
absmuld |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) = ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) |
144 |
57
|
abscld |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
145 |
42
|
fveq2d |
⊢ ( 𝑘 = 𝑛 → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
146 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) |
147 |
|
fvex |
⊢ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ V |
148 |
145 146 147
|
fvmpt |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
149 |
39 148
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
150 |
47
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
151 |
|
uzid |
⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) ) |
152 |
37 151
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) ) |
153 |
|
oveq2 |
⊢ ( 𝑘 = 𝑛 → ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) |
154 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) |
155 |
|
ovex |
⊢ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ V |
156 |
153 154 155
|
fvmpt |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) |
157 |
39 156
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) = ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) |
158 |
39 90
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ∈ ℝ ) |
159 |
157 158
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ∈ ℝ ) |
160 |
150
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℂ ) |
161 |
149 160
|
eqeltrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) ∈ ℂ ) |
162 |
88
|
recnd |
⊢ ( 𝜑 → ( abs ‘ 𝑋 ) ∈ ℂ ) |
163 |
|
absidm |
⊢ ( 𝑋 ∈ ℂ → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) ) |
164 |
19 163
|
syl |
⊢ ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) = ( abs ‘ 𝑋 ) ) |
165 |
164 109
|
eqbrtrd |
⊢ ( 𝜑 → ( abs ‘ ( abs ‘ 𝑋 ) ) < 1 ) |
166 |
162 165 10 157
|
geolim2 |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ⇝ ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
167 |
|
seqex |
⊢ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ∈ V |
168 |
|
ovex |
⊢ ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ V |
169 |
167 168
|
breldm |
⊢ ( seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ⇝ ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ ) |
170 |
166 169
|
syl |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ∈ dom ⇝ ) |
171 |
119 122
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
172 |
39 171
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) = ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
173 |
39 75
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ∈ ℝ ) |
174 |
63
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑅 ∈ ℝ ) |
175 |
88
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ 𝑋 ) ∈ ℝ ) |
176 |
94
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ ( abs ‘ 𝑋 ) ) |
177 |
175 39 176
|
expge0d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 0 ≤ ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) |
178 |
40
|
fveq2d |
⊢ ( 𝑘 = 𝑛 → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) = ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ) |
179 |
178
|
breq1d |
⊢ ( 𝑘 = 𝑛 → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅 ↔ ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < 𝑅 ) ) |
180 |
179
|
rspccva |
⊢ ( ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) ) < 𝑅 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < 𝑅 ) |
181 |
11 180
|
sylan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) < 𝑅 ) |
182 |
173 174 181
|
ltled |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) ≤ 𝑅 ) |
183 |
173 174 158 177 182
|
lemul1ad |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( abs ‘ ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) ) · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ≤ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
184 |
172 183
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
185 |
149
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) |
186 |
|
absidm |
⊢ ( ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ∈ ℂ → ( abs ‘ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
187 |
47 186
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
188 |
185 187
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
189 |
157
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
190 |
184 188 189
|
3brtr4d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) ) ≤ ( 𝑅 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) ) |
191 |
36 152 159 161 170 63 190
|
cvgcmpce |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ) ∈ dom ⇝ ) |
192 |
36 37 149 150 191
|
isumrecl |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ∈ ℝ ) |
193 |
|
eldifsni |
⊢ ( 𝑋 ∈ ( 𝑆 ∖ { 1 } ) → 𝑋 ≠ 1 ) |
194 |
8 193
|
syl |
⊢ ( 𝜑 → 𝑋 ≠ 1 ) |
195 |
194
|
necomd |
⊢ ( 𝜑 → 1 ≠ 𝑋 ) |
196 |
|
subeq0 |
⊢ ( ( 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 1 − 𝑋 ) = 0 ↔ 1 = 𝑋 ) ) |
197 |
196
|
necon3bid |
⊢ ( ( 1 ∈ ℂ ∧ 𝑋 ∈ ℂ ) → ( ( 1 − 𝑋 ) ≠ 0 ↔ 1 ≠ 𝑋 ) ) |
198 |
17 19 197
|
sylancr |
⊢ ( 𝜑 → ( ( 1 − 𝑋 ) ≠ 0 ↔ 1 ≠ 𝑋 ) ) |
199 |
195 198
|
mpbird |
⊢ ( 𝜑 → ( 1 − 𝑋 ) ≠ 0 ) |
200 |
21 199
|
absrpcld |
⊢ ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℝ+ ) |
201 |
73 200
|
rerpdivcld |
⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ∈ ℝ ) |
202 |
36 37 46 47 56
|
isumclim2 |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ⇝ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) |
203 |
36 37 149 160 191
|
isumclim2 |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ) ⇝ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
204 |
39 54
|
syldan |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ∈ ℂ ) |
205 |
46
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ) = ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
206 |
149 205
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ) ‘ 𝑛 ) = ( abs ‘ ( ( 𝑘 ∈ ℕ0 ↦ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑘 ) · ( 𝑋 ↑ 𝑘 ) ) ) ‘ 𝑛 ) ) ) |
207 |
36 202 203 37 204 206
|
iserabs |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) |
208 |
88 10
|
reexpcld |
⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ∈ ℝ ) |
209 |
|
difrp |
⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 1 ↔ ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ+ ) ) |
210 |
88 110 209
|
sylancl |
⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) < 1 ↔ ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ+ ) ) |
211 |
109 210
|
mpbid |
⊢ ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ+ ) |
212 |
208 211
|
rerpdivcld |
⊢ ( 𝜑 → ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ ) |
213 |
63 212
|
remulcld |
⊢ ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ∈ ℝ ) |
214 |
153
|
oveq2d |
⊢ ( 𝑘 = 𝑛 → ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
215 |
|
eqid |
⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) |
216 |
|
ovex |
⊢ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ∈ V |
217 |
214 215 216
|
fvmpt |
⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
218 |
39 217
|
syl |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
219 |
174 158
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ∈ ℝ ) |
220 |
9
|
rpcnd |
⊢ ( 𝜑 → 𝑅 ∈ ℂ ) |
221 |
159
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ∈ ℂ ) |
222 |
218 189
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( 𝑘 ∈ ℕ0 ↦ ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ‘ 𝑛 ) ) ) |
223 |
36 37 220 166 221 222
|
isermulc2 |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ⇝ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
224 |
|
seqex |
⊢ seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ V |
225 |
|
ovex |
⊢ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ∈ V |
226 |
224 225
|
breldm |
⊢ ( seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ⇝ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ) |
227 |
223 226
|
syl |
⊢ ( 𝜑 → seq 𝑁 ( + , ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑘 ) ) ) ) ∈ dom ⇝ ) |
228 |
36 37 149 150 218 219 184 191 227
|
isumle |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ) |
229 |
219
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) ∈ ℂ ) |
230 |
36 37 218 229 223
|
isumclim |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝑅 · ( ( abs ‘ 𝑋 ) ↑ 𝑛 ) ) = ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
231 |
228 230
|
breqtrd |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
232 |
9 211
|
rpdivcld |
⊢ ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ+ ) |
233 |
232
|
rpred |
⊢ ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ ) |
234 |
208
|
recnd |
⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ∈ ℂ ) |
235 |
211
|
rpcnd |
⊢ ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℂ ) |
236 |
211
|
rpne0d |
⊢ ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ≠ 0 ) |
237 |
220 234 235 236
|
div12d |
⊢ ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
238 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
239 |
232
|
rpge0d |
⊢ ( 𝜑 → 0 ≤ ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
240 |
|
exple1 |
⊢ ( ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑋 ) ∧ ( abs ‘ 𝑋 ) ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ≤ 1 ) |
241 |
88 94 113 10 240
|
syl31anc |
⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) ≤ 1 ) |
242 |
208 238 233 239 241
|
lemul1ad |
⊢ ( 𝜑 → ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( 1 · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
243 |
232
|
rpcnd |
⊢ ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℂ ) |
244 |
243
|
mulid2d |
⊢ ( 𝜑 → ( 1 · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
245 |
242 244
|
breqtrd |
⊢ ( 𝜑 → ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) · ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
246 |
237 245
|
eqbrtrd |
⊢ ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
247 |
18
|
simprd |
⊢ ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
248 |
|
resubcl |
⊢ ( ( 1 ∈ ℝ ∧ ( abs ‘ 𝑋 ) ∈ ℝ ) → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ ) |
249 |
110 88 248
|
sylancr |
⊢ ( 𝜑 → ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ ) |
250 |
3 249
|
remulcld |
⊢ ( 𝜑 → ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ∈ ℝ ) |
251 |
74 250 9
|
lemul2d |
⊢ ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ↔ ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) ) |
252 |
247 251
|
mpbid |
⊢ ( 𝜑 → ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
253 |
3
|
recnd |
⊢ ( 𝜑 → 𝑀 ∈ ℂ ) |
254 |
220 253 235
|
mul12d |
⊢ ( 𝜑 → ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( 𝑀 · ( 𝑅 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) ) |
255 |
220 235
|
mulcomd |
⊢ ( 𝜑 → ( 𝑅 · ( 1 − ( abs ‘ 𝑋 ) ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · 𝑅 ) ) |
256 |
255
|
oveq2d |
⊢ ( 𝜑 → ( 𝑀 · ( 𝑅 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( 𝑀 · ( ( 1 − ( abs ‘ 𝑋 ) ) · 𝑅 ) ) ) |
257 |
253 235 220
|
mul12d |
⊢ ( 𝜑 → ( 𝑀 · ( ( 1 − ( abs ‘ 𝑋 ) ) · 𝑅 ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ) |
258 |
254 256 257
|
3eqtrd |
⊢ ( 𝜑 → ( 𝑅 · ( 𝑀 · ( 1 − ( abs ‘ 𝑋 ) ) ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ) |
259 |
252 258
|
breqtrd |
⊢ ( 𝜑 → ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ) |
260 |
249 73
|
remulcld |
⊢ ( 𝜑 → ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ∈ ℝ ) |
261 |
63 260 200
|
lemuldivd |
⊢ ( 𝜑 → ( ( 𝑅 · ( abs ‘ ( 1 − 𝑋 ) ) ) ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) ↔ 𝑅 ≤ ( ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) |
262 |
259 261
|
mpbid |
⊢ ( 𝜑 → 𝑅 ≤ ( ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) |
263 |
73
|
recnd |
⊢ ( 𝜑 → ( 𝑀 · 𝑅 ) ∈ ℂ ) |
264 |
74
|
recnd |
⊢ ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ∈ ℂ ) |
265 |
200
|
rpne0d |
⊢ ( 𝜑 → ( abs ‘ ( 1 − 𝑋 ) ) ≠ 0 ) |
266 |
235 263 264 265
|
divassd |
⊢ ( 𝜑 → ( ( ( 1 − ( abs ‘ 𝑋 ) ) · ( 𝑀 · 𝑅 ) ) / ( abs ‘ ( 1 − 𝑋 ) ) ) = ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) |
267 |
262 266
|
breqtrd |
⊢ ( 𝜑 → 𝑅 ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) |
268 |
|
posdif |
⊢ ( ( ( abs ‘ 𝑋 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( abs ‘ 𝑋 ) < 1 ↔ 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
269 |
88 110 268
|
sylancl |
⊢ ( 𝜑 → ( ( abs ‘ 𝑋 ) < 1 ↔ 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) ) |
270 |
109 269
|
mpbid |
⊢ ( 𝜑 → 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) |
271 |
|
ledivmul |
⊢ ( ( 𝑅 ∈ ℝ ∧ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ∈ ℝ ∧ ( ( 1 − ( abs ‘ 𝑋 ) ) ∈ ℝ ∧ 0 < ( 1 − ( abs ‘ 𝑋 ) ) ) ) → ( ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ↔ 𝑅 ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) ) |
272 |
63 201 249 270 271
|
syl112anc |
⊢ ( 𝜑 → ( ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ↔ 𝑅 ≤ ( ( 1 − ( abs ‘ 𝑋 ) ) · ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) ) |
273 |
267 272
|
mpbird |
⊢ ( 𝜑 → ( 𝑅 / ( 1 − ( abs ‘ 𝑋 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) |
274 |
213 233 201 246 273
|
letrd |
⊢ ( 𝜑 → ( 𝑅 · ( ( ( abs ‘ 𝑋 ) ↑ 𝑁 ) / ( 1 − ( abs ‘ 𝑋 ) ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) |
275 |
192 213 201 231 274
|
letrd |
⊢ ( 𝜑 → Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( abs ‘ ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) |
276 |
144 192 201 207 275
|
letrd |
⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) |
277 |
144 73 200
|
lemuldiv2d |
⊢ ( 𝜑 → ( ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ≤ ( 𝑀 · 𝑅 ) ↔ ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ≤ ( ( 𝑀 · 𝑅 ) / ( abs ‘ ( 1 − 𝑋 ) ) ) ) ) |
278 |
276 277
|
mpbird |
⊢ ( 𝜑 → ( ( abs ‘ ( 1 − 𝑋 ) ) · ( abs ‘ Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ≤ ( 𝑀 · 𝑅 ) ) |
279 |
143 278
|
eqbrtrd |
⊢ ( 𝜑 → ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ≤ ( 𝑀 · 𝑅 ) ) |
280 |
35 59 63 73 142 279
|
ltleaddd |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) < ( 𝑅 + ( 𝑀 · 𝑅 ) ) ) |
281 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
282 |
253 281 220
|
adddird |
⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑅 ) = ( ( 𝑀 · 𝑅 ) + ( 1 · 𝑅 ) ) ) |
283 |
220
|
mulid2d |
⊢ ( 𝜑 → ( 1 · 𝑅 ) = 𝑅 ) |
284 |
283
|
oveq2d |
⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) + ( 1 · 𝑅 ) ) = ( ( 𝑀 · 𝑅 ) + 𝑅 ) ) |
285 |
263 220
|
addcomd |
⊢ ( 𝜑 → ( ( 𝑀 · 𝑅 ) + 𝑅 ) = ( 𝑅 + ( 𝑀 · 𝑅 ) ) ) |
286 |
282 284 285
|
3eqtrd |
⊢ ( 𝜑 → ( ( 𝑀 + 1 ) · 𝑅 ) = ( 𝑅 + ( 𝑀 · 𝑅 ) ) ) |
287 |
280 286
|
breqtrrd |
⊢ ( 𝜑 → ( ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) + ( abs ‘ ( ( 1 − 𝑋 ) · Σ 𝑛 ∈ ( ℤ≥ ‘ 𝑁 ) ( ( seq 0 ( + , 𝐴 ) ‘ 𝑛 ) · ( 𝑋 ↑ 𝑛 ) ) ) ) ) < ( ( 𝑀 + 1 ) · 𝑅 ) ) |
288 |
16 60 64 72 287
|
lelttrd |
⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ 𝑋 ) ) < ( ( 𝑀 + 1 ) · 𝑅 ) ) |