Step | Hyp | Ref
| Expression |
1 | | abelthlem6.1 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝑆 ∖ {1})) |
2 | 1 | eldifad 3552 |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝑆) |
3 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥↑𝑛) = (𝑋↑𝑛)) |
4 | 3 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑛) · (𝑋↑𝑛))) |
5 | 4 | sumeq2sdv 14282 |
. . . 4
⊢ (𝑥 = 𝑋 → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛))) |
6 | | abelth.6 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) |
7 | | sumex 14266 |
. . . 4
⊢
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛)) ∈ V |
8 | 5, 6, 7 | fvmpt 6191 |
. . 3
⊢ (𝑋 ∈ 𝑆 → (𝐹‘𝑋) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛))) |
9 | 2, 8 | syl 17 |
. 2
⊢ (𝜑 → (𝐹‘𝑋) = Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛))) |
10 | | nn0uz 11598 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
11 | | 0zd 11266 |
. . 3
⊢ (𝜑 → 0 ∈
ℤ) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝐴‘𝑘) = (𝐴‘𝑛)) |
13 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = 𝑛 → (𝑋↑𝑘) = (𝑋↑𝑛)) |
14 | 12, 13 | oveq12d 6567 |
. . . . 5
⊢ (𝑘 = 𝑛 → ((𝐴‘𝑘) · (𝑋↑𝑘)) = ((𝐴‘𝑛) · (𝑋↑𝑛))) |
15 | | eqid 2610 |
. . . . 5
⊢ (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘))) |
16 | | ovex 6577 |
. . . . 5
⊢ ((𝐴‘𝑛) · (𝑋↑𝑛)) ∈ V |
17 | 14, 15, 16 | fvmpt 6191 |
. . . 4
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((𝐴‘𝑛) · (𝑋↑𝑛))) |
18 | 17 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((𝐴‘𝑛) · (𝑋↑𝑛))) |
19 | | abelth.1 |
. . . . 5
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
20 | 19 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) ∈ ℂ) |
21 | | abelth.5 |
. . . . . . 7
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} |
22 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑧 ∈ ℂ ∣
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))} ⊆
ℂ |
23 | 21, 22 | eqsstri 3598 |
. . . . . 6
⊢ 𝑆 ⊆
ℂ |
24 | 23, 2 | sseldi 3566 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
25 | | expcl 12740 |
. . . . 5
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑋↑𝑛) ∈
ℂ) |
26 | 24, 25 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑋↑𝑛) ∈ ℂ) |
27 | 20, 26 | mulcld 9939 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
28 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛)) |
29 | 28, 13 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
30 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))) |
31 | | ovex 6577 |
. . . . . . . 8
⊢ ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ V |
32 | 29, 30, 31 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
33 | 32 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
34 | 10, 11, 20 | serf 12691 |
. . . . . . . 8
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) |
35 | 34 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑛) ∈
ℂ) |
36 | 35, 26 | mulcld 9939 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
37 | | abelth.2 |
. . . . . . . . . 10
⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝
) |
38 | | abelth.3 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℝ) |
39 | | abelth.4 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝑀) |
40 | 19, 37, 38, 39, 21 | abelthlem2 23990 |
. . . . . . . . 9
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
41 | 40 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) |
42 | 41, 1 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) |
43 | | abelth.7 |
. . . . . . . 8
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) |
44 | 19, 37, 38, 39, 21, 6, 43 | abelthlem5 23993 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , (𝑘
∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
45 | 42, 44 | mpdan 699 |
. . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
46 | 10, 11, 33, 36, 45 | isumclim2 14331 |
. . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ⇝ Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
47 | | seqex 12665 |
. . . . . 6
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ∈ V |
48 | 47 | a1i 11 |
. . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ∈ V) |
49 | | 0nn0 11184 |
. . . . . . . 8
⊢ 0 ∈
ℕ0 |
50 | 49 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℕ0) |
51 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (𝑘 − 1) = (𝑖 − 1)) |
52 | 51 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑖 → (0...(𝑘 − 1)) = (0...(𝑖 − 1))) |
53 | 52 | sumeq1d 14279 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚)) |
54 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑖 → (𝑋↑𝑘) = (𝑋↑𝑖)) |
55 | 53, 54 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑖 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖))) |
56 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))) |
57 | | ovex 6577 |
. . . . . . . . . 10
⊢
(Σ𝑚 ∈
(0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖)) ∈ V |
58 | 55, 56, 57 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑖) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖))) |
59 | 58 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑖) = (Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖))) |
60 | | fzfid 12634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(0...(𝑖 − 1)) ∈
Fin) |
61 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) |
62 | | elfznn0 12302 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...(𝑖 − 1)) → 𝑚 ∈ ℕ0) |
63 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑚 ∈
ℕ0) → (𝐴‘𝑚) ∈ ℂ) |
64 | 61, 62, 63 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑚 ∈ (0...(𝑖 − 1))) → (𝐴‘𝑚) ∈ ℂ) |
65 | 60, 64 | fsumcl 14311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
Σ𝑚 ∈ (0...(𝑖 − 1))(𝐴‘𝑚) ∈ ℂ) |
66 | | expcl 12740 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑋↑𝑖) ∈
ℂ) |
67 | 24, 66 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑋↑𝑖) ∈ ℂ) |
68 | 65, 67 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) →
(Σ𝑚 ∈
(0...(𝑖 − 1))(𝐴‘𝑚) · (𝑋↑𝑖)) ∈ ℂ) |
69 | 59, 68 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ) |
70 | 11 | peano2zd 11361 |
. . . . . . . . 9
⊢ (𝜑 → (0 + 1) ∈
ℤ) |
71 | | nnuz 11599 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
72 | | 1e0p1 11428 |
. . . . . . . . . . . . 13
⊢ 1 = (0 +
1) |
73 | 72 | fveq2i 6106 |
. . . . . . . . . . . 12
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
74 | 71, 73 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘(0 + 1)) |
75 | 74 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘(0 + 1))) |
76 | | nnm1nn0 11211 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
77 | 76 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈
ℕ0) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 − 1) → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘(𝑛 − 1))) |
79 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑛 − 1) → (𝑋↑𝑘) = (𝑋↑(𝑛 − 1))) |
80 | 78, 79 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 − 1) → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) |
81 | 80 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 − 1) → (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) |
82 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) |
83 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) ∈ V |
84 | 81, 82, 83 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ ((𝑛 − 1) ∈
ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1)) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) |
85 | 77, 84 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1)) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) |
86 | | ax-1cn 9873 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
87 | | nncn 10905 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℂ) |
88 | 87 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
89 | | nn0ex 11175 |
. . . . . . . . . . . . . 14
⊢
ℕ0 ∈ V |
90 | 89 | mptex 6390 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ V |
91 | 90 | shftval 13662 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℂ ∧ 𝑛
∈ ℂ) → (((𝑘
∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1))) |
92 | 86, 88, 91 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘(𝑛 − 1))) |
93 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴‘𝑚) = (𝐴‘𝑚)) |
94 | 77, 10 | syl6eleq 2698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈
(ℤ≥‘0)) |
95 | 19 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝐴:ℕ0⟶ℂ) |
96 | | elfznn0 12302 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...(𝑛 − 1)) → 𝑚 ∈ ℕ0) |
97 | 95, 96, 63 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴‘𝑚) ∈ ℂ) |
98 | 93, 94, 97 | fsumser 14308 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) = (seq0( + , 𝐴)‘(𝑛 − 1))) |
99 | | expm1t 12750 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ) → (𝑋↑𝑛) = ((𝑋↑(𝑛 − 1)) · 𝑋)) |
100 | 24, 99 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋↑𝑛) = ((𝑋↑(𝑛 − 1)) · 𝑋)) |
101 | 24 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑋 ∈ ℂ) |
102 | | expcl 12740 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℂ ∧ (𝑛 − 1) ∈
ℕ0) → (𝑋↑(𝑛 − 1)) ∈ ℂ) |
103 | 24, 76, 102 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋↑(𝑛 − 1)) ∈ ℂ) |
104 | 101, 103 | mulcomd 9940 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋 · (𝑋↑(𝑛 − 1))) = ((𝑋↑(𝑛 − 1)) · 𝑋)) |
105 | 100, 104 | eqtr4d 2647 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋↑𝑛) = (𝑋 · (𝑋↑(𝑛 − 1)))) |
106 | 98, 105 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋 · (𝑋↑(𝑛 − 1))))) |
107 | | nnnn0 11176 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0) |
109 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑛 → (𝑘 − 1) = (𝑛 − 1)) |
110 | 109 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑛 → (0...(𝑘 − 1)) = (0...(𝑛 − 1))) |
111 | 110 | sumeq1d 14279 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) |
112 | 111, 13 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑛 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) |
113 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
(Σ𝑚 ∈
(0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)) ∈ V |
114 | 112, 56, 113 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) |
115 | 108, 114 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) |
116 | | ffvelrn 6265 |
. . . . . . . . . . . . . 14
⊢ ((seq0( +
, 𝐴):ℕ0⟶ℂ ∧
(𝑛 − 1) ∈
ℕ0) → (seq0( + , 𝐴)‘(𝑛 − 1)) ∈ ℂ) |
117 | 34, 76, 116 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (seq0( + , 𝐴)‘(𝑛 − 1)) ∈ ℂ) |
118 | 101, 117,
103 | mul12d 10124 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1)))) = ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋 · (𝑋↑(𝑛 − 1))))) |
119 | 106, 115,
118 | 3eqtr4d 2654 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (𝑋 · ((seq0( + , 𝐴)‘(𝑛 − 1)) · (𝑋↑(𝑛 − 1))))) |
120 | 85, 92, 119 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛)) |
121 | 75, 120 | sylan2br 492 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(0 +
1))) → (((𝑘 ∈
ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)‘𝑛) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛)) |
122 | 70, 121 | seqfeq 12688 |
. . . . . . . 8
⊢ (𝜑 → seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) = seq(0 + 1)( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))) |
123 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑖 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑖)) |
124 | 123, 54 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
125 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ ((seq0( +
, 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ V |
126 | 124, 30, 125 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
127 | 126 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
128 | 34 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑖) ∈
ℂ) |
129 | 128, 67 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ ℂ) |
130 | 127, 129 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ) |
131 | 124 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑖 → (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) |
132 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) ∈ V |
133 | 131, 82, 132 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) |
134 | 133 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) |
135 | 127 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (𝑋 · ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) = (𝑋 · ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) |
136 | 134, 135 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) = (𝑋 · ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖))) |
137 | 10, 11, 24, 46, 130, 136 | isermulc2 14236 |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
138 | | 0z 11265 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
139 | | 1z 11284 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
140 | 90 | isershft 14242 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (seq0( + , (𝑘 ∈ ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ↔ seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
141 | 138, 139,
140 | mp2an 704 |
. . . . . . . . 9
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (𝑋 · ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ↔ seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
142 | 137, 141 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → seq(0 + 1)( + , ((𝑘 ∈ ℕ0
↦ (𝑋 · ((seq0(
+ , 𝐴)‘𝑘) · (𝑋↑𝑘)))) shift 1)) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
143 | 122, 142 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (𝜑 → seq(0 + 1)( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
144 | 10, 50, 69, 143 | clim2ser2 14234 |
. . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))) ⇝ ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0))) |
145 | | seq1 12676 |
. . . . . . . . . . 11
⊢ (0 ∈
ℤ → (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0)) |
146 | 138, 145 | ax-mp 5 |
. . . . . . . . . 10
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0) |
147 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) |
148 | 147 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 0 → (0...(𝑘 − 1)) = (0...(0 −
1))) |
149 | | 0re 9919 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
150 | | ltm1 10742 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℝ → (0 − 1) < 0) |
151 | 149, 150 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ (0
− 1) < 0 |
152 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
ℤ → (0 − 1) ∈ ℤ) |
153 | 138, 152 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (0
− 1) ∈ ℤ |
154 | | fzn 12228 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℤ ∧ (0 − 1) ∈ ℤ) → ((0 − 1) < 0
↔ (0...(0 − 1)) = ∅)) |
155 | 138, 153,
154 | mp2an 704 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
− 1) < 0 ↔ (0...(0 − 1)) = ∅) |
156 | 151, 155 | mpbi 219 |
. . . . . . . . . . . . . . . 16
⊢ (0...(0
− 1)) = ∅ |
157 | 148, 156 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 0 → (0...(𝑘 − 1)) =
∅) |
158 | 157 | sumeq1d 14279 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 0 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = Σ𝑚 ∈ ∅ (𝐴‘𝑚)) |
159 | | sum0 14299 |
. . . . . . . . . . . . . 14
⊢
Σ𝑚 ∈
∅ (𝐴‘𝑚) = 0 |
160 | 158, 159 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) = 0) |
161 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 0 → (𝑋↑𝑘) = (𝑋↑0)) |
162 | 160, 161 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)) = (0 · (𝑋↑0))) |
163 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (0
· (𝑋↑0)) ∈
V |
164 | 162, 56, 163 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0) = (0 · (𝑋↑0))) |
165 | 49, 164 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘0) = (0 · (𝑋↑0)) |
166 | 146, 165 | eqtri 2632 |
. . . . . . . . 9
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = (0 · (𝑋↑0)) |
167 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧ 0 ∈
ℕ0) → (𝑋↑0) ∈ ℂ) |
168 | 24, 49, 167 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋↑0) ∈ ℂ) |
169 | 168 | mul02d 10113 |
. . . . . . . . 9
⊢ (𝜑 → (0 · (𝑋↑0)) = 0) |
170 | 166, 169 | syl5eq 2656 |
. . . . . . . 8
⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0) = 0) |
171 | 170 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0)) = ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + 0)) |
172 | 10, 11, 33, 36, 45 | isumcl 14334 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) ∈ ℂ) |
173 | 24, 172 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) ∈ ℂ) |
174 | 173 | addid1d 10115 |
. . . . . . 7
⊢ (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + 0) = (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
175 | 171, 174 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → ((𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) + (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘0)) = (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
176 | 144, 175 | breqtrd 4609 |
. . . . 5
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))) ⇝ (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
177 | 10, 11, 130 | serf 12691 |
. . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))):ℕ0⟶ℂ) |
178 | 177 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) ∈ ℂ) |
179 | 10, 11, 69 | serf 12691 |
. . . . . 6
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))):ℕ0⟶ℂ) |
180 | 179 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝑘 ∈
ℕ0 ↦ (Σ𝑚 ∈ (0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘𝑖) ∈ ℂ) |
181 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℕ0) |
182 | 181, 10 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
(ℤ≥‘0)) |
183 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → 𝜑) |
184 | | elfznn0 12302 |
. . . . . . 7
⊢ (𝑛 ∈ (0...𝑖) → 𝑛 ∈ ℕ0) |
185 | 33, 36 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
186 | 183, 184,
185 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
187 | 114 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛))) |
188 | | fzfid 12634 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(0...(𝑛 − 1)) ∈
Fin) |
189 | 19 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) |
190 | 189, 96, 63 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...(𝑛 − 1))) → (𝐴‘𝑚) ∈ ℂ) |
191 | 188, 190 | fsumcl 14311 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) ∈ ℂ) |
192 | 191, 26 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
(Σ𝑚 ∈
(0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)) ∈ ℂ) |
193 | 187, 192 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
194 | 183, 184,
193 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛) ∈ ℂ) |
195 | | eqidd 2611 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...𝑛)) → (𝐴‘𝑚) = (𝐴‘𝑚)) |
196 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
ℕ0) |
197 | 196, 10 | syl6eleq 2698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈
(ℤ≥‘0)) |
198 | | elfznn0 12302 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ (0...𝑛) → 𝑚 ∈ ℕ0) |
199 | 189, 198,
63 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ 𝑚 ∈ (0...𝑛)) → (𝐴‘𝑚) ∈ ℂ) |
200 | 195, 197,
199 | fsumser 14308 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
Σ𝑚 ∈ (0...𝑛)(𝐴‘𝑚) = (seq0( + , 𝐴)‘𝑛)) |
201 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → (𝐴‘𝑚) = (𝐴‘𝑛)) |
202 | 197, 199,
201 | fsumm1 14324 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
Σ𝑚 ∈ (0...𝑛)(𝐴‘𝑚) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛))) |
203 | 200, 202 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑛) = (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛))) |
204 | 203 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) = ((Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛)) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚))) |
205 | 191, 20 | pncan2d 10273 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) →
((Σ𝑚 ∈
(0...(𝑛 − 1))(𝐴‘𝑚) + (𝐴‘𝑛)) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) = (𝐴‘𝑛)) |
206 | 204, 205 | eqtr2d 2645 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐴‘𝑛) = ((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚))) |
207 | 206 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑋↑𝑛)) = (((seq0( + , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) · (𝑋↑𝑛))) |
208 | 35, 191, 26 | subdird 10366 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((seq0(
+ , 𝐴)‘𝑛) − Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚)) · (𝑋↑𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)))) |
209 | 207, 208 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐴‘𝑛) · (𝑋↑𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)))) |
210 | 33, 187 | oveq12d 6567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛)) = (((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (Σ𝑚 ∈ (0...(𝑛 − 1))(𝐴‘𝑚) · (𝑋↑𝑛)))) |
211 | 209, 18, 210 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = (((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛))) |
212 | 183, 184,
211 | syl2an 493 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ0) ∧ 𝑛 ∈ (0...𝑖)) → ((𝑘 ∈ ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))‘𝑛) = (((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑛) − ((𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘)))‘𝑛))) |
213 | 182, 186,
194, 212 | sersub 12706 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ0) → (seq0( +
, (𝑘 ∈
ℕ0 ↦ ((𝐴‘𝑘) · (𝑋↑𝑘))))‘𝑖) = ((seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))))‘𝑖) − (seq0( + , (𝑘 ∈ ℕ0 ↦
(Σ𝑚 ∈
(0...(𝑘 − 1))(𝐴‘𝑚) · (𝑋↑𝑘))))‘𝑖))) |
214 | 10, 11, 46, 48, 176, 178, 180, 213 | climsub 14212 |
. . . 4
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ⇝ (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
215 | | 1cnd 9935 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
216 | 215, 24, 172 | subdird 10366 |
. . . . 5
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = ((1 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
217 | 172 | mulid2d 9937 |
. . . . . 6
⊢ (𝜑 → (1 · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) |
218 | 217 | oveq1d 6564 |
. . . . 5
⊢ (𝜑 → ((1 · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) = (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
219 | 216, 218 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0
((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))) = (Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)) − (𝑋 · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛))))) |
220 | 214, 219 | breqtrrd 4611 |
. . 3
⊢ (𝜑 → seq0( + , (𝑘 ∈ ℕ0
↦ ((𝐴‘𝑘) · (𝑋↑𝑘)))) ⇝ ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
221 | 10, 11, 18, 27, 220 | isumclim 14330 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑋↑𝑛)) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |
222 | 9, 221 | eqtrd 2644 |
1
⊢ (𝜑 → (𝐹‘𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋↑𝑛)))) |