Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | cnelprrecn 9908 |
. . 3
⊢ ℂ
∈ {ℝ, ℂ} |
3 | 2 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ℂ ∈ {ℝ,
ℂ}) |
4 | | 0zd 11266 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℤ) |
5 | | fzfid 12634 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (0...𝑘) ∈ Fin) |
6 | | pserf.g |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
7 | | pserf.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
8 | 7 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
9 | | pserdv.b |
. . . . . . . . . . 11
⊢ 𝐵 = (0(ball‘(abs ∘
− ))(((abs‘𝑎) +
𝑀) / 2)) |
10 | | cnxmet 22386 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
12 | | 0cnd 9912 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℂ) |
13 | | pserf.f |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑦 ∈ 𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗)) |
14 | | pserf.r |
. . . . . . . . . . . . . . 15
⊢ 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
15 | | psercn.s |
. . . . . . . . . . . . . . 15
⊢ 𝑆 = (◡abs “ (0[,)𝑅)) |
16 | | psercn.m |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1)) |
17 | 6, 13, 7, 14, 15, 16 | pserdvlem1 23985 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧
(abs‘𝑎) <
(((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅)) |
18 | 17 | simp1d 1066 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ+) |
19 | 18 | rpxrd 11749 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
20 | | blssm 22033 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
21 | 11, 12, 19, 20 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
22 | 9, 21 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ ℂ) |
23 | 22 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆
ℂ) |
24 | 23 | sselda 3568 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
25 | 6, 8, 24 | psergf 23970 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦):ℕ0⟶ℂ) |
26 | | elfznn0 12302 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℕ0) |
27 | | ffvelrn 6265 |
. . . . . . 7
⊢ (((𝐺‘𝑦):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
28 | 25, 26, 27 | syl2an 493 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (0...𝑘)) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
29 | 5, 28 | fsumcl 14311 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
30 | | eqid 2610 |
. . . . 5
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) |
31 | 29, 30 | fmptd 6292 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)):𝐵⟶ℂ) |
32 | | cnex 9896 |
. . . . 5
⊢ ℂ
∈ V |
33 | | ovex 6577 |
. . . . . 6
⊢
(0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ V |
34 | 9, 33 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
35 | 32, 34 | elmap 7772 |
. . . 4
⊢ ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) ∈ (ℂ ↑𝑚
𝐵) ↔ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)):𝐵⟶ℂ) |
36 | 31, 35 | sylibr 223 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) ∈ (ℂ ↑𝑚
𝐵)) |
37 | | eqid 2610 |
. . 3
⊢ (𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))) = (𝑘 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))) |
38 | 36, 37 | fmptd 6292 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑘 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))):ℕ0⟶(ℂ
↑𝑚 𝐵)) |
39 | 6, 13, 7, 14, 15, 16 | psercn 23984 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |
40 | | cncff 22504 |
. . . . 5
⊢ (𝐹 ∈ (𝑆–cn→ℂ) → 𝐹:𝑆⟶ℂ) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
42 | 41 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
43 | 6, 13, 7, 14, 15, 17 | psercnlem2 23982 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs
∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)) |
44 | 43 | simp2d 1067 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2)))) |
45 | 9, 44 | syl5eqss 3612 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2)))) |
46 | 43 | simp3d 1068 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆) |
47 | 45, 46 | sstrd 3578 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ 𝑆) |
48 | 42, 47 | fssresd 5984 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ 𝐵):𝐵⟶ℂ) |
49 | | 0zd 11266 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 0 ∈ ℤ) |
50 | | eqidd 2611 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑧)‘𝑗) = ((𝐺‘𝑧)‘𝑗)) |
51 | 7 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
52 | 22 | sselda 3568 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ℂ) |
53 | 6, 51, 52 | psergf 23970 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧):ℕ0⟶ℂ) |
54 | 53 | ffvelrnda 6267 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑧)‘𝑗) ∈ ℂ) |
55 | 52 | abscld 14023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) ∈ ℝ) |
56 | 55 | rexrd 9968 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) ∈
ℝ*) |
57 | 19 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
58 | | iccssxr 12127 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
59 | 6, 7, 14 | radcnvcl 23975 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
60 | 58, 59 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
61 | 60 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑅 ∈
ℝ*) |
62 | | 0cn 9911 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
63 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
64 | 63 | cnmetdval 22384 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑧(abs
∘ − )0) = (abs‘(𝑧 − 0))) |
65 | 52, 62, 64 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0))) |
66 | 52 | subid1d 10260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧 − 0) = 𝑧) |
67 | 66 | fveq2d 6107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘(𝑧 − 0)) = (abs‘𝑧)) |
68 | 65, 67 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) = (abs‘𝑧)) |
69 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
70 | 69, 9 | syl6eleq 2698 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2))) |
71 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
72 | | 0cnd 9912 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 0 ∈ ℂ) |
73 | | elbl3 22007 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) ∧ (0
∈ ℂ ∧ 𝑧
∈ ℂ)) → (𝑧
∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2))) |
74 | 71, 57, 72, 52, 73 | syl22anc 1319 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2))) |
75 | 70, 74 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2)) |
76 | 68, 75 | eqbrtrrd 4607 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) < (((abs‘𝑎) + 𝑀) / 2)) |
77 | 17 | simp3d 1068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅) |
78 | 77 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅) |
79 | 56, 57, 61, 76, 78 | xrlttrd 11866 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) < 𝑅) |
80 | 6, 51, 14, 52, 79 | radcnvlt2 23977 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ∈ dom ⇝ ) |
81 | 1, 49, 50, 54, 80 | isumclim2 14331 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ⇝ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
82 | 47 | sselda 3568 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑆) |
83 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐺‘𝑦) = (𝐺‘𝑧)) |
84 | 83 | fveq1d 6105 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑗) = ((𝐺‘𝑧)‘𝑗)) |
85 | 84 | sumeq2sdv 14282 |
. . . . . 6
⊢ (𝑦 = 𝑧 → Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
86 | | sumex 14266 |
. . . . . 6
⊢
Σ𝑗 ∈
ℕ0 ((𝐺‘𝑧)‘𝑗) ∈ V |
87 | 85, 13, 86 | fvmpt 6191 |
. . . . 5
⊢ (𝑧 ∈ 𝑆 → (𝐹‘𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
88 | 82, 87 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
89 | 81, 88 | breqtrrd 4611 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ⇝ (𝐹‘𝑧)) |
90 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (0...𝑘) = (0...𝑚)) |
91 | 90 | sumeq1d 14279 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) |
92 | 91 | mpteq2dv 4673 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
93 | 34 | mptex 6390 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) ∈ V |
94 | 92, 37, 93 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
95 | 94 | adantl 481 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
96 | 95 | fveq1d 6105 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧) = ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧)) |
97 | 83 | fveq1d 6105 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑖) = ((𝐺‘𝑧)‘𝑖)) |
98 | 97 | sumeq2sdv 14282 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
99 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) |
100 | | sumex 14266 |
. . . . . . . 8
⊢
Σ𝑖 ∈
(0...𝑚)((𝐺‘𝑧)‘𝑖) ∈ V |
101 | 98, 99, 100 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
102 | 101 | ad2antlr 759 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
103 | | eqidd 2611 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺‘𝑧)‘𝑖) = ((𝐺‘𝑧)‘𝑖)) |
104 | | simpr 476 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
105 | 104, 1 | syl6eleq 2698 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
(ℤ≥‘0)) |
106 | 53 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐺‘𝑧):ℕ0⟶ℂ) |
107 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0) |
108 | | ffvelrn 6265 |
. . . . . . . 8
⊢ (((𝐺‘𝑧):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → ((𝐺‘𝑧)‘𝑖) ∈ ℂ) |
109 | 106, 107,
108 | syl2an 493 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺‘𝑧)‘𝑖) ∈ ℂ) |
110 | 103, 105,
109 | fsumser 14308 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) →
Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖) = (seq0( + , (𝐺‘𝑧))‘𝑚)) |
111 | 96, 102, 110 | 3eqtrd 2648 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧) = (seq0( + , (𝐺‘𝑧))‘𝑚)) |
112 | 111 | mpteq2dva 4672 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚))) |
113 | | 0z 11265 |
. . . . . . 7
⊢ 0 ∈
ℤ |
114 | | seqfn 12675 |
. . . . . . 7
⊢ (0 ∈
ℤ → seq0( + , (𝐺‘𝑧)) Fn
(ℤ≥‘0)) |
115 | 113, 114 | ax-mp 5 |
. . . . . 6
⊢ seq0( + ,
(𝐺‘𝑧)) Fn
(ℤ≥‘0) |
116 | 1 | fneq2i 5900 |
. . . . . 6
⊢ (seq0( +
, (𝐺‘𝑧)) Fn ℕ0 ↔
seq0( + , (𝐺‘𝑧)) Fn
(ℤ≥‘0)) |
117 | 115, 116 | mpbir 220 |
. . . . 5
⊢ seq0( + ,
(𝐺‘𝑧)) Fn ℕ0 |
118 | | dffn5 6151 |
. . . . 5
⊢ (seq0( +
, (𝐺‘𝑧)) Fn ℕ0 ↔
seq0( + , (𝐺‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚))) |
119 | 117, 118 | mpbi 219 |
. . . 4
⊢ seq0( + ,
(𝐺‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚)) |
120 | 112, 119 | syl6eqr 2662 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) = seq0( + , (𝐺‘𝑧))) |
121 | | fvres 6117 |
. . . 4
⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
122 | 121 | adantl 481 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
123 | 89, 120, 122 | 3brtr4d 4615 |
. 2
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) ⇝ ((𝐹 ↾ 𝐵)‘𝑧)) |
124 | 94 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
125 | 124 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)) = (ℂ D (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)))) |
126 | | eqid 2610 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
127 | 126 | cnfldtop 22397 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
128 | 126 | cnfldtopon 22396 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
129 | 128 | toponunii 20547 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
130 | 129 | restid 15917 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
131 | 127, 130 | ax-mp 5 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
132 | 131 | eqcomi 2619 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
133 | 2 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ℂ
∈ {ℝ, ℂ}) |
134 | 126 | cnfldtopn 22395 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
135 | 134 | blopn 22115 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∈
(TopOpen‘ℂfld)) |
136 | 11, 12, 19, 135 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∈
(TopOpen‘ℂfld)) |
137 | 9, 136 | syl5eqel 2692 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ∈
(TopOpen‘ℂfld)) |
138 | 137 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ∈
(TopOpen‘ℂfld)) |
139 | | fzfid 12634 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) →
(0...𝑚) ∈
Fin) |
140 | 7 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) |
141 | 140 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
142 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ⊆
ℂ) |
143 | 142 | sselda 3568 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
144 | 143 | 3adant2 1073 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
145 | 6, 141, 144 | psergf 23970 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦):ℕ0⟶ℂ) |
146 | 107 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝑖 ∈ ℕ0) |
147 | 145, 146 | ffvelrnd 6268 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
148 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ℂ ∈ {ℝ,
ℂ}) |
149 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → (𝐴‘𝑖) ∈ ℂ) |
150 | 140, 107,
149 | syl2an 493 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝐴‘𝑖) ∈ ℂ) |
151 | 150 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → (𝐴‘𝑖) ∈ ℂ) |
152 | 143 | adantlr 747 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
153 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
154 | 107 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0) |
155 | | expcl 12740 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑦↑𝑖) ∈
ℂ) |
156 | 153, 154,
155 | syl2anr 494 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑖) ∈ ℂ) |
157 | 152, 156 | syldan 486 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → (𝑦↑𝑖) ∈ ℂ) |
158 | 151, 157 | mulcld 9939 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · (𝑦↑𝑖)) ∈ ℂ) |
159 | | ovex 6577 |
. . . . . . . . 9
⊢ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V |
160 | 159 | a1i 11 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V) |
161 | | c0ex 9913 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
162 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑖 · (𝑦↑(𝑖 − 1))) ∈ V |
163 | 161, 162 | ifex 4106 |
. . . . . . . . . 10
⊢ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V |
164 | 163 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V) |
165 | 163 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V) |
166 | | dvexp2 23523 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
→ (ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
167 | 154, 166 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
168 | 22 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ⊆ ℂ) |
169 | 137 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ∈
(TopOpen‘ℂfld)) |
170 | 148, 156,
165, 167, 168, 132, 126, 169 | dvmptres 23532 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ (𝑦↑𝑖))) = (𝑦 ∈ 𝐵 ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
171 | 148, 157,
164, 170, 150 | dvmptcmul 23533 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
172 | 148, 158,
160, 171 | dvmptcl 23528 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
173 | 172 | 3impa 1251 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
174 | 107 | ad2antlr 759 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → 𝑖 ∈ ℕ0) |
175 | 6 | pserval2 23969 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ ((𝐺‘𝑦)‘𝑖) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
176 | 152, 174,
175 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑦)‘𝑖) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
177 | 176 | mpteq2dva 4672 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
178 | 177 | oveq2d 6565 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖))) = (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖))))) |
179 | 178, 171 | eqtrd 2644 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖))) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
180 | 132, 126,
133, 138, 139, 147, 173, 179 | dvmptfsum 23542 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
181 | 125, 180 | eqtrd 2644 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
182 | 181 | mpteq2dva 4672 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))) |
183 | | nnssnn0 11172 |
. . . . . 6
⊢ ℕ
⊆ ℕ0 |
184 | | resmpt 5369 |
. . . . . 6
⊢ (ℕ
⊆ ℕ0 → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))) |
185 | 183, 184 | ax-mp 5 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
186 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝑎↑𝑖) = (𝑥↑𝑖)) |
187 | 186 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) |
188 | 187 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖)))) |
189 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝑖 + 1) = (𝑛 + 1)) |
190 | 189 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑛 + 1))) |
191 | 189, 190 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
192 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (𝑥↑𝑖) = (𝑥↑𝑛)) |
193 | 191, 192 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
194 | 193 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
195 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
196 | 195 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝐴‘(𝑚 + 1)) = (𝐴‘(𝑛 + 1))) |
197 | 195, 196 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
198 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1)))) = (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))) |
199 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) ∈ V |
200 | 197, 198,
199 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
201 | 200 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
202 | 201 | mpteq2ia 4668 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ (((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
203 | 194, 202 | eqtr4i 2635 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛))) |
204 | 188, 203 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)))) |
205 | 204 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)))) |
206 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)) |
207 | 206 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
208 | 207 | sumeq2sdv 14282 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
209 | 208 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘)) = (𝑧 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
210 | | peano2nn0 11210 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
211 | 210 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℕ0) |
212 | 211 | nn0cnd 11230 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℂ) |
213 | 140, 211 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝐴‘(𝑚 + 1)) ∈ ℂ) |
214 | 212, 213 | mulcld 9939 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) ∈ ℂ) |
215 | 214, 198 | fmptd 6292 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 +
1)))):ℕ0⟶ℂ) |
216 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑗 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) |
217 | 216 | seqeq3d 12671 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑗 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗))) |
218 | 217 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑗 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + ,
((𝑎 ∈ ℂ ↦
(𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ )) |
219 | 218 | cbvrabv 3172 |
. . . . . . . . 9
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, ((𝑎 ∈ ℂ
↦ (𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ } = {𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ } |
220 | 219 | supeq1i 8236 |
. . . . . . . 8
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑗 ∈
ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ }, ℝ*,
< ) |
221 | 206 | seqeq3d 12671 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))) |
222 | 221 | fveq1d 6105 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) |
223 | 222 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) |
224 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚)) |
225 | 224 | mpteq2dv 4673 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
226 | 223, 225 | syl5eq 2656 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
227 | 226 | cbvmptv 4678 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
228 | 18 | rpred 11748 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ) |
229 | 6, 13, 7, 14, 15, 16 | psercnlem1 23983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |
230 | 229 | simp1d 1066 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
231 | 230 | rpxrd 11749 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ*) |
232 | 205, 215,
220 | radcnvcl 23975 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ (0[,]+∞)) |
233 | 58, 232 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
234 | 229 | simp2d 1067 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) |
235 | | cnvimass 5404 |
. . . . . . . . . . . . . . . 16
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
236 | | absf 13925 |
. . . . . . . . . . . . . . . . 17
⊢
abs:ℂ⟶ℝ |
237 | 236 | fdmi 5965 |
. . . . . . . . . . . . . . . 16
⊢ dom abs =
ℂ |
238 | 235, 237 | sseqtri 3600 |
. . . . . . . . . . . . . . 15
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
239 | 15, 238 | eqsstri 3598 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ⊆
ℂ |
240 | 239 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
241 | 240 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
242 | 241 | abscld 14023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
243 | 230 | rpred 11748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
244 | | avglt2 11148 |
. . . . . . . . . . 11
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑀
∈ ℝ) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀)) |
245 | 242, 243,
244 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀)) |
246 | 234, 245 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑀) |
247 | 230 | rpge0d 11752 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ 𝑀) |
248 | 243, 247 | absidd 14009 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) = 𝑀) |
249 | 230 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℂ) |
250 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑀 → (𝑤↑𝑖) = (𝑀↑𝑖)) |
251 | 250 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑀 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) |
252 | 251 | mpteq2dv 4673 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑀 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
253 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑤 → (𝑎↑𝑖) = (𝑤↑𝑖)) |
254 | 253 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑤 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖))) |
255 | 254 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑤 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)))) |
256 | 255 | cbvmptv 4678 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑤 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)))) |
257 | | nn0ex 11175 |
. . . . . . . . . . . . . . . 16
⊢
ℕ0 ∈ V |
258 | 257 | mptex 6390 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) ∈ V |
259 | 252, 256,
258 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
260 | 249, 259 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
261 | 260 | seqeq3d 12671 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀)) = seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))))) |
262 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝐴‘𝑛) = (𝐴‘𝑖)) |
263 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑥↑𝑛) = (𝑥↑𝑖)) |
264 | 262, 263 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑖) · (𝑥↑𝑖))) |
265 | 264 | cbvmptv 4678 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑥↑𝑖))) |
266 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥↑𝑖) = (𝑦↑𝑖)) |
267 | 266 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐴‘𝑖) · (𝑥↑𝑖)) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
268 | 267 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑥↑𝑖))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
269 | 265, 268 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
270 | 269 | cbvmptv 4678 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
271 | 6, 270 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
272 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (𝐺‘𝑟) = (𝐺‘𝑠)) |
273 | 272 | seqeq3d 12671 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑠))) |
274 | 273 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑠 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ )) |
275 | 274 | cbvrabv 3172 |
. . . . . . . . . . . . . . 15
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑠 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑠)) ∈ dom ⇝
} |
276 | 275 | supeq1i 8236 |
. . . . . . . . . . . . . 14
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑠 ∈
ℝ ∣ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ }, ℝ*,
< ) |
277 | 14, 276 | eqtri 2632 |
. . . . . . . . . . . . 13
⊢ 𝑅 = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ }, ℝ*,
< ) |
278 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) |
279 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) |
280 | 229 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) |
281 | 248, 280 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) < 𝑅) |
282 | 271, 277,
278, 279, 249, 281 | dvradcnv 23979 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) ∈ dom ⇝ ) |
283 | 261, 282 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀)) ∈ dom ⇝ ) |
284 | 205, 215,
220, 249, 283 | radcnvle 23978 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
285 | 248, 284 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
286 | 19, 231, 233, 246, 285 | xrltletrd 11868 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
287 | 205, 209,
215, 220, 227, 228, 286, 45 | pserulm 23980 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘))) |
288 | 22 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
289 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑦 → (𝑎↑𝑖) = (𝑦↑𝑖)) |
290 | 289 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑦 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) |
291 | 290 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑦 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
292 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) |
293 | 257 | mptex 6390 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) ∈ V |
294 | 291, 292,
293 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
295 | 288, 294 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
296 | 295 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
297 | 296 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘)) |
298 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
299 | 298 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑘 + 1))) |
300 | 298, 299 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) |
301 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑦↑𝑖) = (𝑦↑𝑘)) |
302 | 300, 301 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
303 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) |
304 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) ∈ V |
305 | 302, 303,
304 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
306 | 305 | adantl 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
307 | 297, 306 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
308 | 307 | sumeq2dv 14281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
309 | 308 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
310 | 287, 309 | breqtrd 4609 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
311 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
312 | | 1e0p1 11428 |
. . . . . . . . 9
⊢ 1 = (0 +
1) |
313 | 312 | fveq2i 6106 |
. . . . . . . 8
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
314 | 311, 313 | eqtri 2632 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘(0 + 1)) |
315 | | 1zzd 11285 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 1 ∈ ℤ) |
316 | | 0zd 11266 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 0 ∈ ℤ) |
317 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
318 | 317 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℂ) |
319 | 318 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑖 + 1) ∈
ℂ) |
320 | 7 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
321 | | ffvelrn 6265 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴:ℕ0⟶ℂ ∧
(𝑖 + 1) ∈
ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ) |
322 | 320, 317,
321 | syl2an 493 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ) |
323 | 319, 322 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) ∈ ℂ) |
324 | 288, 155 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑦↑𝑖) ∈ ℂ) |
325 | 323, 324 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)) ∈ ℂ) |
326 | 325, 303 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))):ℕ0⟶ℂ) |
327 | 295 | feq1d 5943 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦):ℕ0⟶ℂ ↔
(𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))):ℕ0⟶ℂ)) |
328 | 326, 327 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦):ℕ0⟶ℂ) |
329 | 328 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑚) ∈ ℂ) |
330 | 1, 316, 329 | serf 12691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)):ℕ0⟶ℂ) |
331 | 330 | ffvelrnda 6267 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → (seq0( +
, ((𝑎 ∈ ℂ
↦ (𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) ∈ ℂ) |
332 | 331 | an32s 842 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) ∈ ℂ) |
333 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) |
334 | 332, 333 | fmptd 6292 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ) |
335 | 32, 34 | elmap 7772 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑𝑚
𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ) |
336 | 334, 335 | sylibr 223 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑𝑚
𝐵)) |
337 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) = (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) |
338 | 336, 337 | fmptd 6292 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))):ℕ0⟶(ℂ
↑𝑚 𝐵)) |
339 | | elfznn 12241 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ) |
340 | 339 | nnne0d 10942 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ≠ 0) |
341 | 340 | neneqd 2787 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑚) → ¬ 𝑖 = 0) |
342 | 341 | iffalsed 4047 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑚) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = (𝑖 · (𝑦↑(𝑖 − 1)))) |
343 | 342 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑚) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))) |
344 | 343 | sumeq2i 14277 |
. . . . . . . . . . . 12
⊢
Σ𝑖 ∈
(1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) |
345 | | 1zzd 11285 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 1 ∈ ℤ) |
346 | | nnz 11276 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
347 | 346 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑚 ∈ ℤ) |
348 | 279 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
349 | 339 | nnnn0d 11228 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ0) |
350 | 348, 349,
149 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝐴‘𝑖) ∈ ℂ) |
351 | 339 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ) |
352 | 351 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℂ) |
353 | 288 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
354 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (𝑖 − 1) ∈
ℕ0) |
355 | 339, 354 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑚) → (𝑖 − 1) ∈
ℕ0) |
356 | | expcl 12740 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℂ ∧ (𝑖 − 1) ∈
ℕ0) → (𝑦↑(𝑖 − 1)) ∈ ℂ) |
357 | 353, 355,
356 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑦↑(𝑖 − 1)) ∈ ℂ) |
358 | 352, 357 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑖 · (𝑦↑(𝑖 − 1))) ∈
ℂ) |
359 | 350, 358 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) ∈
ℂ) |
360 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝐴‘𝑖) = (𝐴‘(𝑘 + 1))) |
361 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1)) |
362 | | oveq1 6556 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑘 + 1) → (𝑖 − 1) = ((𝑘 + 1) − 1)) |
363 | 362 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑘 + 1) → (𝑦↑(𝑖 − 1)) = (𝑦↑((𝑘 + 1) − 1))) |
364 | 361, 363 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (𝑦↑(𝑖 − 1))) = ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) |
365 | 360, 364 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
366 | 345, 345,
347, 359, 365 | fsumshftm 14355 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
367 | 344, 366 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
368 | 312 | oveq1i 6559 |
. . . . . . . . . . . . . 14
⊢
(1...𝑚) = ((0 +
1)...𝑚) |
369 | | fzp1ss 12262 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℤ → ((0 + 1)...𝑚) ⊆ (0...𝑚)) |
370 | 113, 369 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((0 +
1)...𝑚) ⊆ (0...𝑚) |
371 | 368, 370 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢
(1...𝑚) ⊆
(0...𝑚) |
372 | 371 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (1...𝑚) ⊆ (0...𝑚)) |
373 | 343 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))) |
374 | 373, 359 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
375 | | eldif 3550 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) ↔ (𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚))) |
376 | | elfzuz2 12217 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (0...𝑚) → 𝑚 ∈
(ℤ≥‘0)) |
377 | | elfzp12 12288 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈
(ℤ≥‘0) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))) |
378 | 376, 377 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (0...𝑚) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))) |
379 | 378 | ibi 255 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0...𝑚) → (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))) |
380 | 379 | ord 391 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0...𝑚) → (¬ 𝑖 = 0 → 𝑖 ∈ ((0 + 1)...𝑚))) |
381 | 380 | con1d 138 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0...𝑚) → (¬ 𝑖 ∈ ((0 + 1)...𝑚) → 𝑖 = 0)) |
382 | 381 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)) → 𝑖 = 0) |
383 | 375, 382 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) → 𝑖 = 0) |
384 | 368 | difeq2i 3687 |
. . . . . . . . . . . . . . . . 17
⊢
((0...𝑚) ∖
(1...𝑚)) = ((0...𝑚) ∖ ((0 + 1)...𝑚)) |
385 | 383, 384 | eleq2s 2706 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 = 0) |
386 | 385 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → 𝑖 = 0) |
387 | 386 | iftrued 4044 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = 0) |
388 | 387 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · 0)) |
389 | | eldifi 3694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ (0...𝑚)) |
390 | 389, 107 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ ℕ0) |
391 | 348, 390,
149 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → (𝐴‘𝑖) ∈ ℂ) |
392 | 391 | mul01d 10114 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · 0) = 0) |
393 | 388, 392 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = 0) |
394 | | fzfid 12634 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (0...𝑚) ∈ Fin) |
395 | 372, 374,
393, 394 | fsumss 14303 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
396 | | 1m1e0 10966 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
397 | 396 | oveq1i 6559 |
. . . . . . . . . . . . 13
⊢ ((1
− 1)...(𝑚 − 1))
= (0...(𝑚 −
1)) |
398 | 397 | sumeq1i 14276 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈ ((1
− 1)...(𝑚 −
1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) |
399 | | elfznn0 12302 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...(𝑚 − 1)) → 𝑘 ∈ ℕ0) |
400 | 399 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℕ0) |
401 | 400, 305 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
402 | 353 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑦 ∈ ℂ) |
403 | 402, 294 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
404 | 403 | fveq1d 6105 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘)) |
405 | 348 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝐴:ℕ0⟶ℂ) |
406 | | peano2nn0 11210 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
407 | 400, 406 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈
ℕ0) |
408 | 405, 407 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝐴‘(𝑘 + 1)) ∈ ℂ) |
409 | 407 | nn0cnd 11230 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℂ) |
410 | | expcl 12740 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑦↑𝑘) ∈
ℂ) |
411 | 353, 399,
410 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑𝑘) ∈ ℂ) |
412 | 408, 409,
411 | mul12d 10124 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑𝑘))) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦↑𝑘)))) |
413 | 400 | nn0cnd 11230 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℂ) |
414 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
415 | | pncan 10166 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
416 | 413, 414,
415 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) − 1) = 𝑘) |
417 | 416 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) = (𝑦↑𝑘)) |
418 | 417 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑦↑𝑘))) |
419 | 418 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑𝑘)))) |
420 | 409, 408,
411 | mulassd 9942 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦↑𝑘)))) |
421 | 412, 419,
420 | 3eqtr4d 2654 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
422 | 401, 404,
421 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
423 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → (𝑚 − 1) ∈
ℕ0) |
424 | 423 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈
ℕ0) |
425 | 424 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑚 − 1) ∈
ℕ0) |
426 | 425, 1 | syl6eleq 2698 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑚 − 1) ∈
(ℤ≥‘0)) |
427 | 417, 411 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) ∈
ℂ) |
428 | 409, 427 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) ∈
ℂ) |
429 | 408, 428 | mulcld 9939 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) ∈
ℂ) |
430 | 422, 426,
429 | fsumser 14308 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
431 | 398, 430 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
432 | 367, 395,
431 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
433 | 432 | mpteq2dva 4672 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
434 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑚 − 1) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
435 | 434 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑚 − 1) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
436 | 34 | mptex 6390 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) ∈ V |
437 | 435, 337,
436 | fvmpt 6191 |
. . . . . . . . . 10
⊢ ((𝑚 − 1) ∈
ℕ0 → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
438 | 424, 437 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
439 | 433, 438 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1))) |
440 | 439 | mpteq2dva 4672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ ↦ ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)))) |
441 | 1, 314, 4, 315, 338, 440 | ulmshft 23948 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) ↔ (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))) |
442 | 310, 441 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
443 | 185, 442 | syl5eqbr 4618 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾
ℕ)(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
444 | | 1nn0 11185 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
445 | 444 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 1 ∈
ℕ0) |
446 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (0...𝑚) ∈ Fin) |
447 | 172 | an32s 842 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
448 | 446, 447 | fsumcl 14311 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
449 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
450 | 448, 449 | fmptd 6292 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ) |
451 | 32, 34 | elmap 7772 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ
↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ) |
452 | 450, 451 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ
↑𝑚 𝐵)) |
453 | | eqid 2610 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
454 | 452, 453 | fmptd 6292 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1))))))):ℕ0⟶(ℂ ↑𝑚 𝐵)) |
455 | 1, 311, 445, 454 | ulmres 23946 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) ↔ ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾
ℕ)(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))) |
456 | 443, 455 | mpbird 246 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
457 | 182, 456 | eqbrtrd 4605 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
458 | 1, 3, 4, 38, 48, 123, 457 | ulmdv 23961 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |