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 e. ( Poly ` S ) -> ( F ` 0 ) = ( A ` 0 ) )

Proof

Step Hyp Ref Expression
1 coefv0.1 
 |-  A = ( coeff ` F )
2 0cn 
 |-  0 e. CC
3 eqid 
 |-  ( deg ` F ) = ( deg ` F )
4 1 3 coeid2 
 |-  ( ( F e. ( Poly ` S ) /\ 0 e. CC ) -> ( F ` 0 ) = sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( 0 ^ k ) ) )
5 2 4 mpan2 
 |-  ( F e. ( Poly ` S ) -> ( F ` 0 ) = sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( 0 ^ k ) ) )
6 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 6 7 eleqtrdi 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. ( ZZ>= ` 0 ) )
9 fzss2 
 |-  ( ( deg ` F ) e. ( ZZ>= ` 0 ) -> ( 0 ... 0 ) C_ ( 0 ... ( deg ` F ) ) )
10 8 9 syl 
 |-  ( F e. ( Poly ` S ) -> ( 0 ... 0 ) C_ ( 0 ... ( deg ` F ) ) )
11 elfz1eq 
 |-  ( k e. ( 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 ) x. ( 0 ^ k ) ) = ( ( A ` 0 ) x. 1 ) )
17 11 16 syl 
 |-  ( k e. ( 0 ... 0 ) -> ( ( A ` k ) x. ( 0 ^ k ) ) = ( ( A ` 0 ) x. 1 ) )
18 1 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
19 0nn0 
 |-  0 e. NN0
20 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ 0 e. NN0 ) -> ( A ` 0 ) e. CC )
21 18 19 20 sylancl 
 |-  ( F e. ( Poly ` S ) -> ( A ` 0 ) e. CC )
22 21 mulridd 
 |-  ( F e. ( Poly ` S ) -> ( ( A ` 0 ) x. 1 ) = ( A ` 0 ) )
23 17 22 sylan9eqr 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... 0 ) ) -> ( ( A ` k ) x. ( 0 ^ k ) ) = ( A ` 0 ) )
24 21 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... 0 ) ) -> ( A ` 0 ) e. CC )
25 23 24 eqeltrd 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( 0 ... 0 ) ) -> ( ( A ` k ) x. ( 0 ^ k ) ) e. CC )
26 eldifn 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> -. k e. ( 0 ... 0 ) )
27 eldifi 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> k e. ( 0 ... ( deg ` F ) ) )
28 elfznn0 
 |-  ( k e. ( 0 ... ( deg ` F ) ) -> k e. NN0 )
29 27 28 syl 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> k e. NN0 )
30 elnn0 
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
31 29 30 sylib 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> ( k e. NN \/ k = 0 ) )
32 31 ord 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> ( -. k e. NN -> k = 0 ) )
33 id 
 |-  ( k = 0 -> k = 0 )
34 0z 
 |-  0 e. ZZ
35 elfz3 
 |-  ( 0 e. ZZ -> 0 e. ( 0 ... 0 ) )
36 34 35 ax-mp 
 |-  0 e. ( 0 ... 0 )
37 33 36 eqeltrdi 
 |-  ( k = 0 -> k e. ( 0 ... 0 ) )
38 32 37 syl6 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> ( -. k e. NN -> k e. ( 0 ... 0 ) ) )
39 26 38 mt3d 
 |-  ( k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) -> k e. NN )
40 39 adantl 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) ) -> k e. NN )
41 40 0expd 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) ) -> ( 0 ^ k ) = 0 )
42 41 oveq2d 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) ) -> ( ( A ` k ) x. ( 0 ^ k ) ) = ( ( A ` k ) x. 0 ) )
43 ffvelcdm 
 |-  ( ( A : NN0 --> CC /\ k e. NN0 ) -> ( A ` k ) e. CC )
44 18 29 43 syl2an 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) ) -> ( A ` k ) e. CC )
45 44 mul01d 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) ) -> ( ( A ` k ) x. 0 ) = 0 )
46 42 45 eqtrd 
 |-  ( ( F e. ( Poly ` S ) /\ k e. ( ( 0 ... ( deg ` F ) ) \ ( 0 ... 0 ) ) ) -> ( ( A ` k ) x. ( 0 ^ k ) ) = 0 )
47 fzfid 
 |-  ( F e. ( Poly ` S ) -> ( 0 ... ( deg ` F ) ) e. Fin )
48 10 25 46 47 fsumss 
 |-  ( F e. ( Poly ` S ) -> sum_ k e. ( 0 ... 0 ) ( ( A ` k ) x. ( 0 ^ k ) ) = sum_ k e. ( 0 ... ( deg ` F ) ) ( ( A ` k ) x. ( 0 ^ k ) ) )
49 22 21 eqeltrd 
 |-  ( F e. ( Poly ` S ) -> ( ( A ` 0 ) x. 1 ) e. CC )
50 16 fsum1 
 |-  ( ( 0 e. ZZ /\ ( ( A ` 0 ) x. 1 ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( A ` k ) x. ( 0 ^ k ) ) = ( ( A ` 0 ) x. 1 ) )
51 34 49 50 sylancr 
 |-  ( F e. ( Poly ` S ) -> sum_ k e. ( 0 ... 0 ) ( ( A ` k ) x. ( 0 ^ k ) ) = ( ( A ` 0 ) x. 1 ) )
52 51 22 eqtrd 
 |-  ( F e. ( Poly ` S ) -> sum_ k e. ( 0 ... 0 ) ( ( A ` k ) x. ( 0 ^ k ) ) = ( A ` 0 ) )
53 5 48 52 3eqtr2d 
 |-  ( F e. ( Poly ` S ) -> ( F ` 0 ) = ( A ` 0 ) )