Metamath Proof Explorer

Theorem bpolydiflem

Description: Lemma for bpolydif . (Contributed by Scott Fenton, 12-Jun-2014)

Ref Expression
Hypotheses bpolydiflem.1 
|- ( ph -> N e. NN )
bpolydiflem.2 
|- ( ph -> X e. CC )
bpolydiflem.3 
|- ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) )
Assertion bpolydiflem 
|- ( ph -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 bpolydiflem.1 
 |-  ( ph -> N e. NN )
2 bpolydiflem.2 
 |-  ( ph -> X e. CC )
3 bpolydiflem.3 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) )
4 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
5 peano2cn 
 |-  ( X e. CC -> ( X + 1 ) e. CC )
6 2 5 syl 
 |-  ( ph -> ( X + 1 ) e. CC )
7 bpolyval 
 |-  ( ( N e. NN0 /\ ( X + 1 ) e. CC ) -> ( N BernPoly ( X + 1 ) ) = ( ( ( X + 1 ) ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) )
8 4 6 7 syl2anc 
 |-  ( ph -> ( N BernPoly ( X + 1 ) ) = ( ( ( X + 1 ) ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) )
9 bpolyval 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
10 4 2 9 syl2anc 
 |-  ( ph -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
11 8 10 oveq12d 
 |-  ( ph -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( ( ( ( X + 1 ) ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) - ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) )
12 6 4 expcld 
 |-  ( ph -> ( ( X + 1 ) ^ N ) e. CC )
13 fzfid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) e. Fin )
14 elfzelz 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. ZZ )
15 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
16 4 14 15 syl2an 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( N _C k ) e. NN0 )
17 16 nn0cnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( N _C k ) e. CC )
18 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
19 bpolycl 
 |-  ( ( k e. NN0 /\ ( X + 1 ) e. CC ) -> ( k BernPoly ( X + 1 ) ) e. CC )
20 18 6 19 syl2anr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k BernPoly ( X + 1 ) ) e. CC )
21 fzssp1 
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
22 1 nncnd 
 |-  ( ph -> N e. CC )
23 ax-1cn 
 |-  1 e. CC
24 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
25 22 23 24 sylancl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
26 25 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
27 21 26 sseqtrid 
 |-  ( ph -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
28 27 sselda 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. ( 0 ... N ) )
29 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
30 28 29 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( N - k ) e. NN0 )
31 nn0p1nn 
 |-  ( ( N - k ) e. NN0 -> ( ( N - k ) + 1 ) e. NN )
32 30 31 syl 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - k ) + 1 ) e. NN )
33 32 nncnd 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - k ) + 1 ) e. CC )
34 32 nnne0d 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - k ) + 1 ) =/= 0 )
35 20 33 34 divcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) e. CC )
36 17 35 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) e. CC )
37 13 36 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) e. CC )
38 2 4 expcld 
 |-  ( ph -> ( X ^ N ) e. CC )
39 bpolycl 
 |-  ( ( k e. NN0 /\ X e. CC ) -> ( k BernPoly X ) e. CC )
40 18 2 39 syl2anr 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k BernPoly X ) e. CC )
41 40 33 34 divcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) e. CC )
42 17 41 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
43 13 42 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
44 12 37 38 43 sub4d 
 |-  ( ph -> ( ( ( ( X + 1 ) ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) - ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) = ( ( ( ( X + 1 ) ^ N ) - ( X ^ N ) ) - ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) )
45 27 sselda 
 |-  ( ( ph /\ m e. ( 0 ... ( N - 1 ) ) ) -> m e. ( 0 ... N ) )
46 bccl2 
 |-  ( m e. ( 0 ... N ) -> ( N _C m ) e. NN )
47 46 adantl 
 |-  ( ( ph /\ m e. ( 0 ... N ) ) -> ( N _C m ) e. NN )
48 47 nncnd 
 |-  ( ( ph /\ m e. ( 0 ... N ) ) -> ( N _C m ) e. CC )
49 elfznn0 
 |-  ( m e. ( 0 ... N ) -> m e. NN0 )
50 expcl 
 |-  ( ( X e. CC /\ m e. NN0 ) -> ( X ^ m ) e. CC )
51 2 49 50 syl2an 
 |-  ( ( ph /\ m e. ( 0 ... N ) ) -> ( X ^ m ) e. CC )
52 48 51 mulcld 
 |-  ( ( ph /\ m e. ( 0 ... N ) ) -> ( ( N _C m ) x. ( X ^ m ) ) e. CC )
53 45 52 syldan 
 |-  ( ( ph /\ m e. ( 0 ... ( N - 1 ) ) ) -> ( ( N _C m ) x. ( X ^ m ) ) e. CC )
54 13 53 fsumcl 
 |-  ( ph -> sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) e. CC )
