Theorem coefv0

Description: The result of evaluating a polynomial at zero is the constant term. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypothesis	coefv0.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion	coefv0	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	⊢ 𝐴 = ( coeff ‘ 𝐹 )
2		0cn	⊢ 0 ∈ ℂ
3		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
4	1 3	coeid2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 0 ∈ ℂ ) → ( 𝐹 ‘ 0 ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
5	2 4	mpan2	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
6		dgrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
7		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
8	6 7	eleqtrdi	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) )
9		fzss2	⊢ ( ( deg ‘ 𝐹 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... 0 ) ⊆ ( 0 ... ( deg ‘ 𝐹 ) ) )
10	8 9	syl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0 ... 0 ) ⊆ ( 0 ... ( deg ‘ 𝐹 ) ) )
11		elfz1eq	⊢ ( 𝑘 ∈ ( 0 ... 0 ) → 𝑘 = 0 )
12		fveq2	⊢ ( 𝑘 = 0 → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ 0 ) )
13		oveq2	⊢ ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = ( 0 ↑ 0 ) )
14		0exp0e1	⊢ ( 0 ↑ 0 ) = 1
15	13 14	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 ↑ 𝑘 ) = 1 )
16	12 15	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
17	11 16	syl	⊢ ( 𝑘 ∈ ( 0 ... 0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
18	1	coef3	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐴 : ℕ0 ⟶ ℂ )
19		0nn0	⊢ 0 ∈ ℕ0
20		ffvelcdm	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
21	18 19 20	sylancl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
22	21	mulridd	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 ‘ 0 ) · 1 ) = ( 𝐴 ‘ 0 ) )
23	17 22	sylan9eqr	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( 𝐴 ‘ 0 ) )
24	21	adantr	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( 𝐴 ‘ 0 ) ∈ ℂ )
25	23 24	eqeltrd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) ∈ ℂ )
26		eldifn	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ¬ 𝑘 ∈ ( 0 ... 0 ) )
27		eldifi	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) )
28		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) → 𝑘 ∈ ℕ0 )
29	27 28	syl	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ℕ0 )
30		elnn0	⊢ ( 𝑘 ∈ ℕ0 ↔ ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
31	29 30	sylib	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ( 𝑘 ∈ ℕ ∨ 𝑘 = 0 ) )
32	31	ord	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 = 0 ) )
33		id	⊢ ( 𝑘 = 0 → 𝑘 = 0 )
34		0z	⊢ 0 ∈ ℤ
35		elfz3	⊢ ( 0 ∈ ℤ → 0 ∈ ( 0 ... 0 ) )
36	34 35	ax-mp	⊢ 0 ∈ ( 0 ... 0 )
37	33 36	eqeltrdi	⊢ ( 𝑘 = 0 → 𝑘 ∈ ( 0 ... 0 ) )
38	32 37	syl6	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → ( ¬ 𝑘 ∈ ℕ → 𝑘 ∈ ( 0 ... 0 ) ) )
39	26 38	mt3d	⊢ ( 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) → 𝑘 ∈ ℕ )
40	39	adantl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → 𝑘 ∈ ℕ )
41	40	0expd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( 0 ↑ 𝑘 ) = 0 )
42	41	oveq2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 𝑘 ) · 0 ) )
43		ffvelcdm	⊢ ( ( 𝐴 : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
44	18 29 43	syl2an	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
45	44	mul01d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 0 ) = 0 )
46	42 45	eqtrd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑘 ∈ ( ( 0 ... ( deg ‘ 𝐹 ) ) ∖ ( 0 ... 0 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = 0 )
47		fzfid	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 0 ... ( deg ‘ 𝐹 ) ) ∈ Fin )
48	10 25 46 47	fsumss	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝐹 ) ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) )
49	22 21	eqeltrd	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( ( 𝐴 ‘ 0 ) · 1 ) ∈ ℂ )
50	16	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( ( 𝐴 ‘ 0 ) · 1 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
51	34 49 50	sylancr	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( ( 𝐴 ‘ 0 ) · 1 ) )
52	51 22	eqtrd	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 𝐴 ‘ 𝑘 ) · ( 0 ↑ 𝑘 ) ) = ( 𝐴 ‘ 0 ) )
53	5 48 52	3eqtr2d	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 ‘ 0 ) = ( 𝐴 ‘ 0 ) )