Metamath Proof Explorer

Theorem basellem2

Description: Lemma for basel . Show that P is a polynomial of degree M , and compute its coefficient function. (Contributed by Mario Carneiro, 30-Jul-2014)

Ref Expression
Hypotheses basel.n 
|- N = ( ( 2 x. M ) + 1 )
basel.p 
|- P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
Assertion basellem2 
|- ( M e. NN -> ( P e. ( Poly ` CC ) /\ ( deg ` P ) = M /\ ( coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 basel.n 
 |-  N = ( ( 2 x. M ) + 1 )
2 basel.p 
 |-  P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
3 ssidd 
 |-  ( M e. NN -> CC C_ CC )
4 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
5 elfznn0 
 |-  ( j e. ( 0 ... M ) -> j e. NN0 )
6 oveq2 
 |-  ( n = j -> ( 2 x. n ) = ( 2 x. j ) )
7 6 oveq2d 
 |-  ( n = j -> ( N _C ( 2 x. n ) ) = ( N _C ( 2 x. j ) ) )
8 oveq2 
 |-  ( n = j -> ( M - n ) = ( M - j ) )
9 8 oveq2d 
 |-  ( n = j -> ( -u 1 ^ ( M - n ) ) = ( -u 1 ^ ( M - j ) ) )
10 7 9 oveq12d 
 |-  ( n = j -> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) = ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) )
11 eqid 
 |-  ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) )
12 ovex 
 |-  ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) e. _V
13 10 11 12 fvmpt 
 |-  ( j e. NN0 -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) )
14 5 13 syl 
 |-  ( j e. ( 0 ... M ) -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) )
15 14 adantl 
 |-  ( ( M e. NN /\ j e. ( 0 ... M ) ) -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) )
16 2nn 
 |-  2 e. NN
17 nnmulcl 
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
18 16 17 mpan 
 |-  ( M e. NN -> ( 2 x. M ) e. NN )
19 18 peano2nnd 
 |-  ( M e. NN -> ( ( 2 x. M ) + 1 ) e. NN )
20 1 19 eqeltrid 
 |-  ( M e. NN -> N e. NN )
21 20 nnnn0d 
 |-  ( M e. NN -> N e. NN0 )
22 2z 
 |-  2 e. ZZ
23 nn0z 
 |-  ( n e. NN0 -> n e. ZZ )
24 zmulcl 
 |-  ( ( 2 e. ZZ /\ n e. ZZ ) -> ( 2 x. n ) e. ZZ )
25 22 23 24 sylancr 
 |-  ( n e. NN0 -> ( 2 x. n ) e. ZZ )
26 bccl 
 |-  ( ( N e. NN0 /\ ( 2 x. n ) e. ZZ ) -> ( N _C ( 2 x. n ) ) e. NN0 )
27 21 25 26 syl2an 
 |-  ( ( M e. NN /\ n e. NN0 ) -> ( N _C ( 2 x. n ) ) e. NN0 )
28 27 nn0cnd 
 |-  ( ( M e. NN /\ n e. NN0 ) -> ( N _C ( 2 x. n ) ) e. CC )
29 neg1cn 
 |-  -u 1 e. CC
30 neg1ne0 
 |-  -u 1 =/= 0
31 nnz 
 |-  ( M e. NN -> M e. ZZ )
32 zsubcl 
 |-  ( ( M e. ZZ /\ n e. ZZ ) -> ( M - n ) e. ZZ )
33 31 23 32 syl2an 
 |-  ( ( M e. NN /\ n e. NN0 ) -> ( M - n ) e. ZZ )
34 expclz 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ ( M - n ) e. ZZ ) -> ( -u 1 ^ ( M - n ) ) e. CC )
35 29 30 33 34 mp3an12i 
 |-  ( ( M e. NN /\ n e. NN0 ) -> ( -u 1 ^ ( M - n ) ) e. CC )