55 addcom 
 |-  ( ( X e. CC /\ 1 e. CC ) -> ( X + 1 ) = ( 1 + X ) )
56 2 23 55 sylancl 
 |-  ( ph -> ( X + 1 ) = ( 1 + X ) )
57 56 oveq1d 
 |-  ( ph -> ( ( X + 1 ) ^ N ) = ( ( 1 + X ) ^ N ) )
58 binom1p 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( ( 1 + X ) ^ N ) = sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( X ^ m ) ) )
59 2 4 58 syl2anc 
 |-  ( ph -> ( ( 1 + X ) ^ N ) = sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( X ^ m ) ) )
60 57 59 eqtrd 
 |-  ( ph -> ( ( X + 1 ) ^ N ) = sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( X ^ m ) ) )
61 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
62 4 61 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
63 oveq2 
 |-  ( m = N -> ( N _C m ) = ( N _C N ) )
64 oveq2 
 |-  ( m = N -> ( X ^ m ) = ( X ^ N ) )
65 63 64 oveq12d 
 |-  ( m = N -> ( ( N _C m ) x. ( X ^ m ) ) = ( ( N _C N ) x. ( X ^ N ) ) )
66 62 52 65 fsumm1 
 |-  ( ph -> sum_ m e. ( 0 ... N ) ( ( N _C m ) x. ( X ^ m ) ) = ( sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( ( N _C N ) x. ( X ^ N ) ) ) )
67 bcnn 
 |-  ( N e. NN0 -> ( N _C N ) = 1 )
68 4 67 syl 
 |-  ( ph -> ( N _C N ) = 1 )
69 68 oveq1d 
 |-  ( ph -> ( ( N _C N ) x. ( X ^ N ) ) = ( 1 x. ( X ^ N ) ) )
70 38 mulid2d 
 |-  ( ph -> ( 1 x. ( X ^ N ) ) = ( X ^ N ) )
71 69 70 eqtrd 
 |-  ( ph -> ( ( N _C N ) x. ( X ^ N ) ) = ( X ^ N ) )
72 71 oveq2d 
 |-  ( ph -> ( sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( ( N _C N ) x. ( X ^ N ) ) ) = ( sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( X ^ N ) ) )
73 60 66 72 3eqtrd 
 |-  ( ph -> ( ( X + 1 ) ^ N ) = ( sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( X ^ N ) ) )
74 54 38 73 mvrraddd 
 |-  ( ph -> ( ( ( X + 1 ) ^ N ) - ( X ^ N ) ) = sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) )
