Step | Hyp | Ref
| Expression |
1 | | nn0uz 11722 |
. 2
⊢
ℕ0 = (ℤ≥‘0) |
2 | | cnelprrecn 10029 |
. . 3
⊢ ℂ
∈ {ℝ, ℂ} |
3 | 2 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ℂ ∈ {ℝ,
ℂ}) |
4 | | 0zd 11389 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ∈ ℤ) |
5 | | fzfid 12772 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (0...𝑘) ∈ Fin) |
6 | | pserf.g |
. . . . . . . 8
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
7 | | pserf.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
8 | 7 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
9 | | pserdv.b |
. . . . . . . . . . 11
⊢ 𝐵 = (0(ball‘(abs ∘
− ))(((abs‘𝑎) +
𝑀) / 2)) |
10 | | cnxmet 22576 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
11 | 10 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
12 | | 0cnd 10033 |
. . . . . . . . . . . 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 24181 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧
(abs‘𝑎) <
(((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅)) |
18 | 17 | simp1d 1073 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ+) |
19 | 18 | rpxrd 11873 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
20 | | blssm 22223 |
. . . . . . . . . . . 12
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
21 | 11, 12, 19, 20 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆
ℂ) |
22 | 9, 21 | syl5eqss 3649 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ ℂ) |
23 | 22 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → 𝐵 ⊆
ℂ) |
24 | 23 | sselda 3603 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
25 | 6, 8, 24 | psergf 24166 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦):ℕ0⟶ℂ) |
26 | | elfznn0 12433 |
. . . . . . 7
⊢ (𝑖 ∈ (0...𝑘) → 𝑖 ∈ ℕ0) |
27 | | ffvelrn 6357 |
. . . . . . 7
⊢ (((𝐺‘𝑦):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
28 | 25, 26, 27 | syl2an 494 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (0...𝑘)) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
29 | 5, 28 | fsumcl 14464 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
30 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) |
31 | 29, 30 | fmptd 6385 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)):𝐵⟶ℂ) |
32 | | cnex 10017 |
. . . . 5
⊢ ℂ
∈ V |
33 | | ovex 6678 |
. . . . . 6
⊢
(0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∈ V |
34 | 9, 33 | eqeltri 2697 |
. . . . 5
⊢ 𝐵 ∈ V |
35 | 32, 34 | elmap 7886 |
. . . 4
⊢ ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) ∈ (ℂ ↑𝑚
𝐵) ↔ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)):𝐵⟶ℂ) |
36 | 31, 35 | sylibr 224 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑘 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) ∈ (ℂ ↑𝑚
𝐵)) |
37 | | eqid 2622 |
. . 3
⊢ (𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))) = (𝑘 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))) |
38 | 36, 37 | fmptd 6385 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑘 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖))):ℕ0⟶(ℂ
↑𝑚 𝐵)) |
39 | 6, 13, 7, 14, 15, 16 | psercn 24180 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |
40 | | cncff 22696 |
. . . . 5
⊢ (𝐹 ∈ (𝑆–cn→ℂ) → 𝐹:𝑆⟶ℂ) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
42 | 41 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
43 | 6, 13, 7, 14, 15, 17 | psercnlem2 24178 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs
∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆)) |
44 | 43 | simp2d 1074 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2)))) |
45 | 9, 44 | syl5eqss 3649 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2)))) |
46 | 43 | simp3d 1075 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (◡abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆) |
47 | 45, 46 | sstrd 3613 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ⊆ 𝑆) |
48 | 42, 47 | fssresd 6071 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝐹 ↾ 𝐵):𝐵⟶ℂ) |
49 | | 0zd 11389 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 0 ∈ ℤ) |
50 | | eqidd 2623 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑧)‘𝑗) = ((𝐺‘𝑧)‘𝑗)) |
51 | 7 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
52 | 22 | sselda 3603 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ ℂ) |
53 | 6, 51, 52 | psergf 24166 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝐺‘𝑧):ℕ0⟶ℂ) |
54 | 53 | ffvelrnda 6359 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → ((𝐺‘𝑧)‘𝑗) ∈ ℂ) |
55 | 52 | abscld 14175 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) ∈ ℝ) |
56 | 55 | rexrd 10089 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) ∈
ℝ*) |
57 | 19 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (((abs‘𝑎) + 𝑀) / 2) ∈
ℝ*) |
58 | | iccssxr 12256 |
. . . . . . . . 9
⊢
(0[,]+∞) ⊆ ℝ* |
59 | 6, 7, 14 | radcnvcl 24171 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ (0[,]+∞)) |
60 | 58, 59 | sseldi 3601 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈
ℝ*) |
61 | 60 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑅 ∈
ℝ*) |
62 | | 0cn 10032 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
63 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) = (abs ∘ − ) |
64 | 63 | cnmetdval 22574 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑧(abs
∘ − )0) = (abs‘(𝑧 − 0))) |
65 | 52, 62, 64 | sylancl 694 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0))) |
66 | 52 | subid1d 10381 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧 − 0) = 𝑧) |
67 | 66 | fveq2d 6195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘(𝑧 − 0)) = (abs‘𝑧)) |
68 | 65, 67 | eqtrd 2656 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) = (abs‘𝑧)) |
69 | | simpr 477 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝐵) |
70 | 69, 9 | syl6eleq 2711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2))) |
71 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
72 | | 0cnd 10033 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 0 ∈ ℂ) |
73 | | elbl3 22197 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) ∧ (0
∈ ℂ ∧ 𝑧
∈ ℂ)) → (𝑧
∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2))) |
74 | 71, 57, 72, 52, 73 | syl22anc 1327 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧 ∈ (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ↔ (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2))) |
75 | 70, 74 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑧(abs ∘ − )0) <
(((abs‘𝑎) + 𝑀) / 2)) |
76 | 68, 75 | eqbrtrrd 4677 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) < (((abs‘𝑎) + 𝑀) / 2)) |
77 | 17 | simp3d 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅) |
78 | 77 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (((abs‘𝑎) + 𝑀) / 2) < 𝑅) |
79 | 56, 57, 61, 76, 78 | xrlttrd 11990 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (abs‘𝑧) < 𝑅) |
80 | 6, 51, 14, 52, 79 | radcnvlt2 24173 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ∈ dom ⇝ ) |
81 | 1, 49, 50, 54, 80 | isumclim2 14489 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ⇝ Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
82 | 47 | sselda 3603 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ 𝑆) |
83 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝐺‘𝑦) = (𝐺‘𝑧)) |
84 | 83 | fveq1d 6193 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑗) = ((𝐺‘𝑧)‘𝑗)) |
85 | 84 | sumeq2sdv 14435 |
. . . . . 6
⊢ (𝑦 = 𝑧 → Σ𝑗 ∈ ℕ0 ((𝐺‘𝑦)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
86 | | sumex 14418 |
. . . . . 6
⊢
Σ𝑗 ∈
ℕ0 ((𝐺‘𝑧)‘𝑗) ∈ V |
87 | 85, 13, 86 | fvmpt 6282 |
. . . . 5
⊢ (𝑧 ∈ 𝑆 → (𝐹‘𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
88 | 82, 87 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝐹‘𝑧) = Σ𝑗 ∈ ℕ0 ((𝐺‘𝑧)‘𝑗)) |
89 | 81, 88 | breqtrrd 4681 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → seq0( + , (𝐺‘𝑧)) ⇝ (𝐹‘𝑧)) |
90 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (0...𝑘) = (0...𝑚)) |
91 | 90 | sumeq1d 14431 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑚 → Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) |
92 | 91 | mpteq2dv 4745 |
. . . . . . . . 9
⊢ (𝑘 = 𝑚 → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
93 | 34 | mptex 6486 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) ∈ V |
94 | 92, 37, 93 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
95 | 94 | adantl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
96 | 95 | fveq1d 6193 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧) = ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧)) |
97 | 83 | fveq1d 6193 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → ((𝐺‘𝑦)‘𝑖) = ((𝐺‘𝑧)‘𝑖)) |
98 | 97 | sumeq2sdv 14435 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
99 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)) |
100 | | sumex 14418 |
. . . . . . . 8
⊢
Σ𝑖 ∈
(0...𝑚)((𝐺‘𝑧)‘𝑖) ∈ V |
101 | 98, 99, 100 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑧 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
102 | 101 | ad2antlr 763 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))‘𝑧) = Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖)) |
103 | | eqidd 2623 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺‘𝑧)‘𝑖) = ((𝐺‘𝑧)‘𝑖)) |
104 | | simpr 477 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
105 | 104, 1 | syl6eleq 2711 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
(ℤ≥‘0)) |
106 | 53 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (𝐺‘𝑧):ℕ0⟶ℂ) |
107 | | elfznn0 12433 |
. . . . . . . 8
⊢ (𝑖 ∈ (0...𝑚) → 𝑖 ∈ ℕ0) |
108 | | ffvelrn 6357 |
. . . . . . . 8
⊢ (((𝐺‘𝑧):ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → ((𝐺‘𝑧)‘𝑖) ∈ ℂ) |
109 | 106, 107,
108 | syl2an 494 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐺‘𝑧)‘𝑖) ∈ ℂ) |
110 | 103, 105,
109 | fsumser 14461 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) →
Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑧)‘𝑖) = (seq0( + , (𝐺‘𝑧))‘𝑚)) |
111 | 96, 102, 110 | 3eqtrd 2660 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧) = (seq0( + , (𝐺‘𝑧))‘𝑚)) |
112 | 111 | mpteq2dva 4744 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚))) |
113 | | 0z 11388 |
. . . . . . 7
⊢ 0 ∈
ℤ |
114 | | seqfn 12813 |
. . . . . . 7
⊢ (0 ∈
ℤ → seq0( + , (𝐺‘𝑧)) Fn
(ℤ≥‘0)) |
115 | 113, 114 | ax-mp 5 |
. . . . . 6
⊢ seq0( + ,
(𝐺‘𝑧)) Fn
(ℤ≥‘0) |
116 | 1 | fneq2i 5986 |
. . . . . 6
⊢ (seq0( +
, (𝐺‘𝑧)) Fn ℕ0 ↔
seq0( + , (𝐺‘𝑧)) Fn
(ℤ≥‘0)) |
117 | 115, 116 | mpbir 221 |
. . . . 5
⊢ seq0( + ,
(𝐺‘𝑧)) Fn ℕ0 |
118 | | dffn5 6241 |
. . . . 5
⊢ (seq0( +
, (𝐺‘𝑧)) Fn ℕ0 ↔
seq0( + , (𝐺‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚))) |
119 | 117, 118 | mpbi 220 |
. . . 4
⊢ seq0( + ,
(𝐺‘𝑧)) = (𝑚 ∈ ℕ0 ↦ (seq0( +
, (𝐺‘𝑧))‘𝑚)) |
120 | 112, 119 | syl6eqr 2674 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) = seq0( + , (𝐺‘𝑧))) |
121 | | fvres 6207 |
. . . 4
⊢ (𝑧 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
122 | 121 | adantl 482 |
. . 3
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → ((𝐹 ↾ 𝐵)‘𝑧) = (𝐹‘𝑧)) |
123 | 89, 120, 122 | 3brtr4d 4685 |
. 2
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑧 ∈ 𝐵) → (𝑚 ∈ ℕ0 ↦ (((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)‘𝑧)) ⇝ ((𝐹 ↾ 𝐵)‘𝑧)) |
124 | 94 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) |
125 | 124 | oveq2d 6666 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)) = (ℂ D (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖)))) |
126 | | eqid 2622 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
127 | 126 | cnfldtop 22587 |
. . . . . . . 8
⊢
(TopOpen‘ℂfld) ∈ Top |
128 | 126 | cnfldtopon 22586 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
129 | 128 | toponunii 20721 |
. . . . . . . . 9
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
130 | 129 | restid 16094 |
. . . . . . . 8
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
131 | 127, 130 | ax-mp 5 |
. . . . . . 7
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
132 | 131 | eqcomi 2631 |
. . . . . 6
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
133 | 2 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ℂ
∈ {ℝ, ℂ}) |
134 | 126 | cnfldtopn 22585 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
135 | 134 | blopn 22305 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ (((abs‘𝑎) +
𝑀) / 2) ∈
ℝ*) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∈
(TopOpen‘ℂfld)) |
136 | 11, 12, 19, 135 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (0(ball‘(abs ∘ −
))(((abs‘𝑎) + 𝑀) / 2)) ∈
(TopOpen‘ℂfld)) |
137 | 9, 136 | syl5eqel 2705 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐵 ∈
(TopOpen‘ℂfld)) |
138 | 137 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ∈
(TopOpen‘ℂfld)) |
139 | | fzfid 12772 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) →
(0...𝑚) ∈
Fin) |
140 | 7 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐴:ℕ0⟶ℂ) |
141 | 140 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
142 | 22 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → 𝐵 ⊆
ℂ) |
143 | 142 | sselda 3603 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
144 | 143 | 3adant2 1080 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
145 | 6, 141, 144 | psergf 24166 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → (𝐺‘𝑦):ℕ0⟶ℂ) |
146 | 107 | 3ad2ant2 1083 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → 𝑖 ∈ ℕ0) |
147 | 145, 146 | ffvelrnd 6360 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑦)‘𝑖) ∈ ℂ) |
148 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → ℂ ∈ {ℝ,
ℂ}) |
149 | | ffvelrn 6357 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ0⟶ℂ ∧
𝑖 ∈
ℕ0) → (𝐴‘𝑖) ∈ ℂ) |
150 | 140, 107,
149 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝐴‘𝑖) ∈ ℂ) |
151 | 150 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → (𝐴‘𝑖) ∈ ℂ) |
152 | 143 | adantlr 751 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
153 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → 𝑦 ∈
ℂ) |
154 | 107 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝑖 ∈ ℕ0) |
155 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑦↑𝑖) ∈
ℂ) |
156 | 153, 154,
155 | syl2anr 495 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → (𝑦↑𝑖) ∈ ℂ) |
157 | 152, 156 | syldan 487 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → (𝑦↑𝑖) ∈ ℂ) |
158 | 151, 157 | mulcld 10060 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · (𝑦↑𝑖)) ∈ ℂ) |
159 | | ovexd 6680 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈ V) |
160 | | c0ex 10034 |
. . . . . . . . . . 11
⊢ 0 ∈
V |
161 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑖 · (𝑦↑(𝑖 − 1))) ∈ V |
162 | 160, 161 | ifex 4156 |
. . . . . . . . . 10
⊢ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V |
163 | 162 | a1i 11 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V) |
164 | 162 | a1i 11 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ ℂ) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) ∈ V) |
165 | | dvexp2 23717 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
→ (ℂ D (𝑦 ∈
ℂ ↦ (𝑦↑𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
166 | 154, 165 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ ℂ ↦ (𝑦↑𝑖))) = (𝑦 ∈ ℂ ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
167 | 22 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ⊆ ℂ) |
168 | 137 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → 𝐵 ∈
(TopOpen‘ℂfld)) |
169 | 148, 156,
164, 166, 167, 132, 126, 168 | dvmptres 23726 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ (𝑦↑𝑖))) = (𝑦 ∈ 𝐵 ↦ if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
170 | 148, 157,
163, 169, 150 | dvmptcmul 23727 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
171 | 148, 158,
159, 170 | dvmptcl 23722 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
172 | 171 | 3impa 1259 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚) ∧ 𝑦 ∈ 𝐵) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
173 | 107 | ad2antlr 763 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → 𝑖 ∈ ℕ0) |
174 | 6 | pserval2 24165 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ ((𝐺‘𝑦)‘𝑖) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
175 | 152, 173,
174 | syl2anc 693 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) ∧ 𝑦 ∈ 𝐵) → ((𝐺‘𝑦)‘𝑖) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
176 | 175 | mpteq2dva 4744 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖)) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
177 | 176 | oveq2d 6666 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖))) = (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖))))) |
178 | 177, 170 | eqtrd 2656 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑚)) → (ℂ D (𝑦 ∈ 𝐵 ↦ ((𝐺‘𝑦)‘𝑖))) = (𝑦 ∈ 𝐵 ↦ ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
179 | 132, 126,
133, 138, 139, 147, 172, 178 | dvmptfsum 23738 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐺‘𝑦)‘𝑖))) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
180 | 125, 179 | eqtrd 2656 |
. . . 4
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
181 | 180 | mpteq2dva 4744 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚))) = (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))) |
182 | | nnssnn0 11295 |
. . . . . 6
⊢ ℕ
⊆ ℕ0 |
183 | | resmpt 5449 |
. . . . . 6
⊢ (ℕ
⊆ ℕ0 → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))))) |
184 | 182, 183 | ax-mp 5 |
. . . . 5
⊢ ((𝑚 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾ ℕ) = (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
185 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑥 → (𝑎↑𝑖) = (𝑥↑𝑖)) |
186 | 185 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑥 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) |
187 | 186 | mpteq2dv 4745 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖)))) |
188 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝑖 + 1) = (𝑛 + 1)) |
189 | 188 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑛 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑛 + 1))) |
190 | 188, 189 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
191 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑛 → (𝑥↑𝑖) = (𝑥↑𝑛)) |
192 | 190, 191 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑛 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑥↑𝑖)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
193 | 192 | cbvmptv 4750 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
194 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
195 | 194 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑛 → (𝐴‘(𝑚 + 1)) = (𝐴‘(𝑛 + 1))) |
196 | 194, 195 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
197 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1)))) = (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1)))) |
198 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 + 1) · (𝐴‘(𝑛 + 1))) ∈ V |
199 | 196, 197,
198 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ ((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) = ((𝑛 + 1) · (𝐴‘(𝑛 + 1)))) |
200 | 199 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)) = (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
201 | 200 | mpteq2ia 4740 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ (((𝑚 ∈
ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛))) = (𝑛 ∈ ℕ0 ↦ (((𝑛 + 1) · (𝐴‘(𝑛 + 1))) · (𝑥↑𝑛))) |
202 | 193, 201 | eqtr4i 2647 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑥↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛))) |
203 | 187, 202 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)))) |
204 | 203 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ (((𝑚 ∈ ℕ0
↦ ((𝑚 + 1) ·
(𝐴‘(𝑚 + 1))))‘𝑛) · (𝑥↑𝑛)))) |
205 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)) |
206 | 205 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
207 | 206 | sumeq2sdv 14435 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
208 | 207 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘)) = (𝑧 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧)‘𝑘)) |
209 | | peano2nn0 11333 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
210 | 209 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℕ0) |
211 | 210 | nn0cnd 11353 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑚 + 1) ∈
ℂ) |
212 | 140, 210 | ffvelrnd 6360 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝐴‘(𝑚 + 1)) ∈ ℂ) |
213 | 211, 212 | mulcld 10060 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1) · (𝐴‘(𝑚 + 1))) ∈ ℂ) |
214 | 213, 197 | fmptd 6385 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ ((𝑚 + 1) · (𝐴‘(𝑚 +
1)))):ℕ0⟶ℂ) |
215 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑗 → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟) = ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) |
216 | 215 | seqeq3d 12809 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑗 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗))) |
217 | 216 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑗 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ ↔ seq0( + ,
((𝑎 ∈ ℂ ↦
(𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ )) |
218 | 217 | cbvrabv 3199 |
. . . . . . . . 9
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, ((𝑎 ∈ ℂ
↦ (𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ } = {𝑗 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ } |
219 | 218 | supeq1i 8353 |
. . . . . . . 8
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑗 ∈
ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑗)) ∈ dom ⇝ }, ℝ*,
< ) |
220 | 205 | seqeq3d 12809 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)) = seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))) |
221 | 220 | fveq1d 6193 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) |
222 | 221 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) |
223 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑗 = 𝑚 → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚)) |
224 | 223 | mpteq2dv 4745 |
. . . . . . . . . 10
⊢ (𝑗 = 𝑚 → (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
225 | 222, 224 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝑗 = 𝑚 → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
226 | 225 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) = (𝑚 ∈ ℕ0 ↦ (𝑧 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑧))‘𝑚))) |
227 | 18 | rpred 11872 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ) |
228 | 6, 13, 7, 14, 15, 16 | psercnlem1 24179 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑀 ∈ ℝ+ ∧
(abs‘𝑎) < 𝑀 ∧ 𝑀 < 𝑅)) |
229 | 228 | simp1d 1073 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ+) |
230 | 229 | rpxrd 11873 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈
ℝ*) |
231 | 204, 214,
219 | radcnvcl 24171 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ (0[,]+∞)) |
232 | 58, 231 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
233 | 228 | simp2d 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) < 𝑀) |
234 | | cnvimass 5485 |
. . . . . . . . . . . . . . . 16
⊢ (◡abs “ (0[,)𝑅)) ⊆ dom abs |
235 | | absf 14077 |
. . . . . . . . . . . . . . . . 17
⊢
abs:ℂ⟶ℝ |
236 | 235 | fdmi 6052 |
. . . . . . . . . . . . . . . 16
⊢ dom abs =
ℂ |
237 | 234, 236 | sseqtri 3637 |
. . . . . . . . . . . . . . 15
⊢ (◡abs “ (0[,)𝑅)) ⊆ ℂ |
238 | 15, 237 | eqsstri 3635 |
. . . . . . . . . . . . . 14
⊢ 𝑆 ⊆
ℂ |
239 | 238 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
240 | 239 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ℂ) |
241 | 240 | abscld 14175 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑎) ∈ ℝ) |
242 | 229 | rpred 11872 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℝ) |
243 | | avglt2 11271 |
. . . . . . . . . . 11
⊢
(((abs‘𝑎)
∈ ℝ ∧ 𝑀
∈ ℝ) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀)) |
244 | 241, 242,
243 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((abs‘𝑎) < 𝑀 ↔ (((abs‘𝑎) + 𝑀) / 2) < 𝑀)) |
245 | 233, 244 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < 𝑀) |
246 | 229 | rpge0d 11876 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 0 ≤ 𝑀) |
247 | 242, 246 | absidd 14161 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) = 𝑀) |
248 | 229 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ∈ ℂ) |
249 | | oveq1 6657 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑀 → (𝑤↑𝑖) = (𝑀↑𝑖)) |
250 | 249 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑀 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) |
251 | 250 | mpteq2dv 4745 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑀 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
252 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑤 → (𝑎↑𝑖) = (𝑤↑𝑖)) |
253 | 252 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑤 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖))) |
254 | 253 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑤 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)))) |
255 | 254 | cbvmptv 4750 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑤 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑤↑𝑖)))) |
256 | | nn0ex 11298 |
. . . . . . . . . . . . . . . 16
⊢
ℕ0 ∈ V |
257 | 256 | mptex 6486 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) ∈ V |
258 | 251, 255,
257 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
259 | 248, 258 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) |
260 | 259 | seqeq3d 12809 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀)) = seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))))) |
261 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝐴‘𝑛) = (𝐴‘𝑖)) |
262 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑖 → (𝑥↑𝑛) = (𝑥↑𝑖)) |
263 | 261, 262 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑖 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑖) · (𝑥↑𝑖))) |
264 | 263 | cbvmptv 4750 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑥↑𝑖))) |
265 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥↑𝑖) = (𝑦↑𝑖)) |
266 | 265 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((𝐴‘𝑖) · (𝑥↑𝑖)) = ((𝐴‘𝑖) · (𝑦↑𝑖))) |
267 | 266 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑥↑𝑖))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
268 | 264, 267 | syl5eq 2668 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
269 | 268 | cbvmptv 4750 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
270 | 6, 269 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑦 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ ((𝐴‘𝑖) · (𝑦↑𝑖)))) |
271 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑠 → (𝐺‘𝑟) = (𝐺‘𝑠)) |
272 | 271 | seqeq3d 12809 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑠 → seq0( + , (𝐺‘𝑟)) = seq0( + , (𝐺‘𝑠))) |
273 | 272 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑠 → (seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ ↔ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ )) |
274 | 273 | cbvrabv 3199 |
. . . . . . . . . . . . . . 15
⊢ {𝑟 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑟)) ∈ dom ⇝ } = {𝑠 ∈ ℝ ∣ seq0( +
, (𝐺‘𝑠)) ∈ dom ⇝
} |
275 | 274 | supeq1i 8353 |
. . . . . . . . . . . . . 14
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , (𝐺‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑠 ∈
ℝ ∣ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ }, ℝ*,
< ) |
276 | 14, 275 | eqtri 2644 |
. . . . . . . . . . . . 13
⊢ 𝑅 = sup({𝑠 ∈ ℝ ∣ seq0( + , (𝐺‘𝑠)) ∈ dom ⇝ }, ℝ*,
< ) |
277 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖))) |
278 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝐴:ℕ0⟶ℂ) |
279 | 228 | simp3d 1075 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 < 𝑅) |
280 | 247, 279 | eqbrtrd 4675 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) < 𝑅) |
281 | 270, 276,
277, 278, 248, 280 | dvradcnv 24175 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑀↑𝑖)))) ∈ dom ⇝ ) |
282 | 260, 281 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑀)) ∈ dom ⇝ ) |
283 | 204, 214,
219, 248, 282 | radcnvle 24174 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (abs‘𝑀) ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
284 | 247, 283 | eqbrtrrd 4677 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 𝑀 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
285 | 19, 230, 232, 245, 284 | xrltletrd 11992 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (((abs‘𝑎) + 𝑀) / 2) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
286 | 204, 208,
214, 219, 226, 227, 285, 45 | pserulm 24176 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘))) |
287 | 22 | sselda 3603 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
288 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑦 → (𝑎↑𝑖) = (𝑦↑𝑖)) |
289 | 288 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑦 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)) = (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) |
290 | 289 | mpteq2dv 4745 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑦 → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
291 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) = (𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖)))) |
292 | 256 | mptex 6486 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) ∈ V |
293 | 290, 291,
292 | fvmpt 6282 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℂ → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
294 | 287, 293 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
295 | 294 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
296 | 295 | fveq1d 6193 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘)) |
297 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
298 | 297 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝐴‘(𝑖 + 1)) = (𝐴‘(𝑘 + 1))) |
299 | 297, 298 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) = ((𝑘 + 1) · (𝐴‘(𝑘 + 1)))) |
300 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑦↑𝑖) = (𝑦↑𝑘)) |
301 | 299, 300 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
302 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))) |
303 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) ∈ V |
304 | 301, 302,
303 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
305 | 304 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
306 | 296, 305 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
307 | 306 | sumeq2dv 14433 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
308 | 307 | mpteq2dva 4744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
309 | 286, 308 | breqtrd 4679 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
310 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
311 | | 1e0p1 11552 |
. . . . . . . . 9
⊢ 1 = (0 +
1) |
312 | 311 | fveq2i 6194 |
. . . . . . . 8
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
313 | 310, 312 | eqtri 2644 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘(0 + 1)) |
314 | | 1zzd 11408 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 1 ∈ ℤ) |
315 | | 0zd 11389 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 0 ∈ ℤ) |
316 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℕ0) |
317 | 316 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ ℕ0
→ (𝑖 + 1) ∈
ℂ) |
318 | 317 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑖 + 1) ∈
ℂ) |
319 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
320 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴:ℕ0⟶ℂ ∧
(𝑖 + 1) ∈
ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ) |
321 | 319, 316,
320 | syl2an 494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝐴‘(𝑖 + 1)) ∈ ℂ) |
322 | 318, 321 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → ((𝑖 + 1) · (𝐴‘(𝑖 + 1))) ∈ ℂ) |
323 | 287, 155 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (𝑦↑𝑖) ∈ ℂ) |
324 | 322, 323 | mulcld 10060 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ℕ0) → (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)) ∈ ℂ) |
325 | 324, 302 | fmptd 6385 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))):ℕ0⟶ℂ) |
326 | 294 | feq1d 6030 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦):ℕ0⟶ℂ ↔
(𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖))):ℕ0⟶ℂ)) |
327 | 325, 326 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦):ℕ0⟶ℂ) |
328 | 327 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑚 ∈ ℕ0) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑚) ∈ ℂ) |
329 | 1, 315, 328 | serf 12829 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) → seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)):ℕ0⟶ℂ) |
330 | 329 | ffvelrnda 6359 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑦 ∈ 𝐵) ∧ 𝑗 ∈ ℕ0) → (seq0( +
, ((𝑎 ∈ ℂ
↦ (𝑖 ∈
ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) ∈ ℂ) |
331 | 330 | an32s 846 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) ∈ ℂ) |
332 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) |
333 | 331, 332 | fmptd 6385 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ) |
334 | 32, 34 | elmap 7886 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑𝑚
𝐵) ↔ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)):𝐵⟶ℂ) |
335 | 333, 334 | sylibr 224 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑗 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) ∈ (ℂ ↑𝑚
𝐵)) |
336 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) = (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))) |
337 | 335, 336 | fmptd 6385 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗))):ℕ0⟶(ℂ
↑𝑚 𝐵)) |
338 | | elfznn 12370 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ) |
339 | 338 | nnne0d 11065 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ≠ 0) |
340 | 339 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑚) → ¬ 𝑖 = 0) |
341 | 340 | iffalsed 4097 |
. . . . . . . . . . . . . 14
⊢ (𝑖 ∈ (1...𝑚) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = (𝑖 · (𝑦↑(𝑖 − 1)))) |
342 | 341 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ (𝑖 ∈ (1...𝑚) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))) |
343 | 342 | sumeq2i 14429 |
. . . . . . . . . . . 12
⊢
Σ𝑖 ∈
(1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) |
344 | | 1zzd 11408 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 1 ∈ ℤ) |
345 | | nnz 11399 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℤ) |
346 | 345 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑚 ∈ ℤ) |
347 | 278 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝐴:ℕ0⟶ℂ) |
348 | 338 | nnnn0d 11351 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...𝑚) → 𝑖 ∈ ℕ0) |
349 | 347, 348,
149 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝐴‘𝑖) ∈ ℂ) |
350 | 338 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℕ) |
351 | 350 | nncnd 11036 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → 𝑖 ∈ ℂ) |
352 | 287 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℂ) |
353 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ℕ → (𝑖 − 1) ∈
ℕ0) |
354 | 338, 353 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...𝑚) → (𝑖 − 1) ∈
ℕ0) |
355 | | expcl 12878 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℂ ∧ (𝑖 − 1) ∈
ℕ0) → (𝑦↑(𝑖 − 1)) ∈ ℂ) |
356 | 352, 354,
355 | syl2an 494 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑦↑(𝑖 − 1)) ∈ ℂ) |
357 | 351, 356 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → (𝑖 · (𝑦↑(𝑖 − 1))) ∈
ℂ) |
358 | 349, 357 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) ∈
ℂ) |
359 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝐴‘𝑖) = (𝐴‘(𝑘 + 1))) |
360 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑘 + 1) → 𝑖 = (𝑘 + 1)) |
361 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑘 + 1) → (𝑖 − 1) = ((𝑘 + 1) − 1)) |
362 | 361 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑘 + 1) → (𝑦↑(𝑖 − 1)) = (𝑦↑((𝑘 + 1) − 1))) |
363 | 360, 362 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑘 + 1) → (𝑖 · (𝑦↑(𝑖 − 1))) = ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) |
364 | 359, 363 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑘 + 1) → ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
365 | 344, 344,
346, 358, 364 | fsumshftm 14513 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1)))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
366 | 343, 365 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
367 | 311 | oveq1i 6660 |
. . . . . . . . . . . . . 14
⊢
(1...𝑚) = ((0 +
1)...𝑚) |
368 | | fzp1ss 12392 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℤ → ((0 + 1)...𝑚) ⊆ (0...𝑚)) |
369 | 113, 368 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ((0 +
1)...𝑚) ⊆ (0...𝑚) |
370 | 367, 369 | eqsstri 3635 |
. . . . . . . . . . . . 13
⊢
(1...𝑚) ⊆
(0...𝑚) |
371 | 370 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (1...𝑚) ⊆ (0...𝑚)) |
372 | 342 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · (𝑖 · (𝑦↑(𝑖 − 1))))) |
373 | 372, 358 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (1...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
374 | | eldif 3584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) ↔ (𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚))) |
375 | | elfzuz2 12346 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 ∈ (0...𝑚) → 𝑚 ∈
(ℤ≥‘0)) |
376 | | elfzp12 12419 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈
(ℤ≥‘0) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))) |
377 | 375, 376 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 ∈ (0...𝑚) → (𝑖 ∈ (0...𝑚) ↔ (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚)))) |
378 | 377 | ibi 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0...𝑚) → (𝑖 = 0 ∨ 𝑖 ∈ ((0 + 1)...𝑚))) |
379 | 378 | ord 392 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (0...𝑚) → (¬ 𝑖 = 0 → 𝑖 ∈ ((0 + 1)...𝑚))) |
380 | 379 | con1d 139 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (0...𝑚) → (¬ 𝑖 ∈ ((0 + 1)...𝑚) → 𝑖 = 0)) |
381 | 380 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑖 ∈ (0...𝑚) ∧ ¬ 𝑖 ∈ ((0 + 1)...𝑚)) → 𝑖 = 0) |
382 | 374, 381 | sylbi 207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ ((0...𝑚) ∖ ((0 + 1)...𝑚)) → 𝑖 = 0) |
383 | 367 | difeq2i 3725 |
. . . . . . . . . . . . . . . . 17
⊢
((0...𝑚) ∖
(1...𝑚)) = ((0...𝑚) ∖ ((0 + 1)...𝑚)) |
384 | 382, 383 | eleq2s 2719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 = 0) |
385 | 384 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → 𝑖 = 0) |
386 | 385 | iftrued 4094 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))) = 0) |
387 | 386 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = ((𝐴‘𝑖) · 0)) |
388 | | eldifi 3732 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ (0...𝑚)) |
389 | 388, 107 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ((0...𝑚) ∖ (1...𝑚)) → 𝑖 ∈ ℕ0) |
390 | 347, 389,
149 | syl2an 494 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → (𝐴‘𝑖) ∈ ℂ) |
391 | 390 | mul01d 10235 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · 0) = 0) |
392 | 387, 391 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ ((0...𝑚) ∖ (1...𝑚))) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = 0) |
393 | | fzfid 12772 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (0...𝑚) ∈ Fin) |
394 | 371, 373,
392, 393 | fsumss 14456 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (1...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
395 | | 1m1e0 11089 |
. . . . . . . . . . . . . 14
⊢ (1
− 1) = 0 |
396 | 395 | oveq1i 6660 |
. . . . . . . . . . . . 13
⊢ ((1
− 1)...(𝑚 − 1))
= (0...(𝑚 −
1)) |
397 | 396 | sumeq1i 14428 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈ ((1
− 1)...(𝑚 −
1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) |
398 | | elfznn0 12433 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (0...(𝑚 − 1)) → 𝑘 ∈ ℕ0) |
399 | 398 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℕ0) |
400 | 399, 304 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
401 | 352 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑦 ∈ ℂ) |
402 | 401, 293 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦) = (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))) |
403 | 402 | fveq1d 6193 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑦↑𝑖)))‘𝑘)) |
404 | 347 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝐴:ℕ0⟶ℂ) |
405 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) |
406 | 399, 405 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈
ℕ0) |
407 | 404, 406 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝐴‘(𝑘 + 1)) ∈ ℂ) |
408 | 406 | nn0cnd 11353 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑘 + 1) ∈ ℂ) |
409 | | expcl 12878 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑦↑𝑘) ∈
ℂ) |
410 | 352, 398,
409 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑𝑘) ∈ ℂ) |
411 | 407, 408,
410 | mul12d 10245 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑𝑘))) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦↑𝑘)))) |
412 | 399 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → 𝑘 ∈ ℂ) |
413 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
414 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 + 1)
− 1) = 𝑘) |
415 | 412, 413,
414 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) − 1) = 𝑘) |
416 | 415 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) = (𝑦↑𝑘)) |
417 | 416 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) = ((𝑘 + 1) · (𝑦↑𝑘))) |
418 | 417 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑𝑘)))) |
419 | 408, 407,
410 | mulassd 10063 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)) = ((𝑘 + 1) · ((𝐴‘(𝑘 + 1)) · (𝑦↑𝑘)))) |
420 | 411, 418,
419 | 3eqtr4d 2666 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) |
421 | 400, 403,
420 | 3eqtr4d 2666 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦)‘𝑘) = ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))))) |
422 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ → (𝑚 − 1) ∈
ℕ0) |
423 | 422 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑚 − 1) ∈
ℕ0) |
424 | 423 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑚 − 1) ∈
ℕ0) |
425 | 424, 1 | syl6eleq 2711 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → (𝑚 − 1) ∈
(ℤ≥‘0)) |
426 | 416, 410 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → (𝑦↑((𝑘 + 1) − 1)) ∈
ℂ) |
427 | 408, 426 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1))) ∈
ℂ) |
428 | 407, 427 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) ∧ 𝑘 ∈ (0...(𝑚 − 1))) → ((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) ∈
ℂ) |
429 | 421, 425,
428 | fsumser 14461 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ (0...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
430 | 397, 429 | syl5eq 2668 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑘 ∈ ((1 − 1)...(𝑚 − 1))((𝐴‘(𝑘 + 1)) · ((𝑘 + 1) · (𝑦↑((𝑘 + 1) − 1)))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
431 | 366, 394,
430 | 3eqtr3d 2664 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
432 | 431 | mpteq2dva 4744 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
433 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑗 = (𝑚 − 1) → (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0
↦ (((𝑖 + 1) ·
(𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗) = (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) |
434 | 433 | mpteq2dv 4745 |
. . . . . . . . . . 11
⊢ (𝑗 = (𝑚 − 1) → (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
435 | 34 | mptex 6486 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1))) ∈ V |
436 | 434, 336,
435 | fvmpt 6282 |
. . . . . . . . . 10
⊢ ((𝑚 − 1) ∈
ℕ0 → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
437 | 423, 436 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)) = (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘(𝑚 − 1)))) |
438 | 432, 437 | eqtr4d 2659 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1))) |
439 | 438 | mpteq2dva 4744 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ ↦ ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))‘(𝑚 − 1)))) |
440 | 1, 313, 4, 314, 337, 439 | ulmshft 24144 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑗 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ (seq0( + , ((𝑎 ∈ ℂ ↦ (𝑖 ∈ ℕ0 ↦ (((𝑖 + 1) · (𝐴‘(𝑖 + 1))) · (𝑎↑𝑖))))‘𝑦))‘𝑗)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) ↔ (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))) |
441 | 309, 440 | mpbid 222 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
442 | 184, 441 | syl5eqbr 4688 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾
ℕ)(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
443 | | 1nn0 11308 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
444 | 443 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → 1 ∈
ℕ0) |
445 | | fzfid 12772 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → (0...𝑚) ∈ Fin) |
446 | 171 | an32s 846 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) ∧ 𝑖 ∈ (0...𝑚)) → ((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
447 | 445, 446 | fsumcl 14464 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) ∧ 𝑦 ∈ 𝐵) → Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))) ∈
ℂ) |
448 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) = (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) |
449 | 447, 448 | fmptd 6385 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ) |
450 | 32, 34 | elmap 7886 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ
↑𝑚 𝐵) ↔ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))):𝐵⟶ℂ) |
451 | 449, 450 | sylibr 224 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝑆) ∧ 𝑚 ∈ ℕ0) → (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1)))))) ∈ (ℂ
↑𝑚 𝐵)) |
452 | | eqid 2622 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) = (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) |
453 | 451, 452 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1))))))):ℕ0⟶(ℂ ↑𝑚 𝐵)) |
454 | 1, 310, 444, 453 | ulmres 24142 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))) ↔ ((𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 − 1))))))) ↾
ℕ)(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘))))) |
455 | 442, 454 | mpbird 247 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑚)((𝐴‘𝑖) · if(𝑖 = 0, 0, (𝑖 · (𝑦↑(𝑖 −
1)))))))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
456 | 181, 455 | eqbrtrd 4675 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (𝑚 ∈ ℕ0 ↦ (ℂ
D ((𝑘 ∈
ℕ0 ↦ (𝑦 ∈ 𝐵 ↦ Σ𝑖 ∈ (0...𝑘)((𝐺‘𝑦)‘𝑖)))‘𝑚)))(⇝𝑢‘𝐵)(𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |
457 | 1, 3, 4, 38, 48, 123, 456 | ulmdv 24157 |
1
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑆) → (ℂ D (𝐹 ↾ 𝐵)) = (𝑦 ∈ 𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦↑𝑘)))) |