36 28 35 mulcld 
 |-  ( ( M e. NN /\ n e. NN0 ) -> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) e. CC )
37 36 fmpttd 
 |-  ( M e. NN -> ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) : NN0 --> CC )
38 ffvelcdm 
 |-  ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) : NN0 --> CC /\ j e. NN0 ) -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) e. CC )
39 37 5 38 syl2an 
 |-  ( ( M e. NN /\ j e. ( 0 ... M ) ) -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) e. CC )
40 15 39 eqeltrrd 
 |-  ( ( M e. NN /\ j e. ( 0 ... M ) ) -> ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) e. CC )
41 3 4 40 elplyd 
 |-  ( M e. NN -> ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) ) e. ( Poly ` CC ) )
42 2 41 eqeltrid 
 |-  ( M e. NN -> P e. ( Poly ` CC ) )
43 nnre 
 |-  ( M e. NN -> M e. RR )
44 nn0re 
 |-  ( j e. NN0 -> j e. RR )
45 ltnle 
 |-  ( ( M e. RR /\ j e. RR ) -> ( M < j <-> -. j <_ M ) )
46 43 44 45 syl2an 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( M < j <-> -. j <_ M ) )
47 13 ad2antlr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) )
48 21 ad2antrr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> N e. NN0 )
49 nn0z 
 |-  ( j e. NN0 -> j e. ZZ )
50 49 ad2antlr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> j e. ZZ )
51 zmulcl 
 |-  ( ( 2 e. ZZ /\ j e. ZZ ) -> ( 2 x. j ) e. ZZ )
52 22 50 51 sylancr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 x. j ) e. ZZ )
53 ax-1cn 
 |-  1 e. CC
54 53 2timesi 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
55 54 oveq2i 
 |-  ( ( 2 x. M ) + ( 2 x. 1 ) ) = ( ( 2 x. M ) + ( 1 + 1 ) )
56 2cnd 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> 2 e. CC )
57 nncn 
 |-  ( M e. NN -> M e. CC )
58 57 ad2antrr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> M e. CC )
59 53 a1i 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> 1 e. CC )
60 56 58 59 adddid 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 x. ( M + 1 ) ) = ( ( 2 x. M ) + ( 2 x. 1 ) ) )
61 1 oveq1i 
 |-  ( N + 1 ) = ( ( ( 2 x. M ) + 1 ) + 1 )
62 18 ad2antrr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 x. M ) e. NN )
63 62 nncnd 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 x. M ) e. CC )
64 63 59 59 addassd 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( ( ( 2 x. M ) + 1 ) + 1 ) = ( ( 2 x. M ) + ( 1 + 1 ) ) )
65 61 64 eqtrid 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( N + 1 ) = ( ( 2 x. M ) + ( 1 + 1 ) ) )
66 55 60 65 3eqtr4a 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 x. ( M + 1 ) ) = ( N + 1 ) )
67 zltp1le 
 |-  ( ( M e. ZZ /\ j e. ZZ ) -> ( M < j <-> ( M + 1 ) <_ j ) )
68 31 49 67 syl2an 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( M < j <-> ( M + 1 ) <_ j ) )
69 68 biimpa 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( M + 1 ) <_ j )
70 43 ad2antrr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> M e. RR )
71 peano2re 
 |-  ( M e. RR -> ( M + 1 ) e. RR )
72 70 71 syl 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( M + 1 ) e. RR )
73 44 ad2antlr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> j e. RR )
74 2re 
 |-  2 e. RR
75 2pos 
 |-  0 < 2
76 74 75 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
77 76 a1i 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 e. RR /\ 0 < 2 ) )
78 lemul2 
 |-  ( ( ( M + 1 ) e. RR /\ j e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( M + 1 ) <_ j <-> ( 2 x. ( M + 1 ) ) <_ ( 2 x. j ) ) )
