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 ffvelrn
 |-  ( ( 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 mulid1d
 |-  ( 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 ffvelrn
 |-  ( ( 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 ) )