Theorem coeidlem

Description: Lemma for coeid . (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	dgrub.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
	dgrub.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
	coeid.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
	coeid.4	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	coeid.5	⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
	coeid.6	⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
	coeid.7	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion	coeidlem	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		dgrub.2	⊢ 𝑁 = ( deg ‘ 𝐹 )
3		coeid.3	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
4		coeid.4	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5		coeid.5	⊢ ( 𝜑 → 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
6		coeid.6	⊢ ( 𝜑 → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
7		coeid.7	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
8		plybss	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )
9	3 8	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
10		0cnd	⊢ ( 𝜑 → 0 ∈ ℂ )
11	10	snssd	⊢ ( 𝜑 → { 0 } ⊆ ℂ )
12	9 11	unssd	⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
13		cnex	⊢ ℂ ∈ V
14		ssexg	⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
15	12 13 14	sylancl	⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ∈ V )
16		nn0ex	⊢ ℕ0 ∈ V
17		elmapg	⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
18	15 16 17	sylancl	⊢ ( 𝜑 → ( 𝐵 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
19	5 18	mpbid	⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
20	19 12	fssd	⊢ ( 𝜑 → 𝐵 : ℕ0 ⟶ ℂ )
21	3 4 20 6 7	coeeq	⊢ ( 𝜑 → ( coeff ‘ 𝐹 ) = 𝐵 )
22	1 21	eqtr2id	⊢ ( 𝜑 → 𝐵 = 𝐴 )
23	22	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐵 = 𝐴 )
24		fveq1	⊢ ( 𝐵 = 𝐴 → ( 𝐵 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
25	24	oveq1d	⊢ ( 𝐵 = 𝐴 → ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
26	25	sumeq2sdv	⊢ ( 𝐵 = 𝐴 → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
27	23 26	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
28	3	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
29		dgrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
30	2 29	eqeltrid	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
31	28 30	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
32	31	nn0zd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ∈ ℤ )
33	4	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑀 ∈ ℕ0 )
34	33	nn0zd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑀 ∈ ℤ )
35	23	imaeq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
36	6	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐵 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
37	35 36	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } )
38	1 2	dgrlb	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 “ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) = { 0 } ) → 𝑁 ≤ 𝑀 )
39	28 33 37 38	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑁 ≤ 𝑀 )
40		eluz2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ≤ 𝑀 ) )
41	32 34 39 40	syl3anbrc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
42		fzss2	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... 𝑀 ) )
43	41 42	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑁 ) ⊆ ( 0 ... 𝑀 ) )
44		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
45		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
46	45 3	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
47	1	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
48	46 47	syl	⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝐴 : ℕ0 ⟶ ℂ )
50	49	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
51		expcl	⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
52	51	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
53	50 52	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
54	44 53	sylan2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ∈ ℂ )
55		eldifn	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
56	55	adantl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 𝑁 ) )
57		eldifi	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( 0 ... 𝑀 ) )
58		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ℕ0 )
59	57 58	syl	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
60	1 2	dgrub	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ 𝑁 )
61	60	3expia	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
62	28 59 61	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
63		elfzuz	⊢ ( 𝑘 ∈ ( 0 ... 𝑀 ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
64	57 63	syl	⊢ ( 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
65		elfz5	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑁 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
66	64 32 65	syl2anr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ≤ 𝑁 ) )
67	62 66	sylibrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 𝑁 ) ) )
68	67	necon1bd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
69	56 68	mpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
70	69	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( 0 · ( 𝑧 ↑ 𝑘 ) ) )
71		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
72	71 59 51	syl2an	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 𝑧 ↑ 𝑘 ) ∈ ℂ )
73	72	mul02d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( 0 · ( 𝑧 ↑ 𝑘 ) ) = 0 )
74	70 73	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 ... 𝑀 ) ∖ ( 0 ... 𝑁 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = 0 )
75		fzfid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → ( 0 ... 𝑀 ) ∈ Fin )
76	43 54 74 75	fsumss	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
77	27 76	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) )
78	77	mpteq2dva	⊢ ( 𝜑 → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( ( 𝐵 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
79	7 78	eqtrd	⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )