Step | Hyp | Ref
| Expression |
1 | | cnex 10017 |
. . . 4
⊢ ℂ
∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ℂ ∈
V) |
3 | | sumex 14418 |
. . . 4
⊢
Σ𝑘 ∈
(0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V |
4 | 3 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ V) |
5 | | sumex 14418 |
. . . 4
⊢
Σ𝑘 ∈
(0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ V) |
7 | | plyaddlem.f |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)))) |
8 | | plyaddlem.g |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
9 | 2, 4, 6, 7, 8 | offval2 6914 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))) |
10 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝐵‘𝑚) = (𝐵‘𝑛)) |
11 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑧↑𝑚) = (𝑧↑𝑛)) |
12 | 10, 11 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((𝐵‘𝑚) · (𝑧↑𝑚)) = ((𝐵‘𝑛) · (𝑧↑𝑛))) |
13 | 12 | oveq2d 6666 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑚) · (𝑧↑𝑚))) = (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛)))) |
14 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 − 𝑘) → (𝐵‘𝑚) = (𝐵‘(𝑛 − 𝑘))) |
15 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑚 = (𝑛 − 𝑘) → (𝑧↑𝑚) = (𝑧↑(𝑛 − 𝑘))) |
16 | 14, 15 | oveq12d 6668 |
. . . . . . 7
⊢ (𝑚 = (𝑛 − 𝑘) → ((𝐵‘𝑚) · (𝑧↑𝑚)) = ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) |
17 | 16 | oveq2d 6666 |
. . . . . 6
⊢ (𝑚 = (𝑛 − 𝑘) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑚) · (𝑧↑𝑚))) = (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘))))) |
18 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝑘 ∈ (0...(𝑀 + 𝑁)) → 𝑘 ∈ ℕ0) |
19 | | plyaddlem.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
20 | 19 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ) |
21 | 20 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
22 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝑧↑𝑘) ∈
ℂ) |
23 | 22 | adantll 750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ) |
24 | 21, 23 | mulcld 10060 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
25 | 18, 24 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
26 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)) → 𝑛 ∈ ℕ0) |
27 | | plyaddlem.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵:ℕ0⟶ℂ) |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ) |
29 | 28 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ ℕ0) → (𝐵‘𝑛) ∈ ℂ) |
30 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ 𝑛 ∈ ℕ0)
→ (𝑧↑𝑛) ∈
ℂ) |
31 | 30 | adantll 750 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ ℕ0) → (𝑧↑𝑛) ∈ ℂ) |
32 | 29, 31 | mulcld 10060 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ ℕ0) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) |
33 | 26, 32 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) |
34 | 25, 33 | anim12dan 882 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ ∧ ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)) |
35 | | mulcl 10020 |
. . . . . . 7
⊢ ((((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ ∧ ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ) |
37 | 13, 17, 36 | fsum0diag2 14515 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑛 ∈ (0...(𝑀 + 𝑁))Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘))))) |
38 | | plyaddlem.m |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
39 | 38 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑀 ∈ ℂ) |
40 | 39 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℂ) |
41 | | plyaddlem.n |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
42 | 41 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℂ) |
43 | 42 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℂ) |
44 | | elfznn0 12433 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0) |
45 | 44 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0) |
46 | 45 | nn0cnd 11353 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ) |
47 | 40, 43, 46 | addsubd 10413 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) = ((𝑀 − 𝑘) + 𝑁)) |
48 | | fznn0sub 12373 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (0...𝑀) → (𝑀 − 𝑘) ∈
ℕ0) |
49 | 48 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝑀 − 𝑘) ∈
ℕ0) |
50 | | nn0uz 11722 |
. . . . . . . . . . . . 13
⊢
ℕ0 = (ℤ≥‘0) |
51 | 49, 50 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝑀 − 𝑘) ∈
(ℤ≥‘0)) |
52 | 41 | nn0zd 11480 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℤ) |
53 | 52 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ) |
54 | | eluzadd 11716 |
. . . . . . . . . . . 12
⊢ (((𝑀 − 𝑘) ∈ (ℤ≥‘0)
∧ 𝑁 ∈ ℤ)
→ ((𝑀 − 𝑘) + 𝑁) ∈ (ℤ≥‘(0 +
𝑁))) |
55 | 51, 53, 54 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 − 𝑘) + 𝑁) ∈ (ℤ≥‘(0 +
𝑁))) |
56 | 47, 55 | eqeltrd 2701 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) ∈ (ℤ≥‘(0 +
𝑁))) |
57 | 43 | addid2d 10237 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (0 + 𝑁) = 𝑁) |
58 | 57 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (ℤ≥‘(0 +
𝑁)) =
(ℤ≥‘𝑁)) |
59 | 56, 58 | eleqtrd 2703 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) ∈ (ℤ≥‘𝑁)) |
60 | | fzss2 12381 |
. . . . . . . . 9
⊢ (((𝑀 + 𝑁) − 𝑘) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...((𝑀 + 𝑁) − 𝑘))) |
61 | 59, 60 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (0...𝑁) ⊆ (0...((𝑀 + 𝑁) − 𝑘))) |
62 | 44, 24 | sylan2 491 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
63 | 62 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
64 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ∈ ℕ0) |
65 | 64, 32 | sylan2 491 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...𝑁)) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) |
66 | 65 | adantlr 751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...𝑁)) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) |
67 | 63, 66 | mulcld 10060 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ) |
68 | | eldifn 3733 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁)) → ¬ 𝑛 ∈ (0...𝑁)) |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ¬ 𝑛 ∈ (0...𝑁)) |
70 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁)) → 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) |
71 | 70, 26 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁)) → 𝑛 ∈ ℕ0) |
72 | 71 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → 𝑛 ∈ ℕ0) |
73 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
74 | 41, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) |
75 | 74, 50 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) |
76 | | uzsplit 12412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1)))) |
78 | 50, 77 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ℕ0 =
((0...((𝑁 + 1) − 1))
∪ (ℤ≥‘(𝑁 + 1)))) |
79 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℂ |
80 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑁 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑁 + 1)
− 1) = 𝑁) |
81 | 42, 79, 80 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁) |
82 | 81 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁)) |
83 | 82 | uneq1d 3766 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
84 | 78, 83 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ℕ0 =
((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
85 | 84 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ℕ0 = ((0...𝑁) ∪
(ℤ≥‘(𝑁 + 1)))) |
86 | 72, 85 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → 𝑛 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1)))) |
87 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) ↔ (𝑛 ∈ (0...𝑁) ∨ 𝑛 ∈ (ℤ≥‘(𝑁 + 1)))) |
88 | 86, 87 | sylib 208 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝑛 ∈ (0...𝑁) ∨ 𝑛 ∈ (ℤ≥‘(𝑁 + 1)))) |
89 | 88 | ord 392 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (¬ 𝑛 ∈ (0...𝑁) → 𝑛 ∈ (ℤ≥‘(𝑁 + 1)))) |
90 | 69, 89 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → 𝑛 ∈ (ℤ≥‘(𝑁 + 1))) |
91 | | ffun 6048 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵:ℕ0⟶ℂ →
Fun 𝐵) |
92 | 27, 91 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Fun 𝐵) |
93 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℤ≥‘(𝑁 + 1)) ⊆ ((0...((𝑁 + 1) − 1)) ∪
(ℤ≥‘(𝑁 + 1))) |
94 | 93, 78 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆
ℕ0) |
95 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵:ℕ0⟶ℂ →
dom 𝐵 =
ℕ0) |
96 | 27, 95 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom 𝐵 = ℕ0) |
97 | 94, 96 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) |
98 | | funfvima2 6493 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐵 ∧
(ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑛) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
99 | 92, 97, 98 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑛) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
100 | 99 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑛) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1))))) |
101 | 90, 100 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵‘𝑛) ∈ (𝐵 “
(ℤ≥‘(𝑁 + 1)))) |
102 | | plyaddlem.b2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
103 | 102 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵 “
(ℤ≥‘(𝑁 + 1))) = {0}) |
104 | 101, 103 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵‘𝑛) ∈ {0}) |
105 | | elsni 4194 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘𝑛) ∈ {0} → (𝐵‘𝑛) = 0) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵‘𝑛) = 0) |
107 | 106 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) = (0 · (𝑧↑𝑛))) |
108 | | simplr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑧 ∈ ℂ) |
109 | 108, 71, 30 | syl2an 494 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝑧↑𝑛) ∈ ℂ) |
110 | 109 | mul02d 10234 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (0 · (𝑧↑𝑛)) = 0) |
111 | 107, 110 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) = 0) |
112 | 111 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = (((𝐴‘𝑘) · (𝑧↑𝑘)) · 0)) |
113 | 62 | adantr 481 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
114 | 113 | mul01d 10235 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · 0) = 0) |
115 | 112, 114 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0) |
116 | | fzfid 12772 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin) |
117 | 61, 67, 115, 116 | fsumss 14456 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → Σ𝑛 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛)))) |
118 | 117 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛)))) |
119 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ∈ Fin) |
120 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin) |
121 | 119, 120,
62, 65 | fsum2mul 14521 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛)))) |
122 | 39, 42 | addcomd 10238 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑀 + 𝑁) = (𝑁 + 𝑀)) |
123 | 41, 50 | syl6eleq 2711 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
124 | 38 | nn0zd 11480 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
125 | | eluzadd 11716 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘0) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 +
𝑀))) |
126 | 123, 124,
125 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 +
𝑀))) |
127 | 39 | addid2d 10237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + 𝑀) = 𝑀) |
128 | 127 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (𝜑 →
(ℤ≥‘(0 + 𝑀)) = (ℤ≥‘𝑀)) |
129 | 126, 128 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 + 𝑀) ∈ (ℤ≥‘𝑀)) |
130 | 122, 129 | eqeltrd 2701 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘𝑀)) |
131 | | fzss2 12381 |
. . . . . . . . 9
⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑀) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) |
132 | 130, 131 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) |
133 | 132 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁))) |
134 | 62 | adantr 481 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ) |
135 | 33 | adantlr 751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) |
136 | 134, 135 | mulcld 10060 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ) |
137 | 116, 136 | fsumcl 14464 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ) |
138 | | eldifn 3733 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → ¬ 𝑘 ∈ (0...𝑀)) |
139 | 138 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ¬ 𝑘 ∈ (0...𝑀)) |
140 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ (0...(𝑀 + 𝑁))) |
141 | 140, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ ℕ0) |
142 | 141 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ ℕ0) |
143 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑀 ∈ ℕ0
→ (𝑀 + 1) ∈
ℕ0) |
144 | 38, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑀 + 1) ∈
ℕ0) |
145 | 144, 50 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝑀 + 1) ∈
(ℤ≥‘0)) |
146 | | uzsplit 12412 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑀 + 1) ∈
(ℤ≥‘0) → (ℤ≥‘0) =
((0...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 →
(ℤ≥‘0) = ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1)))) |
148 | 50, 147 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ℕ0 =
((0...((𝑀 + 1) − 1))
∪ (ℤ≥‘(𝑀 + 1)))) |
149 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑀 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑀 + 1)
− 1) = 𝑀) |
150 | 39, 79, 149 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀) |
151 | 150 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (0...((𝑀 + 1) − 1)) = (0...𝑀)) |
152 | 151 | uneq1d 3766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) = ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
153 | 148, 152 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ℕ0 =
((0...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
154 | 153 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ℕ0 = ((0...𝑀) ∪
(ℤ≥‘(𝑀 + 1)))) |
155 | 142, 154 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1)))) |
156 | | elun 3753 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) ↔ (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
157 | 155, 156 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
158 | 157 | ord 392 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (¬ 𝑘 ∈ (0...𝑀) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))) |
159 | 139, 158 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1))) |
160 | | ffun 6048 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐴:ℕ0⟶ℂ →
Fun 𝐴) |
161 | 19, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Fun 𝐴) |
162 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(ℤ≥‘(𝑀 + 1)) ⊆ ((0...((𝑀 + 1) − 1)) ∪
(ℤ≥‘(𝑀 + 1))) |
163 | 162, 148 | syl5sseqr 3654 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆
ℕ0) |
164 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴:ℕ0⟶ℂ →
dom 𝐴 =
ℕ0) |
165 | 19, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → dom 𝐴 = ℕ0) |
166 | 163, 165 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) |
167 | | funfvima2 6493 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐴 ∧
(ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
168 | 161, 166,
167 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
169 | 168 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1))))) |
170 | 159, 169 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ (𝐴 “
(ℤ≥‘(𝑀 + 1)))) |
171 | | plyaddlem.a2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
172 | 171 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴 “
(ℤ≥‘(𝑀 + 1))) = {0}) |
173 | 170, 172 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ {0}) |
174 | | elsni 4194 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘𝑘) ∈ {0} → (𝐴‘𝑘) = 0) |
175 | 173, 174 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) = 0) |
176 | 175 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘))) |
177 | 141, 23 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑧↑𝑘) ∈ ℂ) |
178 | 177 | mul02d 10234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (0 · (𝑧↑𝑘)) = 0) |
179 | 176, 178 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0) |
180 | 179 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0) |
181 | 180 | oveq1d 6665 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = (0 · ((𝐵‘𝑛) · (𝑧↑𝑛)))) |
182 | 33 | adantlr 751 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) |
183 | 182 | mul02d 10234 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (0 · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0) |
184 | 181, 183 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0) |
185 | 184 | sumeq2dv 14433 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))0) |
186 | | fzfid 12772 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin) |
187 | 186 | olcd 408 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((0...((𝑀 + 𝑁) − 𝑘)) ⊆ (ℤ≥‘0)
∨ (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin)) |
188 | | sumz 14453 |
. . . . . . . . 9
⊢
(((0...((𝑀 + 𝑁) − 𝑘)) ⊆ (ℤ≥‘0)
∨ (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))0 = 0) |
189 | 187, 188 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))0 = 0) |
190 | 185, 189 | eqtrd 2656 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0) |
191 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...(𝑀 + 𝑁)) ∈ Fin) |
192 | 133, 137,
190, 191 | fsumss 14456 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛)))) |
193 | 118, 121,
192 | 3eqtr3d 2664 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛)))) |
194 | | fzfid 12772 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (0...𝑛) ∈ Fin) |
195 | | elfznn0 12433 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...(𝑀 + 𝑁)) → 𝑛 ∈ ℕ0) |
196 | 195, 31 | sylan2 491 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (𝑧↑𝑛) ∈ ℂ) |
197 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → 𝜑) |
198 | | elfznn0 12433 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0) |
199 | 19 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ) |
200 | 197, 198,
199 | syl2an 494 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐴‘𝑘) ∈ ℂ) |
201 | | fznn0sub 12373 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (0...𝑛) → (𝑛 − 𝑘) ∈
ℕ0) |
202 | 27 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 − 𝑘) ∈ ℕ0) → (𝐵‘(𝑛 − 𝑘)) ∈ ℂ) |
203 | 197, 201,
202 | syl2an 494 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐵‘(𝑛 − 𝑘)) ∈ ℂ) |
204 | 200, 203 | mulcld 10060 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → ((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) ∈ ℂ) |
205 | 194, 196,
204 | fsummulc1 14517 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))) |
206 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → 𝑧 ∈ ℂ) |
207 | 206, 198,
22 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑𝑘) ∈ ℂ) |
208 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℂ ∧ (𝑛 − 𝑘) ∈ ℕ0) → (𝑧↑(𝑛 − 𝑘)) ∈ ℂ) |
209 | 206, 201,
208 | syl2an 494 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑(𝑛 − 𝑘)) ∈ ℂ) |
210 | 200, 207,
203, 209 | mul4d 10248 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) = (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘))))) |
211 | 206 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑧 ∈ ℂ) |
212 | 201 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑛 − 𝑘) ∈
ℕ0) |
213 | 198 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0) |
214 | 211, 212,
213 | expaddd 13010 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑(𝑘 + (𝑛 − 𝑘))) = ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘)))) |
215 | 213 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℂ) |
216 | 195 | ad2antlr 763 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑛 ∈ ℕ0) |
217 | 216 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑛 ∈ ℂ) |
218 | 215, 217 | pncan3d 10395 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘 + (𝑛 − 𝑘)) = 𝑛) |
219 | 218 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑(𝑘 + (𝑛 − 𝑘))) = (𝑧↑𝑛)) |
220 | 214, 219 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘))) = (𝑧↑𝑛)) |
221 | 220 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘)))) = (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))) |
222 | 210, 221 | eqtrd 2656 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) = (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))) |
223 | 222 | sumeq2dv 14433 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) = Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))) |
224 | 205, 223 | eqtr4d 2659 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘))))) |
225 | 224 | sumeq2dv 14433 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = Σ𝑛 ∈ (0...(𝑀 + 𝑁))Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘))))) |
226 | 37, 193, 225 | 3eqtr4rd 2667 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛)))) |
227 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘)) |
228 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (𝑧↑𝑛) = (𝑧↑𝑘)) |
229 | 227, 228 | oveq12d 6668 |
. . . . . 6
⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (𝑧↑𝑛)) = ((𝐵‘𝑘) · (𝑧↑𝑘))) |
230 | 229 | cbvsumv 14426 |
. . . . 5
⊢
Σ𝑛 ∈
(0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛)) = Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) |
231 | 230 | oveq2i 6661 |
. . . 4
⊢
(Σ𝑘 ∈
(0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛))) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))) |
232 | 226, 231 | syl6eq 2672 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))) |
233 | 232 | mpteq2dva 4744 |
. 2
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))) |
234 | 9, 233 | eqtr4d 2659 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)))) |