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	$⊢ A = coeff (F)$
	Assertion	coefv0	$⊢ F \in Poly (S) \to F (0) = A (0)$

Proof

Step	Hyp	Ref	Expression
1		coefv0.1	$⊢ A = coeff (F)$
2		0cn	$⊢ 0 \in ℂ$
3		eqid	$⊢ \deg (F) = \deg (F)$
4	1 3	coeid2	$⊢ (F \in Poly (S) \land 0 \in ℂ) \to F (0) = \sum_{k = 0}^{\deg (F)} A (k) 0^{k}$
5	2 4	mpan2	$⊢ F \in Poly (S) \to F (0) = \sum_{k = 0}^{\deg (F)} A (k) 0^{k}$
6		dgrcl	$⊢ F \in Poly (S) \to \deg (F) \in ℕ_{0}$
7		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
8	6 7	eleqtrdi	$⊢ F \in Poly (S) \to \deg (F) \in ℤ_{\geq 0}$
9		fzss2	$⊢ \deg (F) \in ℤ_{\geq 0} \to (0 \dots 0) \subseteq (0 \dots \deg (F))$
10	8 9	syl	$⊢ F \in Poly (S) \to (0 \dots 0) \subseteq (0 \dots \deg (F))$
11		elfz1eq	$⊢ k \in (0 \dots 0) \to k = 0$
12		fveq2	$⊢ k = 0 \to A (k) = A (0)$
13		oveq2	$⊢ k = 0 \to 0^{k} = 0^{0}$
14		0exp0e1	$⊢ 0^{0} = 1$
15	13 14	eqtrdi	$⊢ k = 0 \to 0^{k} = 1$
16	12 15	oveq12d	$⊢ k = 0 \to A (k) 0^{k} = A (0) \cdot 1$
17	11 16	syl	$⊢ k \in (0 \dots 0) \to A (k) 0^{k} = A (0) \cdot 1$
18	1	coef3	$⊢ F \in Poly (S) \to A : ℕ_{0} ⟶ ℂ$
19		0nn0	$⊢ 0 \in ℕ_{0}$
20		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land 0 \in ℕ_{0}) \to A (0) \in ℂ$
21	18 19 20	sylancl	$⊢ F \in Poly (S) \to A (0) \in ℂ$
22	21	mulid1d	$⊢ F \in Poly (S) \to A (0) \cdot 1 = A (0)$
23	17 22	sylan9eqr	$⊢ (F \in Poly (S) \land k \in (0 \dots 0)) \to A (k) 0^{k} = A (0)$
24	21	adantr	$⊢ (F \in Poly (S) \land k \in (0 \dots 0)) \to A (0) \in ℂ$
25	23 24	eqeltrd	$⊢ (F \in Poly (S) \land k \in (0 \dots 0)) \to A (k) 0^{k} \in ℂ$
26		eldifn	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to \neg k \in (0 \dots 0)$
27		eldifi	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to k \in (0 \dots \deg (F))$
28		elfznn0	$⊢ k \in (0 \dots \deg (F)) \to k \in ℕ_{0}$
29	27 28	syl	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to k \in ℕ_{0}$
30		elnn0	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℕ \lor k = 0)$
31	29 30	sylib	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to (k \in ℕ \lor k = 0)$
32	31	ord	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to (\neg k \in ℕ \to k = 0)$
33		id	$⊢ k = 0 \to k = 0$
34		0z	$⊢ 0 \in ℤ$
35		elfz3	$⊢ 0 \in ℤ \to 0 \in (0 \dots 0)$
36	34 35	ax-mp	$⊢ 0 \in (0 \dots 0)$
37	33 36	eqeltrdi	$⊢ k = 0 \to k \in (0 \dots 0)$
38	32 37	syl6	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to (\neg k \in ℕ \to k \in (0 \dots 0))$
39	26 38	mt3d	$⊢ k \in ((0 \dots \deg (F)) ∖ (0 \dots 0)) \to k \in ℕ$
40	39	adantl	$⊢ (F \in Poly (S) \land k \in ((0 \dots \deg (F)) ∖ (0 \dots 0))) \to k \in ℕ$
41	40	0expd	$⊢ (F \in Poly (S) \land k \in ((0 \dots \deg (F)) ∖ (0 \dots 0))) \to 0^{k} = 0$
42	41	oveq2d	$⊢ (F \in Poly (S) \land k \in ((0 \dots \deg (F)) ∖ (0 \dots 0))) \to A (k) 0^{k} = A (k) \cdot 0$
43		ffvelrn	$⊢ (A : ℕ_{0} ⟶ ℂ \land k \in ℕ_{0}) \to A (k) \in ℂ$
44	18 29 43	syl2an	$⊢ (F \in Poly (S) \land k \in ((0 \dots \deg (F)) ∖ (0 \dots 0))) \to A (k) \in ℂ$
45	44	mul01d	$⊢ (F \in Poly (S) \land k \in ((0 \dots \deg (F)) ∖ (0 \dots 0))) \to A (k) \cdot 0 = 0$
46	42 45	eqtrd	$⊢ (F \in Poly (S) \land k \in ((0 \dots \deg (F)) ∖ (0 \dots 0))) \to A (k) 0^{k} = 0$
47		fzfid	$⊢ F \in Poly (S) \to (0 \dots \deg (F)) \in Fin$
48	10 25 46 47	fsumss	$⊢ F \in Poly (S) \to \sum_{k = 0}^{0} A (k) 0^{k} = \sum_{k = 0}^{\deg (F)} A (k) 0^{k}$
49	22 21	eqeltrd	$⊢ F \in Poly (S) \to A (0) \cdot 1 \in ℂ$
50	16	fsum1	$⊢ (0 \in ℤ \land A (0) \cdot 1 \in ℂ) \to \sum_{k = 0}^{0} A (k) 0^{k} = A (0) \cdot 1$
51	34 49 50	sylancr	$⊢ F \in Poly (S) \to \sum_{k = 0}^{0} A (k) 0^{k} = A (0) \cdot 1$
52	51 22	eqtrd	$⊢ F \in Poly (S) \to \sum_{k = 0}^{0} A (k) 0^{k} = A (0)$
53	5 48 52	3eqtr2d	$⊢ F \in Poly (S) \to F (0) = A (0)$

Metamath Proof Explorer

Theorem coefv0

Proof