75 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
76 1 75 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
77 76 61 eleqtrdi 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` 0 ) )
78 oveq2 
 |-  ( m = ( N - 1 ) -> ( N _C m ) = ( N _C ( N - 1 ) ) )
79 oveq2 
 |-  ( m = ( N - 1 ) -> ( X ^ m ) = ( X ^ ( N - 1 ) ) )
80 78 79 oveq12d 
 |-  ( m = ( N - 1 ) -> ( ( N _C m ) x. ( X ^ m ) ) = ( ( N _C ( N - 1 ) ) x. ( X ^ ( N - 1 ) ) ) )
81 77 53 80 fsumm1 
 |-  ( ph -> sum_ m e. ( 0 ... ( N - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) = ( sum_ m e. ( 0 ... ( ( N - 1 ) - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( ( N _C ( N - 1 ) ) x. ( X ^ ( N - 1 ) ) ) ) )
82 1cnd 
 |-  ( ph -> 1 e. CC )
83 22 82 82 subsub4d 
 |-  ( ph -> ( ( N - 1 ) - 1 ) = ( N - ( 1 + 1 ) ) )
84 df-2 
 |-  2 = ( 1 + 1 )
85 84 oveq2i 
 |-  ( N - 2 ) = ( N - ( 1 + 1 ) )
86 83 85 eqtr4di 
 |-  ( ph -> ( ( N - 1 ) - 1 ) = ( N - 2 ) )
87 86 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N - 1 ) - 1 ) ) = ( 0 ... ( N - 2 ) ) )
88 87 sumeq1d 
 |-  ( ph -> sum_ m e. ( 0 ... ( ( N - 1 ) - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) = sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) )
89 bcnm1 
 |-  ( N e. NN0 -> ( N _C ( N - 1 ) ) = N )
90 4 89 syl 
 |-  ( ph -> ( N _C ( N - 1 ) ) = N )
91 90 oveq1d 
 |-  ( ph -> ( ( N _C ( N - 1 ) ) x. ( X ^ ( N - 1 ) ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )
92 88 91 oveq12d 
 |-  ( ph -> ( sum_ m e. ( 0 ... ( ( N - 1 ) - 1 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( ( N _C ( N - 1 ) ) x. ( X ^ ( N - 1 ) ) ) ) = ( sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( N x. ( X ^ ( N - 1 ) ) ) ) )
93 74 81 92 3eqtrd 
 |-  ( ph -> ( ( ( X + 1 ) ^ N ) - ( X ^ N ) ) = ( sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( N x. ( X ^ ( N - 1 ) ) ) ) )
94 oveq2 
 |-  ( k = 0 -> ( N _C k ) = ( N _C 0 ) )
95 oveq1 
 |-  ( k = 0 -> ( k BernPoly ( X + 1 ) ) = ( 0 BernPoly ( X + 1 ) ) )
96 oveq2 
 |-  ( k = 0 -> ( N - k ) = ( N - 0 ) )
97 96 oveq1d 
 |-  ( k = 0 -> ( ( N - k ) + 1 ) = ( ( N - 0 ) + 1 ) )
98 95 97 oveq12d 
 |-  ( k = 0 -> ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) = ( ( 0 BernPoly ( X + 1 ) ) / ( ( N - 0 ) + 1 ) ) )
99 94 98 oveq12d 
 |-  ( k = 0 -> ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) = ( ( N _C 0 ) x. ( ( 0 BernPoly ( X + 1 ) ) / ( ( N - 0 ) + 1 ) ) ) )
100 77 36 99 fsum1p 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) = ( ( ( N _C 0 ) x. ( ( 0 BernPoly ( X + 1 ) ) / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) )
101 bpoly0 
 |-  ( ( X + 1 ) e. CC -> ( 0 BernPoly ( X + 1 ) ) = 1 )
102 6 101 syl 
 |-  ( ph -> ( 0 BernPoly ( X + 1 ) ) = 1 )
103 102 oveq1d 
 |-  ( ph -> ( ( 0 BernPoly ( X + 1 ) ) / ( ( N - 0 ) + 1 ) ) = ( 1 / ( ( N - 0 ) + 1 ) ) )
104 103 oveq2d 
 |-  ( ph -> ( ( N _C 0 ) x. ( ( 0 BernPoly ( X + 1 ) ) / ( ( N - 0 ) + 1 ) ) ) = ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) )
105 104 oveq1d 
 |-  ( ph -> ( ( ( N _C 0 ) x. ( ( 0 BernPoly ( X + 1 ) ) / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) = ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) )
106 100 105 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) = ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) )
107 oveq1 
 |-  ( k = 0 -> ( k BernPoly X ) = ( 0 BernPoly X ) )
108 107 97 oveq12d 
 |-  ( k = 0 -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) = ( ( 0 BernPoly X ) / ( ( N - 0 ) + 1 ) ) )
109 94 108 oveq12d 
 |-  ( k = 0 -> ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( ( N _C 0 ) x. ( ( 0 BernPoly X ) / ( ( N - 0 ) + 1 ) ) ) )
110 77 42 109 fsum1p 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( ( ( N _C 0 ) x. ( ( 0 BernPoly X ) / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
111 bpoly0 
 |-  ( X e. CC -> ( 0 BernPoly X ) = 1 )
112 2 111 syl 
 |-  ( ph -> ( 0 BernPoly X ) = 1 )
113 112 oveq1d 
 |-  ( ph -> ( ( 0 BernPoly X ) / ( ( N - 0 ) + 1 ) ) = ( 1 / ( ( N - 0 ) + 1 ) ) )
114 113 oveq2d 
 |-  ( ph -> ( ( N _C 0 ) x. ( ( 0 BernPoly X ) / ( ( N - 0 ) + 1 ) ) ) = ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) )
115 114 oveq1d 
 |-  ( ph -> ( ( ( N _C 0 ) x. ( ( 0 BernPoly X ) / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
116 110 115 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
117 106 116 oveq12d 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) - ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) )
118 0z 
 |-  0 e. ZZ
119 bccl 
 |-  ( ( N e. NN0 /\ 0 e. ZZ ) -> ( N _C 0 ) e. NN0 )
120 4 118 119 sylancl 
 |-  ( ph -> ( N _C 0 ) e. NN0 )
121 120 nn0cnd 
 |-  ( ph -> ( N _C 0 ) e. CC )
122 22 subid1d 
 |-  ( ph -> ( N - 0 ) = N )
123 122 1 eqeltrd 
 |-  ( ph -> ( N - 0 ) e. NN )
124 123 peano2nnd 
 |-  ( ph -> ( ( N - 0 ) + 1 ) e. NN )
125 124 nnrecred 
 |-  ( ph -> ( 1 / ( ( N - 0 ) + 1 ) ) e. RR )
126 125 recnd 
 |-  ( ph -> ( 1 / ( ( N - 0 ) + 1 ) ) e. CC )
127 121 126 mulcld 
 |-  ( ph -> ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) e. CC )
128 fzfid 
 |-  ( ph -> ( ( 0 + 1 ) ... ( N - 1 ) ) e. Fin )
129 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... ( N - 1 ) ) C_ ( 0 ... ( N - 1 ) ) )
130 118 129 ax-mp 
 |-  ( ( 0 + 1 ) ... ( N - 1 ) ) C_ ( 0 ... ( N - 1 ) )
131 130 sseli 
 |-  ( k e. ( ( 0 + 1 ) ... ( N - 1 ) ) -> k e. ( 0 ... ( N - 1 ) ) )
132 131 36 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) e. CC )
133 128 132 fsumcl 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) e. CC )
134 131 42 sylan2 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
135 128 134 fsumcl 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
136 127 133 135 pnpcand 
 |-  ( ph -> ( ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) ) - ( ( ( N _C 0 ) x. ( 1 / ( ( N - 0 ) + 1 ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) = ( sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
137 1zzd 
 |-  ( ph -> 1 e. ZZ )
138 0zd 
 |-  ( ph -> 0 e. ZZ )
139 1 nnzd 
 |-  ( ph -> N e. ZZ )
140 2z 
 |-  2 e. ZZ
141 zsubcl 
 |-  ( ( N e. ZZ /\ 2 e. ZZ ) -> ( N - 2 ) e. ZZ )
142 139 140 141 sylancl 
 |-  ( ph -> ( N - 2 ) e. ZZ )
143 fzssp1 
 |-  ( 0 ... ( N - 2 ) ) C_ ( 0 ... ( ( N - 2 ) + 1 ) )
144 2m1e1 
 |-  ( 2 - 1 ) = 1
145 144 oveq2i 
 |-  ( N - ( 2 - 1 ) ) = ( N - 1 )
146 2cnd 
 |-  ( ph -> 2 e. CC )
147 22 146 82 subsubd 
 |-  ( ph -> ( N - ( 2 - 1 ) ) = ( ( N - 2 ) + 1 ) )
148 145 147 syl5reqr 
 |-  ( ph -> ( ( N - 2 ) + 1 ) = ( N - 1 ) )
149 148 oveq2d 
 |-  ( ph -> ( 0 ... ( ( N - 2 ) + 1 ) ) = ( 0 ... ( N - 1 ) ) )
150 143 149 sseqtrid 
 |-  ( ph -> ( 0 ... ( N - 2 ) ) C_ ( 0 ... ( N - 1 ) ) )
151 150 sselda 
 |-  ( ( ph /\ m e. ( 0 ... ( N - 2 ) ) ) -> m e. ( 0 ... ( N - 1 ) ) )
152 151 53 syldan 
 |-  ( ( ph /\ m e. ( 0 ... ( N - 2 ) ) ) -> ( ( N _C m ) x. ( X ^ m ) ) e. CC )
153 oveq2 
 |-  ( m = ( k - 1 ) -> ( N _C m ) = ( N _C ( k - 1 ) ) )
154 oveq2 
 |-  ( m = ( k - 1 ) -> ( X ^ m ) = ( X ^ ( k - 1 ) ) )
155 153 154 oveq12d 
 |-  ( m = ( k - 1 ) -> ( ( N _C m ) x. ( X ^ m ) ) = ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
156 137 138 142 152 155 fsumshft 
 |-  ( ph -> sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) = sum_ k e. ( ( 0 + 1 ) ... ( ( N - 2 ) + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
157 148 oveq2d 
 |-  ( ph -> ( ( 0 + 1 ) ... ( ( N - 2 ) + 1 ) ) = ( ( 0 + 1 ) ... ( N - 1 ) ) )
158 157 sumeq1d 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( ( N - 2 ) + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
159 156 158 eqtrd 
 |-  ( ph -> sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
160 0p1e1 
 |-  ( 0 + 1 ) = 1
161 160 oveq1i 
 |-  ( ( 0 + 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
162 161 eleq2i 
 |-  ( k e. ( ( 0 + 1 ) ... ( N - 1 ) ) <-> k e. ( 1 ... ( N - 1 ) ) )
163 fzssp1 
 |-  ( 1 ... ( N - 1 ) ) C_ ( 1 ... ( ( N - 1 ) + 1 ) )
164 25 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N - 1 ) + 1 ) ) = ( 1 ... N ) )
165 163 164 sseqtrid 
 |-  ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
166 165 sselda 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. ( 1 ... N ) )
167 bcm1k 
 |-  ( k e. ( 1 ... N ) -> ( N _C k ) = ( ( N _C ( k - 1 ) ) x. ( ( N - ( k - 1 ) ) / k ) ) )
168 166 167 syl 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( N _C k ) = ( ( N _C ( k - 1 ) ) x. ( ( N - ( k - 1 ) ) / k ) ) )
169 1 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> N e. NN )
170 169 nncnd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> N e. CC )
171 elfznn 
 |-  ( k e. ( 1 ... ( N - 1 ) ) -> k e. NN )
172 171 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. NN )
173 172 nncnd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> k e. CC )
174 1cnd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> 1 e. CC )
175 170 173 174 subsubd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( N - ( k - 1 ) ) = ( ( N - k ) + 1 ) )
176 175 oveq1d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N - ( k - 1 ) ) / k ) = ( ( ( N - k ) + 1 ) / k ) )
177 176 oveq2d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( N - ( k - 1 ) ) / k ) ) = ( ( N _C ( k - 1 ) ) x. ( ( ( N - k ) + 1 ) / k ) ) )
178 168 177 eqtrd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( N _C k ) = ( ( N _C ( k - 1 ) ) x. ( ( ( N - k ) + 1 ) / k ) ) )
179 3 oveq1d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) / ( ( N - k ) + 1 ) ) = ( ( k x. ( X ^ ( k - 1 ) ) ) / ( ( N - k ) + 1 ) ) )
180 162 131 sylbir 
 |-  ( k e. ( 1 ... ( N - 1 ) ) -> k e. ( 0 ... ( N - 1 ) ) )
181 180 20 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( k BernPoly ( X + 1 ) ) e. CC )
182 180 40 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( k BernPoly X ) e. CC )
183 180 33 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N - k ) + 1 ) e. CC )
184 180 34 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N - k ) + 1 ) =/= 0 )
185 181 182 183 184 divsubdird 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) / ( ( N - k ) + 1 ) ) = ( ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) - ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) )
186 2 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> X e. CC )
187 nnm1nn0 
 |-  ( k e. NN -> ( k - 1 ) e. NN0 )
188 172 187 syl 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( k - 1 ) e. NN0 )
189 186 188 expcld 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( X ^ ( k - 1 ) ) e. CC )
190 173 189 183 184 div23d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k x. ( X ^ ( k - 1 ) ) ) / ( ( N - k ) + 1 ) ) = ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
191 179 185 190 3eqtr3d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) - ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
192 178 191 oveq12d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) - ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( ( N - k ) + 1 ) / k ) ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) )
193 180 17 sylan2 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( N _C k ) e. CC )
194 181 183 184 divcld 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) e. CC )
195 182 183 184 divcld 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) e. CC )
196 193 194 195 subdid 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) - ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
197 169 nnnn0d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> N e. NN0 )
198 188 nn0zd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( k - 1 ) e. ZZ )
199 bccl 
 |-  ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
200 197 198 199 syl2anc 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
201 200 nn0cnd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( N _C ( k - 1 ) ) e. CC )
202 172 nnne0d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> k =/= 0 )
203 183 173 202 divcld 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( N - k ) + 1 ) / k ) e. CC )
204 173 183 184 divcld 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( k / ( ( N - k ) + 1 ) ) e. CC )
205 204 189 mulcld 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) e. CC )
206 201 203 205 mulassd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( ( N - k ) + 1 ) / k ) ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( ( ( N - k ) + 1 ) / k ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) ) )
207 183 173 184 202 divcan6d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( ( N - k ) + 1 ) / k ) x. ( k / ( ( N - k ) + 1 ) ) ) = 1 )
208 207 oveq1d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( ( ( N - k ) + 1 ) / k ) x. ( k / ( ( N - k ) + 1 ) ) ) x. ( X ^ ( k - 1 ) ) ) = ( 1 x. ( X ^ ( k - 1 ) ) ) )
209 203 204 189 mulassd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( ( ( N - k ) + 1 ) / k ) x. ( k / ( ( N - k ) + 1 ) ) ) x. ( X ^ ( k - 1 ) ) ) = ( ( ( ( N - k ) + 1 ) / k ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) )
210 189 mulid2d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( 1 x. ( X ^ ( k - 1 ) ) ) = ( X ^ ( k - 1 ) ) )
211 208 209 210 3eqtr3d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( ( N - k ) + 1 ) / k ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) = ( X ^ ( k - 1 ) ) )
212 211 oveq2d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( ( ( N - k ) + 1 ) / k ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
213 206 212 eqtrd 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( ( N - k ) + 1 ) / k ) ) x. ( ( k / ( ( N - k ) + 1 ) ) x. ( X ^ ( k - 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
214 192 196 213 3eqtr3d 
 |-  ( ( ph /\ k e. ( 1 ... ( N - 1 ) ) ) -> ( ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
215 162 214 sylan2b 
 |-  ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ) -> ( ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
216 215 sumeq2dv 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C ( k - 1 ) ) x. ( X ^ ( k - 1 ) ) ) )
217 128 132 134 fsumsub 
 |-  ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
218 159 216 217 3eqtr2rd 
 |-  ( ph -> ( sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( ( 0 + 1 ) ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) )
219 117 136 218 3eqtrd 
 |-  ( ph -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) )
220 93 219 oveq12d 
 |-  ( ph -> ( ( ( ( X + 1 ) ^ N ) - ( X ^ N ) ) - ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) = ( ( sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( N x. ( X ^ ( N - 1 ) ) ) ) - sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) ) )
221 fzfid 
 |-  ( ph -> ( 0 ... ( N - 2 ) ) e. Fin )
222 221 152 fsumcl 
 |-  ( ph -> sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) e. CC )
223 2 76 expcld 
 |-  ( ph -> ( X ^ ( N - 1 ) ) e. CC )
224 22 223 mulcld 
 |-  ( ph -> ( N x. ( X ^ ( N - 1 ) ) ) e. CC )
225 222 224 pncan2d 
 |-  ( ph -> ( ( sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) + ( N x. ( X ^ ( N - 1 ) ) ) ) - sum_ m e. ( 0 ... ( N - 2 ) ) ( ( N _C m ) x. ( X ^ m ) ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )
226 220 225 eqtrd 
 |-  ( ph -> ( ( ( ( X + 1 ) ^ N ) - ( X ^ N ) ) - ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly ( X + 1 ) ) / ( ( N - k ) + 1 ) ) ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )
227 11 44 226 3eqtrd 
 |-  ( ph -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )