Metamath Proof Explorer

Theorem coeeq2

Description: Compute the coefficient function given a sum expression for the polynomial. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses dgrle.1 
|- ( ph -> F e. ( Poly ` S ) )
dgrle.2 
|- ( ph -> N e. NN0 )
dgrle.3 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
dgrle.4 
|- ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
Assertion coeeq2 
|- ( ph -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )

Proof

Step Hyp Ref Expression
1 dgrle.1 
 |-  ( ph -> F e. ( Poly ` S ) )
2 dgrle.2 
 |-  ( ph -> N e. NN0 )
3 dgrle.3 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> A e. CC )
4 dgrle.4 
 |-  ( ph -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
5 simpll 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> ph )
6 simpr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k <_ N )
7 simplr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k e. NN0 )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 7 8 eleqtrdi 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k e. ( ZZ>= ` 0 ) )
10 2 nn0zd 
 |-  ( ph -> N e. ZZ )
11 10 ad2antrr 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> N e. ZZ )
12 elfz5 
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
13 9 11 12 syl2anc 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> ( k e. ( 0 ... N ) <-> k <_ N ) )
14 6 13 mpbird 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> k e. ( 0 ... N ) )
15 5 14 3 syl2anc 
 |-  ( ( ( ph /\ k e. NN0 ) /\ k <_ N ) -> A e. CC )
16 0cnd 
 |-  ( ( ( ph /\ k e. NN0 ) /\ -. k <_ N ) -> 0 e. CC )
17 15 16 ifclda 
 |-  ( ( ph /\ k e. NN0 ) -> if ( k <_ N , A , 0 ) e. CC )
18 17 fmpttd 
 |-  ( ph -> ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) : NN0 --> CC )
19 simpr 
 |-  ( ( ph /\ k e. NN0 ) -> k e. NN0 )
20 eqid 
 |-  ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) )
21 20 fvmpt2 
 |-  ( ( k e. NN0 /\ if ( k <_ N , A , 0 ) e. CC ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = if ( k <_ N , A , 0 ) )
22 19 17 21 syl2anc 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = if ( k <_ N , A , 0 ) )
23 22 neeq1d 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 <-> if ( k <_ N , A , 0 ) =/= 0 ) )
24 iffalse 
 |-  ( -. k <_ N -> if ( k <_ N , A , 0 ) = 0 )
25 24 necon1ai 
 |-  ( if ( k <_ N , A , 0 ) =/= 0 -> k <_ N )
26 23 25 syl6bi 
 |-  ( ( ph /\ k e. NN0 ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) )
27 26 ralrimiva 
 |-  ( ph -> A. k e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) )
28 nfv 
 |-  F/ m ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N )
29 nffvmpt1 
 |-  F/_ k ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m )
30 nfcv 
 |-  F/_ k 0
31 29 30 nfne 
 |-  F/ k ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0
32 nfv 
 |-  F/ k m <_ N
33 31 32 nfim 
 |-  F/ k ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N )
34 fveq2 
 |-  ( k = m -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) )
35 34 neeq1d 
 |-  ( k = m -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 <-> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 ) )
36 breq1 
 |-  ( k = m -> ( k <_ N <-> m <_ N ) )
37 35 36 imbi12d 
 |-  ( k = m -> ( ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) <-> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) ) )
38 28 33 37 cbvralw 
 |-  ( A. k e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) =/= 0 -> k <_ N ) <-> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) )
39 27 38 sylib 
 |-  ( ph -> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) )
40 plyco0 
 |-  ( ( N e. NN0 /\ ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) : NN0 --> CC ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) ) )
41 2 18 40 syl2anc 
 |-  ( ph -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } <-> A. m e. NN0 ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) =/= 0 -> m <_ N ) ) )
42 39 41 mpbird 
 |-  ( ph -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) " ( ZZ>= ` ( N + 1 ) ) ) = { 0 } )
43 nfcv 
 |-  F/_ m ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) )
44 nfcv 
 |-  F/_ k x.
45 nfcv 
 |-  F/_ k ( z ^ m )
46 29 44 45 nfov 
 |-  F/_ k ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) )
47 oveq2 
 |-  ( k = m -> ( z ^ k ) = ( z ^ m ) )
48 34 47 oveq12d 
 |-  ( k = m -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) )
49 43 46 48 cbvsumi 
 |-  sum_ k e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) )
50 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
51 50 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> k e. NN0 )
52 elfzle2 
 |-  ( k e. ( 0 ... N ) -> k <_ N )
53 52 adantl 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> k <_ N )
54 53 iftrued 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> if ( k <_ N , A , 0 ) = A )
55 3 adantlr 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> A e. CC )
56 54 55 eqeltrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> if ( k <_ N , A , 0 ) e. CC )
57 51 56 21 syl2anc 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = if ( k <_ N , A , 0 ) )
58 57 54 eqtrd 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) = A )
59 58 oveq1d 
 |-  ( ( ( ph /\ z e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = ( A x. ( z ^ k ) ) )
60 59 sumeq2dv 
 |-  ( ( ph /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` k ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) )
61 49 60 eqtr3id 
 |-  ( ( ph /\ z e. CC ) -> sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) = sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) )
62 61 mpteq2dva 
 |-  ( ph -> ( z e. CC |-> sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) ) = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( A x. ( z ^ k ) ) ) )
63 4 62 eqtr4d 
 |-  ( ph -> F = ( z e. CC |-> sum_ m e. ( 0 ... N ) ( ( ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) ` m ) x. ( z ^ m ) ) ) )
64 1 2 18 42 63 coeeq 
 |-  ( ph -> ( coeff ` F ) = ( k e. NN0 |-> if ( k <_ N , A , 0 ) ) )