79 72 73 77 78 syl3anc 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( ( M + 1 ) <_ j <-> ( 2 x. ( M + 1 ) ) <_ ( 2 x. j ) ) )
80 69 79 mpbid 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 2 x. ( M + 1 ) ) <_ ( 2 x. j ) )
81 66 80 eqbrtrrd 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( N + 1 ) <_ ( 2 x. j ) )
82 20 nnzd 
 |-  ( M e. NN -> N e. ZZ )
83 82 ad2antrr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> N e. ZZ )
84 zltp1le 
 |-  ( ( N e. ZZ /\ ( 2 x. j ) e. ZZ ) -> ( N < ( 2 x. j ) <-> ( N + 1 ) <_ ( 2 x. j ) ) )
85 83 52 84 syl2anc 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( N < ( 2 x. j ) <-> ( N + 1 ) <_ ( 2 x. j ) ) )
86 81 85 mpbird 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> N < ( 2 x. j ) )
87 86 olcd 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( ( 2 x. j ) < 0 \/ N < ( 2 x. j ) ) )
88 bcval4 
 |-  ( ( N e. NN0 /\ ( 2 x. j ) e. ZZ /\ ( ( 2 x. j ) < 0 \/ N < ( 2 x. j ) ) ) -> ( N _C ( 2 x. j ) ) = 0 )
89 48 52 87 88 syl3anc 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( N _C ( 2 x. j ) ) = 0 )
90 89 oveq1d 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) = ( 0 x. ( -u 1 ^ ( M - j ) ) ) )
91 zsubcl 
 |-  ( ( M e. ZZ /\ j e. ZZ ) -> ( M - j ) e. ZZ )
92 31 49 91 syl2an 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( M - j ) e. ZZ )
93 expclz 
 |-  ( ( -u 1 e. CC /\ -u 1 =/= 0 /\ ( M - j ) e. ZZ ) -> ( -u 1 ^ ( M - j ) ) e. CC )
94 29 30 92 93 mp3an12i 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( -u 1 ^ ( M - j ) ) e. CC )
95 94 adantr 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( -u 1 ^ ( M - j ) ) e. CC )
96 95 mul02d 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( 0 x. ( -u 1 ^ ( M - j ) ) ) = 0 )
97 47 90 96 3eqtrd 
 |-  ( ( ( M e. NN /\ j e. NN0 ) /\ M < j ) -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = 0 )
98 97 ex 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( M < j -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = 0 ) )
99 46 98 sylbird 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( -. j <_ M -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) = 0 ) )
100 99 necon1ad 
 |-  ( ( M e. NN /\ j e. NN0 ) -> ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) =/= 0 -> j <_ M ) )
101 100 ralrimiva 
 |-  ( M e. NN -> A. j e. NN0 ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) =/= 0 -> j <_ M ) )
102 plyco0 
 |-  ( ( M e. NN0 /\ ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) : NN0 --> CC ) -> ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. j e. NN0 ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) =/= 0 -> j <_ M ) ) )
103 4 37 102 syl2anc 
 |-  ( M e. NN -> ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } <-> A. j e. NN0 ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) =/= 0 -> j <_ M ) ) )
104 101 103 mpbird 
 |-  ( M e. NN -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) " ( ZZ>= ` ( M + 1 ) ) ) = { 0 } )
105 14 oveq1d 
 |-  ( j e. ( 0 ... M ) -> ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) x. ( t ^ j ) ) = ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
106 105 sumeq2i 
 |-  sum_ j e. ( 0 ... M ) ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) x. ( t ^ j ) ) = sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) )
107 106 mpteq2i 
 |-  ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) x. ( t ^ j ) ) ) = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( N _C ( 2 x. j ) ) x. ( -u 1 ^ ( M - j ) ) ) x. ( t ^ j ) ) )
108 2 107 eqtr4i 
 |-  P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) x. ( t ^ j ) ) )
