Metamath Proof Explorer


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 A = coeff F
Assertion coefv0 F Poly S F 0 = A 0

Proof

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