Metamath Proof Explorer

Theorem ply1termlem

Description: Lemma for ply1term . (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis ply1term.1 
|- F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
Assertion ply1termlem 
|- ( ( A e. CC /\ N e. NN0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 ply1term.1 
 |-  F = ( z e. CC |-> ( A x. ( z ^ N ) ) )
2 simplr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> N e. NN0 )
3 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
4 2 3 eleqtrdi 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> N e. ( ZZ>= ` 0 ) )
5 fzss1 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( N ... N ) C_ ( 0 ... N ) )
6 4 5 syl 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> ( N ... N ) C_ ( 0 ... N ) )
7 elfz1eq 
 |-  ( k e. ( N ... N ) -> k = N )
8 7 adantl 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> k = N )
9 iftrue 
 |-  ( k = N -> if ( k = N , A , 0 ) = A )
10 8 9 syl 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> if ( k = N , A , 0 ) = A )
11 simpll 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> A e. CC )
12 11 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> A e. CC )
13 10 12 eqeltrd 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> if ( k = N , A , 0 ) e. CC )
14 simplr 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> z e. CC )
15 2 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> N e. NN0 )
16 8 15 eqeltrd 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> k e. NN0 )
17 14 16 expcld 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> ( z ^ k ) e. CC )
18 13 17 mulcld 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( N ... N ) ) -> ( if ( k = N , A , 0 ) x. ( z ^ k ) ) e. CC )
19 eldifn 
 |-  ( k e. ( ( 0 ... N ) \ ( N ... N ) ) -> -. k e. ( N ... N ) )
20 19 adantl 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> -. k e. ( N ... N ) )
21 2 adantr 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> N e. NN0 )
22 21 nn0zd 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> N e. ZZ )
23 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
24 23 eleq2d 
 |-  ( N e. ZZ -> ( k e. ( N ... N ) <-> k e. { N } ) )
25 elsn2g 
 |-  ( N e. ZZ -> ( k e. { N } <-> k = N ) )
26 24 25 bitrd 
 |-  ( N e. ZZ -> ( k e. ( N ... N ) <-> k = N ) )
27 22 26 syl 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> ( k e. ( N ... N ) <-> k = N ) )
28 20 27 mtbid 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> -. k = N )
29 28 iffalsed 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> if ( k = N , A , 0 ) = 0 )
30 29 oveq1d 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = ( 0 x. ( z ^ k ) ) )
31 simpr 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> z e. CC )
32 eldifi 
 |-  ( k e. ( ( 0 ... N ) \ ( N ... N ) ) -> k e. ( 0 ... N ) )
33 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
34 32 33 syl 
 |-  ( k e. ( ( 0 ... N ) \ ( N ... N ) ) -> k e. NN0 )
35 expcl 
 |-  ( ( z e. CC /\ k e. NN0 ) -> ( z ^ k ) e. CC )
36 31 34 35 syl2an 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> ( z ^ k ) e. CC )
37 36 mul02d 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> ( 0 x. ( z ^ k ) ) = 0 )
38 30 37 eqtrd 
 |-  ( ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) /\ k e. ( ( 0 ... N ) \ ( N ... N ) ) ) -> ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = 0 )
39 fzfid 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> ( 0 ... N ) e. Fin )
40 6 18 38 39 fsumss 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> sum_ k e. ( N ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) )
41 2 nn0zd 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> N e. ZZ )
42 31 2 expcld 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> ( z ^ N ) e. CC )
43 11 42 mulcld 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> ( A x. ( z ^ N ) ) e. CC )
44 oveq2 
 |-  ( k = N -> ( z ^ k ) = ( z ^ N ) )
45 9 44 oveq12d 
 |-  ( k = N -> ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = ( A x. ( z ^ N ) ) )
46 45 fsum1 
 |-  ( ( N e. ZZ /\ ( A x. ( z ^ N ) ) e. CC ) -> sum_ k e. ( N ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = ( A x. ( z ^ N ) ) )
47 41 43 46 syl2anc 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> sum_ k e. ( N ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = ( A x. ( z ^ N ) ) )
48 40 47 eqtr3d 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ z e. CC ) -> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) = ( A x. ( z ^ N ) ) )
49 48 mpteq2dva 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) = ( z e. CC |-> ( A x. ( z ^ N ) ) ) )
50 1 49 eqtr4id 
 |-  ( ( A e. CC /\ N e. NN0 ) -> F = ( z e. CC |-> sum_ k e. ( 0 ... N ) ( if ( k = N , A , 0 ) x. ( z ^ k ) ) ) )