109 108 a1i 
 |-  ( M e. NN -> P = ( t e. CC |-> sum_ j e. ( 0 ... M ) ( ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` j ) x. ( t ^ j ) ) ) )
110 oveq2 
 |-  ( n = M -> ( 2 x. n ) = ( 2 x. M ) )
111 110 oveq2d 
 |-  ( n = M -> ( N _C ( 2 x. n ) ) = ( N _C ( 2 x. M ) ) )
112 oveq2 
 |-  ( n = M -> ( M - n ) = ( M - M ) )
113 112 oveq2d 
 |-  ( n = M -> ( -u 1 ^ ( M - n ) ) = ( -u 1 ^ ( M - M ) ) )
114 111 113 oveq12d 
 |-  ( n = M -> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) = ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) )
115 ovex 
 |-  ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) e. _V
116 114 11 115 fvmpt 
 |-  ( M e. NN0 -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) = ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) )
117 4 116 syl 
 |-  ( M e. NN -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) = ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) )
118 57 subidd 
 |-  ( M e. NN -> ( M - M ) = 0 )
119 118 oveq2d 
 |-  ( M e. NN -> ( -u 1 ^ ( M - M ) ) = ( -u 1 ^ 0 ) )
120 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
121 29 120 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
122 119 121 eqtrdi 
 |-  ( M e. NN -> ( -u 1 ^ ( M - M ) ) = 1 )
123 122 oveq2d 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) x. ( -u 1 ^ ( M - M ) ) ) = ( ( N _C ( 2 x. M ) ) x. 1 ) )
124 18 nnred 
 |-  ( M e. NN -> ( 2 x. M ) e. RR )
125 124 lep1d 
 |-  ( M e. NN -> ( 2 x. M ) <_ ( ( 2 x. M ) + 1 ) )
126 125 1 breqtrrdi 
 |-  ( M e. NN -> ( 2 x. M ) <_ N )
127 18 nnnn0d 
 |-  ( M e. NN -> ( 2 x. M ) e. NN0 )
128 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
129 127 128 eleqtrdi 
 |-  ( M e. NN -> ( 2 x. M ) e. ( ZZ>= ` 0 ) )
130 elfz5 
 |-  ( ( ( 2 x. M ) e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( ( 2 x. M ) e. ( 0 ... N ) <-> ( 2 x. M ) <_ N ) )
131 129 82 130 syl2anc 
 |-  ( M e. NN -> ( ( 2 x. M ) e. ( 0 ... N ) <-> ( 2 x. M ) <_ N ) )
132 126 131 mpbird 
 |-  ( M e. NN -> ( 2 x. M ) e. ( 0 ... N ) )
133 bccl2 
 |-  ( ( 2 x. M ) e. ( 0 ... N ) -> ( N _C ( 2 x. M ) ) e. NN )
134 132 133 syl 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) e. NN )
135 134 nncnd 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) e. CC )
136 135 mulridd 
 |-  ( M e. NN -> ( ( N _C ( 2 x. M ) ) x. 1 ) = ( N _C ( 2 x. M ) ) )
137 117 123 136 3eqtrd 
 |-  ( M e. NN -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) = ( N _C ( 2 x. M ) ) )
138 134 nnne0d 
 |-  ( M e. NN -> ( N _C ( 2 x. M ) ) =/= 0 )
139 137 138 eqnetrd 
 |-  ( M e. NN -> ( ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ` M ) =/= 0 )
140 42 4 37 104 109 139 dgreq 
 |-  ( M e. NN -> ( deg ` P ) = M )
141 42 4 37 104 109 coeeq 
 |-  ( M e. NN -> ( coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) )
142 42 140 141 3jca 
 |-  ( M e. NN -> ( P e. ( Poly ` CC ) /\ ( deg ` P ) = M /\ ( coeff ` P ) = ( n e. NN0 |-> ( ( N _C ( 2 x. n ) ) x. ( -u 1 ^ ( M - n ) ) ) ) ) )