Theorem plymullem1 14984

Description: Derive the coefficient function for the product of two polynomials. (Contributed by Mario Carneiro, 23-Jul-2014.)

Hypotheses

Ref	Expression
plyaddlem.1	⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆))
plyaddlem.2	⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆))
plyaddlem.m	⊢ (𝜑 → 𝑀 ∈ ℕ0)
plyaddlem.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
plyaddlem.a	⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
plyaddlem.b	⊢ (𝜑 → 𝐵:ℕ0⟶ℂ)
plyaddlem.a2	⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})
plyaddlem.b2	⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})
plyaddlem.f	⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))
plyaddlem.g	⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))

Assertion

Ref	Expression
plymullem1	⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))))

Distinct variable groups:   𝐴,𝑛   𝑘,𝑛,𝐵   𝑘,𝑀,𝑛   𝑘,𝑁,𝑛   𝑧,𝑘,𝜑,𝑛

Allowed substitution hints:   𝐴(𝑧,𝑘)   𝐵(𝑧)   𝑆(𝑧,𝑘,𝑛)   𝐹(𝑧,𝑘,𝑛)   𝐺(𝑧,𝑘,𝑛)   𝑀(𝑧)   𝑁(𝑧)

Proof of Theorem plymullem1

Dummy variables 𝑚 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnex 8003	. . . 4 ⊢ ℂ ∈ V
2	1	a1i 9	. . 3 ⊢ (𝜑 → ℂ ∈ V)
3		0zd 9338	. . . . . 6 ⊢ (𝜑 → 0 ∈ ℤ)
4		plyaddlem.m	. . . . . . 7 ⊢ (𝜑 → 𝑀 ∈ ℕ0)
5	4	nn0zd 9446	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ ℤ)
6	3, 5	fzfigd 10523	. . . . 5 ⊢ (𝜑 → (0...𝑀) ∈ Fin)
7	6	adantr 276	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ∈ Fin)
8		plyaddlem.a	. . . . . . 7 ⊢ (𝜑 → 𝐴:ℕ0⟶ℂ)
9	8	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝐴:ℕ0⟶ℂ)
10		elfznn0 10189	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑀) → 𝑘 ∈ ℕ0)
11	10	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℕ0)
12	9, 11	ffvelcdmd 5698	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝐴‘𝑘) ∈ ℂ)
13		simplr 528	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑧 ∈ ℂ)
14	13, 11	expcld 10765	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝑧↑𝑘) ∈ ℂ)
15	12, 14	mulcld 8047	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
16	7, 15	fsumcl 11565	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
17		plyaddlem.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
18	17	nn0zd 9446	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℤ)
19	3, 18	fzfigd 10523	. . . . 5 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
20	19	adantr 276	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin)
21		plyaddlem.b	. . . . . . 7 ⊢ (𝜑 → 𝐵:ℕ0⟶ℂ)
22	21	ad2antrr 488	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝐵:ℕ0⟶ℂ)
23		elfznn0 10189	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0)
24	23	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0)
25	22, 24	ffvelcdmd 5698	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐵‘𝑘) ∈ ℂ)
26		simplr 528	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑧 ∈ ℂ)
27	26, 24	expcld 10765	. . . . 5 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → (𝑧↑𝑘) ∈ ℂ)
28	25, 27	mulcld 8047	. . . 4 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
29	20, 28	fsumcl 11565	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
30		plyaddlem.f	. . 3 ⊢ (𝜑 → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘))))
31		plyaddlem.g	. . 3 ⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))
32	2, 16, 29, 30, 31	offval2 6151	. 2 ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))))
33		fveq2 5558	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝐵‘𝑚) = (𝐵‘𝑛))
34		oveq2 5930	. . . . . . . 8 ⊢ (𝑚 = 𝑛 → (𝑧↑𝑚) = (𝑧↑𝑛))
35	33, 34	oveq12d 5940	. . . . . . 7 ⊢ (𝑚 = 𝑛 → ((𝐵‘𝑚) · (𝑧↑𝑚)) = ((𝐵‘𝑛) · (𝑧↑𝑛)))
36	35	oveq2d 5938	. . . . . 6 ⊢ (𝑚 = 𝑛 → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑚) · (𝑧↑𝑚))) = (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))))
37		fveq2 5558	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑘) → (𝐵‘𝑚) = (𝐵‘(𝑛 − 𝑘)))
38		oveq2 5930	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑘) → (𝑧↑𝑚) = (𝑧↑(𝑛 − 𝑘)))
39	37, 38	oveq12d 5940	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑘) → ((𝐵‘𝑚) · (𝑧↑𝑚)) = ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘))))
40	39	oveq2d 5938	. . . . . 6 ⊢ (𝑚 = (𝑛 − 𝑘) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑚) · (𝑧↑𝑚))) = (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))))
41		elfznn0 10189	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...(𝑀 + 𝑁)) → 𝑘 ∈ ℕ0)
42	8	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐴:ℕ0⟶ℂ)
43	42	ffvelcdmda 5697	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
44		expcl 10649	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
45	44	adantll 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → (𝑧↑𝑘) ∈ ℂ)
46	43, 45	mulcld 8047	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ℕ0) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
47	41, 46	sylan2 286	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...(𝑀 + 𝑁))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
48		elfznn0 10189	. . . . . . . . 9 ⊢ (𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)) → 𝑛 ∈ ℕ0)
49	21	adantr 276	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝐵:ℕ0⟶ℂ)
50	49	ffvelcdmda 5697	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ ℕ0) → (𝐵‘𝑛) ∈ ℂ)
51		expcl 10649	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑧↑𝑛) ∈ ℂ)
52	51	adantll 476	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ ℕ0) → (𝑧↑𝑛) ∈ ℂ)
53	50, 52	mulcld 8047	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ ℕ0) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)
54	48, 53	sylan2 286	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)
55	47, 54	anim12dan 600	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ ∧ ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ))
56		mulcl 8006	. . . . . . 7 ⊢ ((((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ ∧ ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ)
57	55, 56	syl 14	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ (𝑘 ∈ (0...(𝑀 + 𝑁)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ)
58	5, 18	zaddcld 9452	. . . . . . 7 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ ℤ)
59	58	adantr 276	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑀 + 𝑁) ∈ ℤ)
60	36, 40, 57, 59	fisum0diag2 11612	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑛 ∈ (0...(𝑀 + 𝑁))Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))))
61	4	nn0cnd 9304	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℂ)
62	61	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑀 ∈ ℂ)
63	17	nn0cnd 9304	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℂ)
64	63	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℂ)
65	11	nn0cnd 9304	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℂ)
66	62, 64, 65	addsubd 8358	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) = ((𝑀 − 𝑘) + 𝑁))
67		fznn0sub 10132	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (0...𝑀) → (𝑀 − 𝑘) ∈ ℕ0)
68	67	adantl 277	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝑀 − 𝑘) ∈ ℕ0)
69		nn0uz 9636	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
70	68, 69	eleqtrdi 2289	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝑀 − 𝑘) ∈ (ℤ≥‘0))
71	18	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑁 ∈ ℤ)
72		eluzadd 9630	. . . . . . . . . . . 12 ⊢ (((𝑀 − 𝑘) ∈ (ℤ≥‘0) ∧ 𝑁 ∈ ℤ) → ((𝑀 − 𝑘) + 𝑁) ∈ (ℤ≥‘(0 + 𝑁)))
73	70, 71, 72	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 − 𝑘) + 𝑁) ∈ (ℤ≥‘(0 + 𝑁)))
74	66, 73	eqeltrd 2273	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) ∈ (ℤ≥‘(0 + 𝑁)))
75	64	addlidd 8176	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (0 + 𝑁) = 𝑁)
76	75	fveq2d 5562	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (ℤ≥‘(0 + 𝑁)) = (ℤ≥‘𝑁))
77	74, 76	eleqtrd 2275	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) ∈ (ℤ≥‘𝑁))
78		fzss2 10139	. . . . . . . . 9 ⊢ (((𝑀 + 𝑁) − 𝑘) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...((𝑀 + 𝑁) − 𝑘)))
79	77, 78	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (0...𝑁) ⊆ (0...((𝑀 + 𝑁) − 𝑘)))
80	10, 46	sylan2 286	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
81	80	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...𝑁)) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
82		elfznn0 10189	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (0...𝑁) → 𝑛 ∈ ℕ0)
83	82, 53	sylan2 286	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...𝑁)) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)
84	83	adantlr 477	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...𝑁)) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)
85	81, 84	mulcld 8047	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...𝑁)) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ)
86		eldifn 3286	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁)) → ¬ 𝑛 ∈ (0...𝑁))
87	86	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ¬ 𝑛 ∈ (0...𝑁))
88		eldifi 3285	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁)) → 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘)))
89	88, 48	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁)) → 𝑛 ∈ ℕ0)
90	89	adantl 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → 𝑛 ∈ ℕ0)
91		peano2nn0 9289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)
92	17, 91	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑁 + 1) ∈ ℕ0)
93	92, 69	eleqtrdi 2289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ≥‘0))
94		uzsplit 10167	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘0) → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
95	93, 94	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (ℤ≥‘0) = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
96	69, 95	eqtrid 2241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ℕ0 = ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))))
97		ax-1cn 7972	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℂ
98		pncan 8232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
99	63, 97, 98	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑁 + 1) − 1) = 𝑁)
100	99	oveq2d 5938	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (0...((𝑁 + 1) − 1)) = (0...𝑁))
101	100	uneq1d 3316	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1))) = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
102	96, 101	eqtrd 2229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ℕ0 = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
103	102	ad3antrrr 492	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ℕ0 = ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
104	90, 103	eleqtrd 2275	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → 𝑛 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))))
105		elun 3304	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ((0...𝑁) ∪ (ℤ≥‘(𝑁 + 1))) ↔ (𝑛 ∈ (0...𝑁) ∨ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))))
106	104, 105	sylib 122	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝑛 ∈ (0...𝑁) ∨ 𝑛 ∈ (ℤ≥‘(𝑁 + 1))))
107	106	ord 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (¬ 𝑛 ∈ (0...𝑁) → 𝑛 ∈ (ℤ≥‘(𝑁 + 1))))
108	87, 107	mpd 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → 𝑛 ∈ (ℤ≥‘(𝑁 + 1)))
109	21	ffund 5411	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Fun 𝐵)
110		ssun2 3327	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤ≥‘(𝑁 + 1)) ⊆ ((0...((𝑁 + 1) − 1)) ∪ (ℤ≥‘(𝑁 + 1)))
111	110, 96	sseqtrrid 3234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (ℤ≥‘(𝑁 + 1)) ⊆ ℕ0)
112	21	fdmd 5414	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → dom 𝐵 = ℕ0)
113	111, 112	sseqtrrd 3222	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵)
114		funfvima2 5795	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun 𝐵 ∧ (ℤ≥‘(𝑁 + 1)) ⊆ dom 𝐵) → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑛) ∈ (𝐵 “ (ℤ≥‘(𝑁 + 1)))))
115	109, 113, 114	syl2anc 411	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑛) ∈ (𝐵 “ (ℤ≥‘(𝑁 + 1)))))
116	115	ad3antrrr 492	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝑛 ∈ (ℤ≥‘(𝑁 + 1)) → (𝐵‘𝑛) ∈ (𝐵 “ (ℤ≥‘(𝑁 + 1)))))
117	108, 116	mpd 13	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵‘𝑛) ∈ (𝐵 “ (ℤ≥‘(𝑁 + 1))))
118		plyaddlem.b2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})
119	118	ad3antrrr 492	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵 “ (ℤ≥‘(𝑁 + 1))) = {0})
120	117, 119	eleqtrd 2275	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵‘𝑛) ∈ {0})
121		elsni 3640	. . . . . . . . . . . . 13 ⊢ ((𝐵‘𝑛) ∈ {0} → (𝐵‘𝑛) = 0)
122	120, 121	syl 14	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝐵‘𝑛) = 0)
123	122	oveq1d 5937	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) = (0 · (𝑧↑𝑛)))
124	13, 89, 51	syl2an 289	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (𝑧↑𝑛) ∈ ℂ)
125	124	mul02d 8418	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (0 · (𝑧↑𝑛)) = 0)
126	123, 125	eqtrd 2229	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) = 0)
127	126	oveq2d 5938	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = (((𝐴‘𝑘) · (𝑧↑𝑘)) · 0))
128	80	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
129	128	mul01d 8419	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · 0) = 0)
130	127, 129	eqtrd 2229	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ ((0...((𝑀 + 𝑁) − 𝑘)) ∖ (0...𝑁))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0)
131		elfzelz 10100	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘)) → 𝑗 ∈ ℤ)
132	131	adantl 277	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → 𝑗 ∈ ℤ)
133		0zd 9338	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → 0 ∈ ℤ)
134	71	adantr 276	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → 𝑁 ∈ ℤ)
135		fzdcel 10115	. . . . . . . . . 10 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑗 ∈ (0...𝑁))
136	132, 133, 134, 135	syl3anc 1249	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → DECID 𝑗 ∈ (0...𝑁))
137	136	ralrimiva 2570	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ∀𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))DECID 𝑗 ∈ (0...𝑁))
138		0zd 9338	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 0 ∈ ℤ)
139	59	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (𝑀 + 𝑁) ∈ ℤ)
140	11	nn0zd 9446	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → 𝑘 ∈ ℤ)
141	139, 140	zsubcld 9453	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → ((𝑀 + 𝑁) − 𝑘) ∈ ℤ)
142	138, 141	fzfigd 10523	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin)
143	79, 85, 130, 137, 142	fisumss 11557	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → Σ𝑛 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))))
144	143	sumeq2dv 11533	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))))
145		0zd 9338	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 0 ∈ ℤ)
146	5	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑀 ∈ ℤ)
147	145, 146	fzfigd 10523	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ∈ Fin)
148	18	adantr 276	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → 𝑁 ∈ ℤ)
149	145, 148	fzfigd 10523	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑁) ∈ Fin)
150	147, 149, 80, 83	fsum2mul 11618	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...𝑁)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛))))
151	61, 63	addcomd 8177	. . . . . . . . . 10 ⊢ (𝜑 → (𝑀 + 𝑁) = (𝑁 + 𝑀))
152	17, 69	eleqtrdi 2289	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘0))
153		eluzadd 9630	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ (ℤ≥‘0) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 + 𝑀)))
154	152, 5, 153	syl2anc 411	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 + 𝑀) ∈ (ℤ≥‘(0 + 𝑀)))
155	61	addlidd 8176	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 + 𝑀) = 𝑀)
156	155	fveq2d 5562	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘(0 + 𝑀)) = (ℤ≥‘𝑀))
157	154, 156	eleqtrd 2275	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 + 𝑀) ∈ (ℤ≥‘𝑀))
158	151, 157	eqeltrd 2273	. . . . . . . . 9 ⊢ (𝜑 → (𝑀 + 𝑁) ∈ (ℤ≥‘𝑀))
159		fzss2 10139	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) ∈ (ℤ≥‘𝑀) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁)))
160	158, 159	syl 14	. . . . . . . 8 ⊢ (𝜑 → (0...𝑀) ⊆ (0...(𝑀 + 𝑁)))
161	160	adantr 276	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...𝑀) ⊆ (0...(𝑀 + 𝑁)))
162	80	adantr 276	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) ∈ ℂ)
163	54	adantlr 477	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)
164	162, 163	mulcld 8047	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ)
165	142, 164	fsumcl 11565	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ (0...𝑀)) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) ∈ ℂ)
166		eldifn 3286	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → ¬ 𝑘 ∈ (0...𝑀))
167	166	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ¬ 𝑘 ∈ (0...𝑀))
168		eldifi 3285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ (0...(𝑀 + 𝑁)))
169	168, 41	syl 14	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀)) → 𝑘 ∈ ℕ0)
170	169	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ ℕ0)
171		peano2nn0 9289	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℕ0 → (𝑀 + 1) ∈ ℕ0)
172	4, 171	syl 14	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑀 + 1) ∈ ℕ0)
173	172, 69	eleqtrdi 2289	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑀 + 1) ∈ (ℤ≥‘0))
174		uzsplit 10167	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘0) → (ℤ≥‘0) = ((0...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))))
175	173, 174	syl 14	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (ℤ≥‘0) = ((0...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))))
176	69, 175	eqtrid 2241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ℕ0 = ((0...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))))
177		pncan 8232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 + 1) − 1) = 𝑀)
178	61, 97, 177	sylancl 413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑀 + 1) − 1) = 𝑀)
179	178	oveq2d 5938	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (0...((𝑀 + 1) − 1)) = (0...𝑀))
180	179	uneq1d 3316	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((0...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1))) = ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
181	176, 180	eqtrd 2229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ℕ0 = ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
182	181	ad2antrr 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ℕ0 = ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
183	170, 182	eleqtrd 2275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))))
184		elun 3304	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ((0...𝑀) ∪ (ℤ≥‘(𝑀 + 1))) ↔ (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1))))
185	183, 184	sylib 122	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑘 ∈ (0...𝑀) ∨ 𝑘 ∈ (ℤ≥‘(𝑀 + 1))))
186	185	ord 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (¬ 𝑘 ∈ (0...𝑀) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1))))
187	167, 186	mpd 13	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ (ℤ≥‘(𝑀 + 1)))
188	8	ffund 5411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → Fun 𝐴)
189		ssun2 3327	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℤ≥‘(𝑀 + 1)) ⊆ ((0...((𝑀 + 1) − 1)) ∪ (ℤ≥‘(𝑀 + 1)))
190	189, 176	sseqtrrid 3234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (ℤ≥‘(𝑀 + 1)) ⊆ ℕ0)
191	8	fdmd 5414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → dom 𝐴 = ℕ0)
192	190, 191	sseqtrrd 3222	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴)
193		funfvima2 5795	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐴 ∧ (ℤ≥‘(𝑀 + 1)) ⊆ dom 𝐴) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “ (ℤ≥‘(𝑀 + 1)))))
194	188, 192, 193	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “ (ℤ≥‘(𝑀 + 1)))))
195	194	ad2antrr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑘 ∈ (ℤ≥‘(𝑀 + 1)) → (𝐴‘𝑘) ∈ (𝐴 “ (ℤ≥‘(𝑀 + 1)))))
196	187, 195	mpd 13	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ (𝐴 “ (ℤ≥‘(𝑀 + 1))))
197		plyaddlem.a2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})
198	197	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴 “ (ℤ≥‘(𝑀 + 1))) = {0})
199	196, 198	eleqtrd 2275	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) ∈ {0})
200		elsni 3640	. . . . . . . . . . . . . . 15 ⊢ ((𝐴‘𝑘) ∈ {0} → (𝐴‘𝑘) = 0)
201	199, 200	syl 14	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝐴‘𝑘) = 0)
202	201	oveq1d 5937	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = (0 · (𝑧↑𝑘)))
203	169, 45	sylan2 286	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑧↑𝑘) ∈ ℂ)
204	203	mul02d 8418	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (0 · (𝑧↑𝑘)) = 0)
205	202, 204	eqtrd 2229	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0)
206	205	adantr 276	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐴‘𝑘) · (𝑧↑𝑘)) = 0)
207	206	oveq1d 5937	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = (0 · ((𝐵‘𝑛) · (𝑧↑𝑛))))
208	54	adantlr 477	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → ((𝐵‘𝑛) · (𝑧↑𝑛)) ∈ ℂ)
209	208	mul02d 8418	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (0 · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0)
210	207, 209	eqtrd 2229	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) ∧ 𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0)
211	210	sumeq2dv 11533	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))0)
212		0zd 9338	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 0 ∈ ℤ)
213	59	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (𝑀 + 𝑁) ∈ ℤ)
214	170	nn0zd 9446	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → 𝑘 ∈ ℤ)
215	213, 214	zsubcld 9453	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((𝑀 + 𝑁) − 𝑘) ∈ ℤ)
216	212, 215	fzfigd 10523	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin)
217	216	olcd 735	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → ((0 ∈ ℤ ∧ (0...((𝑀 + 𝑁) − 𝑘)) ⊆ (ℤ≥‘0) ∧ ∀𝑗 ∈ (ℤ≥‘0)DECID 𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))) ∨ (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin))
218		isumz 11554	. . . . . . . . 9 ⊢ (((0 ∈ ℤ ∧ (0...((𝑀 + 𝑁) − 𝑘)) ⊆ (ℤ≥‘0) ∧ ∀𝑗 ∈ (ℤ≥‘0)DECID 𝑗 ∈ (0...((𝑀 + 𝑁) − 𝑘))) ∨ (0...((𝑀 + 𝑁) − 𝑘)) ∈ Fin) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))0 = 0)
219	217, 218	syl 14	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))0 = 0)
220	211, 219	eqtrd 2229	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑘 ∈ ((0...(𝑀 + 𝑁)) ∖ (0...𝑀))) → Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = 0)
221		elfzelz 10100	. . . . . . . . . 10 ⊢ (𝑗 ∈ (0...(𝑀 + 𝑁)) → 𝑗 ∈ ℤ)
222	221	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → 𝑗 ∈ ℤ)
223		0zd 9338	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → 0 ∈ ℤ)
224	146	adantr 276	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → 𝑀 ∈ ℤ)
225		fzdcel 10115	. . . . . . . . 9 ⊢ ((𝑗 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑀 ∈ ℤ) → DECID 𝑗 ∈ (0...𝑀))
226	222, 223, 224, 225	syl3anc 1249	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑀 + 𝑁))) → DECID 𝑗 ∈ (0...𝑀))
227	226	ralrimiva 2570	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → ∀𝑗 ∈ (0...(𝑀 + 𝑁))DECID 𝑗 ∈ (0...𝑀))
228	146, 148	zaddcld 9452	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (𝑀 + 𝑁) ∈ ℤ)
229	145, 228	fzfigd 10523	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (0...(𝑀 + 𝑁)) ∈ Fin)
230	161, 165, 220, 227, 229	fisumss 11557	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...𝑀)Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))))
231	144, 150, 230	3eqtr3d 2237	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛))) = Σ𝑘 ∈ (0...(𝑀 + 𝑁))Σ𝑛 ∈ (0...((𝑀 + 𝑁) − 𝑘))(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘𝑛) · (𝑧↑𝑛))))
232		0zd 9338	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → 0 ∈ ℤ)
233		elfzelz 10100	. . . . . . . . . 10 ⊢ (𝑛 ∈ (0...(𝑀 + 𝑁)) → 𝑛 ∈ ℤ)
234	233	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → 𝑛 ∈ ℤ)
235	232, 234	fzfigd 10523	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (0...𝑛) ∈ Fin)
236		elfznn0 10189	. . . . . . . . 9 ⊢ (𝑛 ∈ (0...(𝑀 + 𝑁)) → 𝑛 ∈ ℕ0)
237	236, 52	sylan2 286	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (𝑧↑𝑛) ∈ ℂ)
238		simpll 527	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → 𝜑)
239		elfznn0 10189	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) → 𝑘 ∈ ℕ0)
240	8	ffvelcdmda 5697	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴‘𝑘) ∈ ℂ)
241	238, 239, 240	syl2an 289	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐴‘𝑘) ∈ ℂ)
242		fznn0sub 10132	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑛) → (𝑛 − 𝑘) ∈ ℕ0)
243	21	ffvelcdmda 5697	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑛 − 𝑘) ∈ ℕ0) → (𝐵‘(𝑛 − 𝑘)) ∈ ℂ)
244	238, 242, 243	syl2an 289	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝐵‘(𝑛 − 𝑘)) ∈ ℂ)
245	241, 244	mulcld 8047	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → ((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) ∈ ℂ)
246	235, 237, 245	fsummulc1 11614	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)))
247		simplr 528	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → 𝑧 ∈ ℂ)
248	247, 239, 44	syl2an 289	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑𝑘) ∈ ℂ)
249		expcl 10649	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℂ ∧ (𝑛 − 𝑘) ∈ ℕ0) → (𝑧↑(𝑛 − 𝑘)) ∈ ℂ)
250	247, 242, 249	syl2an 289	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑(𝑛 − 𝑘)) ∈ ℂ)
251	241, 248, 244, 250	mul4d 8181	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) = (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘)))))
252	247	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑧 ∈ ℂ)
253	242	adantl 277	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑛 − 𝑘) ∈ ℕ0)
254	239	adantl 277	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℕ0)
255	252, 253, 254	expaddd 10767	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑(𝑘 + (𝑛 − 𝑘))) = ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘))))
256	254	nn0cnd 9304	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑘 ∈ ℂ)
257	236	ad2antlr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑛 ∈ ℕ0)
258	257	nn0cnd 9304	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → 𝑛 ∈ ℂ)
259	256, 258	pncan3d 8340	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑘 + (𝑛 − 𝑘)) = 𝑛)
260	259	oveq2d 5938	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (𝑧↑(𝑘 + (𝑛 − 𝑘))) = (𝑧↑𝑛))
261	255, 260	eqtr3d 2231	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘))) = (𝑧↑𝑛))
262	261	oveq2d 5938	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · ((𝑧↑𝑘) · (𝑧↑(𝑛 − 𝑘)))) = (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)))
263	251, 262	eqtrd 2229	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) ∧ 𝑘 ∈ (0...𝑛)) → (((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) = (((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)))
264	263	sumeq2dv 11533	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))) = Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)))
265	246, 264	eqtr4d 2232	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ ℂ) ∧ 𝑛 ∈ (0...(𝑀 + 𝑁))) → (Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))))
266	265	sumeq2dv 11533	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = Σ𝑛 ∈ (0...(𝑀 + 𝑁))Σ𝑘 ∈ (0...𝑛)(((𝐴‘𝑘) · (𝑧↑𝑘)) · ((𝐵‘(𝑛 − 𝑘)) · (𝑧↑(𝑛 − 𝑘)))))
267	60, 231, 266	3eqtr4rd 2240	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛))))
268		fveq2 5558	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
269		oveq2 5930	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝑧↑𝑛) = (𝑧↑𝑘))
270	268, 269	oveq12d 5940	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (𝑧↑𝑛)) = ((𝐵‘𝑘) · (𝑧↑𝑘)))
271	270	cbvsumv 11526	. . . . 5 ⊢ Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛)) = Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))
272	271	oveq2i 5933	. . . 4 ⊢ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑛 ∈ (0...𝑁)((𝐵‘𝑛) · (𝑧↑𝑛))) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))
273	267, 272	eqtrdi 2245	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ ℂ) → Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛)) = (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘))))
274	273	mpteq2dva 4123	. 2 ⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))) = (𝑧 ∈ ℂ ↦ (Σ𝑘 ∈ (0...𝑀)((𝐴‘𝑘) · (𝑧↑𝑘)) · Σ𝑘 ∈ (0...𝑁)((𝐵‘𝑘) · (𝑧↑𝑘)))))
275	32, 274	eqtr4d 2232	1 ⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑧 ∈ ℂ ↦ Σ𝑛 ∈ (0...(𝑀 + 𝑁))(Σ𝑘 ∈ (0...𝑛)((𝐴‘𝑘) · (𝐵‘(𝑛 − 𝑘))) · (𝑧↑𝑛))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 709  DECID wdc 835   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  ∀wral 2475  Vcvv 2763   ∖ cdif 3154   ∪ cun 3155   ⊆ wss 3157  {csn 3622   ↦ cmpt 4094  dom cdm 4663   “ cima 4666  Fun wfun 5252  ⟶wf 5254  ‘cfv 5258  (class class class)co 5922   ∘_𝑓 cof 6133  Fincfn 6799  ℂcc 7877  0cc0 7879  1c1 7880   + caddc 7882   · cmul 7884   − cmin 8197  ℕ₀cn0 9249  ℤcz 9326  ℤ_≥cuz 9601  ...cfz 10083  ↑cexp 10630  Σcsu 11518  Polycply 14964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-mulrcl 7978  ax-addcom 7979  ax-mulcom 7980  ax-addass 7981  ax-mulass 7982  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-1rid 7986  ax-0id 7987  ax-rnegex 7988  ax-precex 7989  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-apti 7994  ax-pre-ltadd 7995  ax-pre-mulgt0 7996  ax-pre-mulext 7997  ax-arch 7998  ax-caucvg 7999

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rmo 2483  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-disj 4011  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-po 4331  df-iso 4332  df-iord 4401  df-on 4403  df-ilim 4404  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-isom 5267  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-of 6135  df-1st 6198  df-2nd 6199  df-recs 6363  df-irdg 6428  df-frec 6449  df-1o 6474  df-oadd 6478  df-er 6592  df-en 6800  df-dom 6801  df-fin 6802  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-reap 8602  df-ap 8609  df-div 8700  df-inn 8991  df-2 9049  df-3 9050  df-4 9051  df-n0 9250  df-z 9327  df-uz 9602  df-q 9694  df-rp 9729  df-fz 10084  df-fzo 10218  df-seqfrec 10540  df-exp 10631  df-ihash 10868  df-cj 11007  df-re 11008  df-im 11009  df-rsqrt 11163  df-abs 11164  df-clim 11444  df-sumdc 11519

This theorem is referenced by:  plymullem  14986