Theorem plyaddlem1

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

	Ref	Expression
Hypotheses	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	plyaddlem1	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		plyaddlem.1	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
2		plyaddlem.2	⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
3		plyaddlem.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4		plyaddlem.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		plyaddlem.a	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
6		plyaddlem.b	⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ )
7		plyaddlem.a2	⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
8		plyaddlem.b2	⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
9		plyaddlem.f	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
10		plyaddlem.g	⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
11		cnex	⊢ ℂ ∈ V
12	11	a1i	⊢ ( 𝜑 → ℂ ∈ V )
13		sumex	⊢ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V )
15		sumex	⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ V )
17	12 14 16 9 10	offval2	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
18		fzfid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∈ Fin )
19		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) → 𝑘 ∈ ℕ0 )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
21	20	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
22		expcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
23	22	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
24	21 23	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
25	19 24	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
26	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐵 : ℕ0 ⟶ ℂ )
27	26	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) ∈ ℂ )
28	27 23	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
29	19 28	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
30	18 25 29	fsumadd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
31	5	ffnd	⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
32	6	ffnd	⊢ ( 𝜑 → 𝐵 Fn ℕ0 )
33		nn0ex	⊢ ℕ0 ∈ V
34	33	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
35		inidm	⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
36		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
37		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐵 ‘ 𝑘 ) = ( 𝐵 ‘ 𝑘 ) )
38	31 32 34 34 35 36 37	ofval	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) )
39	38	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) )
40	39	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) )
41	21 27 23	adddird	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ‘ 𝑘 ) + ( 𝐵 ‘ 𝑘 ) ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
42	40 41	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
43	19 42	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ) → ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
44	43	sumeq2dv	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
45	3	nn0zd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
46	4 3	ifcld	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℕ0 )
47	46	nn0zd	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ )
48	3	nn0red	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
49	4	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
50		max1	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
51	48 49 50	syl2anc	⊢ ( 𝜑 → 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
52		eluz2	⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) ↔ ( 𝑀 ∈ ℤ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ 𝑀 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
53	45 47 51 52	syl3anbrc	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
54		fzss2	⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
55	53 54	syl	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
57		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 )
58	57 24	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
59		eldifn	⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
60	59	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑀 ) )
61		eldifi	⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
62	61 19	syl	⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) → 𝑘 ∈ ℕ0 )
63	62	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ℕ0 )
64		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
65		peano2nn0	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
66	3 65	syl	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ℕ0 )
67	66 64	eleqtrdi	⊢ ( 𝜑 → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
68		uzsplit	⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
69	67 68	syl	⊢ ( 𝜑 → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
70	64 69	eqtrid	⊢ ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
71	3	nn0cnd	⊢ ( 𝜑 → 𝑀 ∈ ℂ )
72		ax-1cn	⊢ 1 ∈ ℂ
73		pncan	⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
74	71 72 73	sylancl	⊢ ( 𝜑 → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
75	74	oveq2d	⊢ ( 𝜑 → ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) = ( 0 ... 𝑀 ) )
76	75	uneq1d	⊢ ( 𝜑 → ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
77	70 76	eqtrd	⊢ ( 𝜑 → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
78	77	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ℕ0 = ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
79	63 78	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
80		elun	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
81	79 80	sylib	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑀 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
82	81	ord	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
83	60 82	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
84	5	ffund	⊢ ( 𝜑 → Fun 𝐴 )
85		ssun2	⊢ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑀 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
86	85 70	sseqtrrid	⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ ℕ0 )
87	5	fdmd	⊢ ( 𝜑 → dom 𝐴 = ℕ0 )
88	86 87	sseqtrrd	⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 )
89		funfvima2	⊢ ( ( Fun 𝐴 ∧ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ⊆ dom 𝐴 ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
90	84 88 89	syl2anc	⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
91	90	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ) )
92	83 91	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
93	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
94	92 93	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ { 0 } )
95		elsni	⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ { 0 } → ( 𝐴 ‘ 𝑘 ) = 0 )
96	94 95	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
97	96	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
98	62 23	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
99	98	mul02d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
100	97 99	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑀 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
101	56 58 100 18	fsumss	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
102	4	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
103		max2	⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
104	48 49 103	syl2anc	⊢ ( 𝜑 → 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) )
105		eluz2	⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ℤ ∧ 𝑁 ≤ if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
106	102 47 104 105	syl3anbrc	⊢ ( 𝜑 → if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) )
107		fzss2	⊢ ( if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
108	106 107	syl	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
110		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
111	110 28	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
112		eldifn	⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
113	112	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
114		eldifi	⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) )
115	114 19	syl	⊢ ( 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
116	115	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ℕ0 )
117		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
118	4 117	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
119	118 64	eleqtrdi	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
120		uzsplit	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ 0 ) → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
121	119 120	syl	⊢ ( 𝜑 → ( ℤ≥ ‘ 0 ) = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
122	64 121	eqtrid	⊢ ( 𝜑 → ℕ0 = ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
123	4	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
124		pncan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
125	123 72 124	sylancl	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
126	125	oveq2d	⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
127	126	uneq1d	⊢ ( 𝜑 → ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
128	122 127	eqtrd	⊢ ( 𝜑 → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
129	128	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ℕ0 = ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
130	116 129	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
131		elun	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑁 ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
132	130 131	sylib	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∨ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
133	132	ord	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
134	113 133	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
135	6	ffund	⊢ ( 𝜑 → Fun 𝐵 )
136		ssun2	⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ( ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ∪ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) )
137	136 122	sseqtrrid	⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ ℕ0 )
138	6	fdmd	⊢ ( 𝜑 → dom 𝐵 = ℕ0 )
139	137 138	sseqtrrd	⊢ ( 𝜑 → ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 )
140		funfvima2	⊢ ( ( Fun 𝐵 ∧ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ⊆ dom 𝐵 ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
141	135 139 140	syl2anc	⊢ ( 𝜑 → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
142	141	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) ) )
143	134 142	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) ∈ ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) )
144	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
145	143 144	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) ∈ { 0 } )
146		elsni	⊢ ( ( 𝐵 ‘ 𝑘 ) ∈ { 0 } → ( 𝐵 ‘ 𝑘 ) = 0 )
147	145 146	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐵 ‘ 𝑘 ) = 0 )
148	147	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
149	115 23	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
150	149	mul02d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
151	148 150	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
152	109 111 151 18	fsumss	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
153	101 152	oveq12d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
154	30 44 153	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
155	154	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ ( Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) + Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
156	17 155	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... if ( 𝑀 ≤ 𝑁 , 𝑁 , 𝑀 ) ) ( ( ( 𝐴 ∘f + 𝐵 ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )