Theorem coe1termlem

Description: The coefficient function of a monomial. (Contributed by Mario Carneiro, 26-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypothesis	coe1term.1	⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
Assertion	coe1termlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ∧ ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1term.1	⊢ 𝐹 = ( 𝑧 ∈ ℂ ↦ ( 𝐴 · ( 𝑧 ↑ 𝑁 ) ) )
2		ssid	⊢ ℂ ⊆ ℂ
3	1	ply1term	⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
4	2 3	mp3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
5		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
6		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
7		0cn	⊢ 0 ∈ ℂ
8		ifcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
9	6 7 8	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
10	9	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑛 ∈ ℕ0 ) → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
11	10	fmpttd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ )
12		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) )
13		eqeq1	⊢ ( 𝑛 = 𝑘 → ( 𝑛 = 𝑁 ↔ 𝑘 = 𝑁 ) )
14	13	ifbid	⊢ ( 𝑛 = 𝑘 → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) = if ( 𝑘 = 𝑁 , 𝐴 , 0 ) )
15		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
16		ifcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
17	6 7 16	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
18	17	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ∈ ℂ )
19	12 14 15 18	fvmptd3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝑁 , 𝐴 , 0 ) )
20	19	neeq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 ↔ if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 ) )
21		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
22	21	leidd	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ 𝑁 )
23	22	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑁 ≤ 𝑁 )
24		iffalse	⊢ ( ¬ 𝑘 = 𝑁 → if ( 𝑘 = 𝑁 , 𝐴 , 0 ) = 0 )
25	24	necon1ai	⊢ ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 → 𝑘 = 𝑁 )
26	25	breq1d	⊢ ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 → ( 𝑘 ≤ 𝑁 ↔ 𝑁 ≤ 𝑁 ) )
27	23 26	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
28	20 27	sylbid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
29	28	ralrimiva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) )
30		plyco0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
31	5 11 30	syl2anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } ↔ ∀ 𝑘 ∈ ℕ0 ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ 𝑁 ) ) )
32	29 31	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
33	1	ply1termlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
34		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
35	19	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
36	34 35	sylan2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
37	36	sumeq2dv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) )
38	37	mpteq2dv	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( if ( 𝑘 = 𝑁 , 𝐴 , 0 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
39	33 38	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
40	4 5 11 32 39	coeeq	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) )
41	4	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
42	5	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → 𝑁 ∈ ℕ0 )
43	11	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) : ℕ0 ⟶ ℂ )
44	32	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
45	39	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → 𝐹 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
46		iftrue	⊢ ( 𝑛 = 𝑁 → if ( 𝑛 = 𝑁 , 𝐴 , 0 ) = 𝐴 )
47	46 12	fvmptg	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) = 𝐴 )
48	47	ancoms	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) = 𝐴 )
49	48	neeq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) ≠ 0 ↔ 𝐴 ≠ 0 ) )
50	49	biimpar	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ‘ 𝑁 ) ≠ 0 )
51	41 42 43 44 45 50	dgreq	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ≠ 0 ) → ( deg ‘ 𝐹 ) = 𝑁 )
52	51	ex	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) )
53	40 52	jca	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( coeff ‘ 𝐹 ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 𝑁 , 𝐴 , 0 ) ) ∧ ( 𝐴 ≠ 0 → ( deg ‘ 𝐹 ) = 𝑁 ) ) )