Metamath Proof Explorer

Theorem bpoly3

Description: The Bernoulli polynomials at three. (Contributed by Scott Fenton, 8-Jul-2015)

Ref Expression
Assertion bpoly3 
|- ( X e. CC -> ( 3 BernPoly X ) = ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) )

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 bpolyval 
 |-  ( ( 3 e. NN0 /\ X e. CC ) -> ( 3 BernPoly X ) = ( ( X ^ 3 ) - sum_ k e. ( 0 ... ( 3 - 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) ) )
3 1 2 mpan 
 |-  ( X e. CC -> ( 3 BernPoly X ) = ( ( X ^ 3 ) - sum_ k e. ( 0 ... ( 3 - 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) ) )
4 3m1e2 
 |-  ( 3 - 1 ) = 2
5 df-2 
 |-  2 = ( 1 + 1 )
6 4 5 eqtri 
 |-  ( 3 - 1 ) = ( 1 + 1 )
7 6 oveq2i 
 |-  ( 0 ... ( 3 - 1 ) ) = ( 0 ... ( 1 + 1 ) )
8 7 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 3 - 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... ( 1 + 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) )
9 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
10 9 a1i 
 |-  ( X e. CC -> 1 e. ( ZZ>= ` 0 ) )
11 0z 
 |-  0 e. ZZ
12 fzpr 
 |-  ( 0 e. ZZ -> ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) } )
13 11 12 ax-mp 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , ( 0 + 1 ) }
14 0p1e1 
 |-  ( 0 + 1 ) = 1
15 14 oveq2i 
 |-  ( 0 ... ( 0 + 1 ) ) = ( 0 ... 1 )
16 14 preq2i 
 |-  { 0 , ( 0 + 1 ) } = { 0 , 1 }
17 13 15 16 3eqtr3ri 
 |-  { 0 , 1 } = ( 0 ... 1 )
18 5 sneqi 
 |-  { 2 } = { ( 1 + 1 ) }
19 17 18 uneq12i 
 |-  ( { 0 , 1 } u. { 2 } ) = ( ( 0 ... 1 ) u. { ( 1 + 1 ) } )
20 df-tp 
 |-  { 0 , 1 , 2 } = ( { 0 , 1 } u. { 2 } )
21 fzsuc 
 |-  ( 1 e. ( ZZ>= ` 0 ) -> ( 0 ... ( 1 + 1 ) ) = ( ( 0 ... 1 ) u. { ( 1 + 1 ) } ) )
22 9 21 ax-mp 
 |-  ( 0 ... ( 1 + 1 ) ) = ( ( 0 ... 1 ) u. { ( 1 + 1 ) } )
23 19 20 22 3eqtr4ri 
 |-  ( 0 ... ( 1 + 1 ) ) = { 0 , 1 , 2 }
24 23 eleq2i 
 |-  ( k e. ( 0 ... ( 1 + 1 ) ) <-> k e. { 0 , 1 , 2 } )
25 vex 
 |-  k e. _V
26 25 eltp 
 |-  ( k e. { 0 , 1 , 2 } <-> ( k = 0 \/ k = 1 \/ k = 2 ) )
27 24 26 bitri 
 |-  ( k e. ( 0 ... ( 1 + 1 ) ) <-> ( k = 0 \/ k = 1 \/ k = 2 ) )
28 oveq2 
 |-  ( k = 0 -> ( 3 _C k ) = ( 3 _C 0 ) )
29 bcn0 
 |-  ( 3 e. NN0 -> ( 3 _C 0 ) = 1 )
30 1 29 ax-mp 
 |-  ( 3 _C 0 ) = 1
31 28 30 eqtrdi 
 |-  ( k = 0 -> ( 3 _C k ) = 1 )
32 oveq1 
 |-  ( k = 0 -> ( k BernPoly X ) = ( 0 BernPoly X ) )
33 oveq2 
 |-  ( k = 0 -> ( 3 - k ) = ( 3 - 0 ) )
34 33 oveq1d 
 |-  ( k = 0 -> ( ( 3 - k ) + 1 ) = ( ( 3 - 0 ) + 1 ) )
35 3cn 
 |-  3 e. CC
36 35 subid1i 
 |-  ( 3 - 0 ) = 3
37 36 oveq1i 
 |-  ( ( 3 - 0 ) + 1 ) = ( 3 + 1 )
38 df-4 
 |-  4 = ( 3 + 1 )
39 37 38 eqtr4i 
 |-  ( ( 3 - 0 ) + 1 ) = 4
40 34 39 eqtrdi 
 |-  ( k = 0 -> ( ( 3 - k ) + 1 ) = 4 )
41 32 40 oveq12d 
 |-  ( k = 0 -> ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) = ( ( 0 BernPoly X ) / 4 ) )
42 31 41 oveq12d 
 |-  ( k = 0 -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) )
43 bpoly0 
 |-  ( X e. CC -> ( 0 BernPoly X ) = 1 )
44 43 oveq1d 
 |-  ( X e. CC -> ( ( 0 BernPoly X ) / 4 ) = ( 1 / 4 ) )
45 44 oveq2d 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) = ( 1 x. ( 1 / 4 ) ) )
46 4cn 
 |-  4 e. CC
47 4ne0 
 |-  4 =/= 0
48 46 47 reccli 
 |-  ( 1 / 4 ) e. CC
49 48 mulid2i 
 |-  ( 1 x. ( 1 / 4 ) ) = ( 1 / 4 )
50 45 49 eqtrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) = ( 1 / 4 ) )
51 42 50 sylan9eqr 
 |-  ( ( X e. CC /\ k = 0 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 1 / 4 ) )
52 51 48 eqeltrdi 
 |-  ( ( X e. CC /\ k = 0 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
53 oveq2 
 |-  ( k = 1 -> ( 3 _C k ) = ( 3 _C 1 ) )
54 bcn1 
 |-  ( 3 e. NN0 -> ( 3 _C 1 ) = 3 )
55 1 54 ax-mp 
 |-  ( 3 _C 1 ) = 3
56 53 55 eqtrdi 
 |-  ( k = 1 -> ( 3 _C k ) = 3 )
57 oveq1 
 |-  ( k = 1 -> ( k BernPoly X ) = ( 1 BernPoly X ) )
58 oveq2 
 |-  ( k = 1 -> ( 3 - k ) = ( 3 - 1 ) )
59 58 oveq1d 
 |-  ( k = 1 -> ( ( 3 - k ) + 1 ) = ( ( 3 - 1 ) + 1 ) )
60 ax-1cn 
 |-  1 e. CC
61 npcan 
 |-  ( ( 3 e. CC /\ 1 e. CC ) -> ( ( 3 - 1 ) + 1 ) = 3 )
62 35 60 61 mp2an 
 |-  ( ( 3 - 1 ) + 1 ) = 3
63 59 62 eqtrdi 
 |-  ( k = 1 -> ( ( 3 - k ) + 1 ) = 3 )
64 57 63 oveq12d 
 |-  ( k = 1 -> ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) = ( ( 1 BernPoly X ) / 3 ) )
65 56 64 oveq12d 
 |-  ( k = 1 -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 3 x. ( ( 1 BernPoly X ) / 3 ) ) )
66 bpoly1 
 |-  ( X e. CC -> ( 1 BernPoly X ) = ( X - ( 1 / 2 ) ) )
67 66 oveq1d 
 |-  ( X e. CC -> ( ( 1 BernPoly X ) / 3 ) = ( ( X - ( 1 / 2 ) ) / 3 ) )
68 67 oveq2d 
 |-  ( X e. CC -> ( 3 x. ( ( 1 BernPoly X ) / 3 ) ) = ( 3 x. ( ( X - ( 1 / 2 ) ) / 3 ) ) )
69 halfcn 
 |-  ( 1 / 2 ) e. CC
70 subcl 
 |-  ( ( X e. CC /\ ( 1 / 2 ) e. CC ) -> ( X - ( 1 / 2 ) ) e. CC )
71 69 70 mpan2 
 |-  ( X e. CC -> ( X - ( 1 / 2 ) ) e. CC )
72 3ne0 
 |-  3 =/= 0
73 divcan2 
 |-  ( ( ( X - ( 1 / 2 ) ) e. CC /\ 3 e. CC /\ 3 =/= 0 ) -> ( 3 x. ( ( X - ( 1 / 2 ) ) / 3 ) ) = ( X - ( 1 / 2 ) ) )
74 35 72 73 mp3an23 
 |-  ( ( X - ( 1 / 2 ) ) e. CC -> ( 3 x. ( ( X - ( 1 / 2 ) ) / 3 ) ) = ( X - ( 1 / 2 ) ) )
75 71 74 syl 
 |-  ( X e. CC -> ( 3 x. ( ( X - ( 1 / 2 ) ) / 3 ) ) = ( X - ( 1 / 2 ) ) )
76 68 75 eqtrd 
 |-  ( X e. CC -> ( 3 x. ( ( 1 BernPoly X ) / 3 ) ) = ( X - ( 1 / 2 ) ) )
77 65 76 sylan9eqr 
 |-  ( ( X e. CC /\ k = 1 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( X - ( 1 / 2 ) ) )
78 71 adantr 
 |-  ( ( X e. CC /\ k = 1 ) -> ( X - ( 1 / 2 ) ) e. CC )
79 77 78 eqeltrd 
 |-  ( ( X e. CC /\ k = 1 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
80 oveq2 
 |-  ( k = 2 -> ( 3 _C k ) = ( 3 _C 2 ) )
81 bcn2 
 |-  ( 3 e. NN0 -> ( 3 _C 2 ) = ( ( 3 x. ( 3 - 1 ) ) / 2 ) )
82 1 81 ax-mp 
 |-  ( 3 _C 2 ) = ( ( 3 x. ( 3 - 1 ) ) / 2 )
83 4 oveq2i 
 |-  ( 3 x. ( 3 - 1 ) ) = ( 3 x. 2 )
84 83 oveq1i 
 |-  ( ( 3 x. ( 3 - 1 ) ) / 2 ) = ( ( 3 x. 2 ) / 2 )
85 2cn 
 |-  2 e. CC
86 2ne0 
 |-  2 =/= 0
87 35 85 86 divcan4i 
 |-  ( ( 3 x. 2 ) / 2 ) = 3
88 84 87 eqtri 
 |-  ( ( 3 x. ( 3 - 1 ) ) / 2 ) = 3
89 82 88 eqtri 
 |-  ( 3 _C 2 ) = 3
90 80 89 eqtrdi 
 |-  ( k = 2 -> ( 3 _C k ) = 3 )
91 oveq1 
 |-  ( k = 2 -> ( k BernPoly X ) = ( 2 BernPoly X ) )
92 oveq2 
 |-  ( k = 2 -> ( 3 - k ) = ( 3 - 2 ) )
93 92 oveq1d 
 |-  ( k = 2 -> ( ( 3 - k ) + 1 ) = ( ( 3 - 2 ) + 1 ) )
94 2p1e3 
 |-  ( 2 + 1 ) = 3
95 35 85 60 94 subaddrii 
 |-  ( 3 - 2 ) = 1
96 95 oveq1i 
 |-  ( ( 3 - 2 ) + 1 ) = ( 1 + 1 )
97 96 5 eqtr4i 
 |-  ( ( 3 - 2 ) + 1 ) = 2
98 93 97 eqtrdi 
 |-  ( k = 2 -> ( ( 3 - k ) + 1 ) = 2 )
99 91 98 oveq12d 
 |-  ( k = 2 -> ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) = ( ( 2 BernPoly X ) / 2 ) )
100 90 99 oveq12d 
 |-  ( k = 2 -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) )
101 2nn0 
 |-  2 e. NN0
102 bpolycl 
 |-  ( ( 2 e. NN0 /\ X e. CC ) -> ( 2 BernPoly X ) e. CC )
103 101 102 mpan 
 |-  ( X e. CC -> ( 2 BernPoly X ) e. CC )
104 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
105 div12 
 |-  ( ( 3 e. CC /\ ( 2 BernPoly X ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) = ( ( 2 BernPoly X ) x. ( 3 / 2 ) ) )
106 35 104 105 mp3an13 
 |-  ( ( 2 BernPoly X ) e. CC -> ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) = ( ( 2 BernPoly X ) x. ( 3 / 2 ) ) )
107 103 106 syl 
 |-  ( X e. CC -> ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) = ( ( 2 BernPoly X ) x. ( 3 / 2 ) ) )
108 35 85 86 divcli 
 |-  ( 3 / 2 ) e. CC
109 mulcom 
 |-  ( ( ( 2 BernPoly X ) e. CC /\ ( 3 / 2 ) e. CC ) -> ( ( 2 BernPoly X ) x. ( 3 / 2 ) ) = ( ( 3 / 2 ) x. ( 2 BernPoly X ) ) )
110 103 108 109 sylancl 
 |-  ( X e. CC -> ( ( 2 BernPoly X ) x. ( 3 / 2 ) ) = ( ( 3 / 2 ) x. ( 2 BernPoly X ) ) )
111 bpoly2 
 |-  ( X e. CC -> ( 2 BernPoly X ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
112 111 oveq2d 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( 2 BernPoly X ) ) = ( ( 3 / 2 ) x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) )
113 sqcl 
 |-  ( X e. CC -> ( X ^ 2 ) e. CC )
114 6cn 
 |-  6 e. CC
115 6re 
 |-  6 e. RR
116 6pos 
 |-  0 < 6
117 115 116 gt0ne0ii 
 |-  6 =/= 0
118 114 117 reccli 
 |-  ( 1 / 6 ) e. CC
119 subsub 
 |-  ( ( ( X ^ 2 ) e. CC /\ X e. CC /\ ( 1 / 6 ) e. CC ) -> ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
120 118 119 mp3an3 
 |-  ( ( ( X ^ 2 ) e. CC /\ X e. CC ) -> ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
121 113 120 mpancom 
 |-  ( X e. CC -> ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
122 121 oveq2d 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) ) = ( ( 3 / 2 ) x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) )
123 subcl 
 |-  ( ( X e. CC /\ ( 1 / 6 ) e. CC ) -> ( X - ( 1 / 6 ) ) e. CC )
124 118 123 mpan2 
 |-  ( X e. CC -> ( X - ( 1 / 6 ) ) e. CC )
125 subdi 
 |-  ( ( ( 3 / 2 ) e. CC /\ ( X ^ 2 ) e. CC /\ ( X - ( 1 / 6 ) ) e. CC ) -> ( ( 3 / 2 ) x. ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) )
126 108 113 124 125 mp3an2i 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( ( X ^ 2 ) - ( X - ( 1 / 6 ) ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) )
127 112 122 126 3eqtr2d 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( 2 BernPoly X ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) )
128 107 110 127 3eqtrd 
 |-  ( X e. CC -> ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) )
129 100 128 sylan9eqr 
 |-  ( ( X e. CC /\ k = 2 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) )
130 mulcl 
 |-  ( ( ( 3 / 2 ) e. CC /\ ( X ^ 2 ) e. CC ) -> ( ( 3 / 2 ) x. ( X ^ 2 ) ) e. CC )
131 108 113 130 sylancr 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( X ^ 2 ) ) e. CC )
132 mulcl 
 |-  ( ( ( 3 / 2 ) e. CC /\ ( X - ( 1 / 6 ) ) e. CC ) -> ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) e. CC )
133 108 124 132 sylancr 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) e. CC )
134 131 133 subcld 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) e. CC )
135 134 adantr 
 |-  ( ( X e. CC /\ k = 2 ) -> ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) e. CC )
136 129 135 eqeltrd 
 |-  ( ( X e. CC /\ k = 2 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
137 52 79 136 3jaodan 
 |-  ( ( X e. CC /\ ( k = 0 \/ k = 1 \/ k = 2 ) ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
138 27 137 sylan2b 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 1 + 1 ) ) ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
139 5 eqeq2i 
 |-  ( k = 2 <-> k = ( 1 + 1 ) )
140 139 100 sylbir 
 |-  ( k = ( 1 + 1 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) )
141 10 138 140 fsump1 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 1 + 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) ) )
142 128 oveq2d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( 3 x. ( ( 2 BernPoly X ) / 2 ) ) ) = ( sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) )
143 15 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) )
144 0nn0 
 |-  0 e. NN0
145 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
146 144 145 eleqtri 
 |-  0 e. ( ZZ>= ` 0 )
147 146 a1i 
 |-  ( X e. CC -> 0 e. ( ZZ>= ` 0 ) )
148 13 16 eqtri 
 |-  ( 0 ... ( 0 + 1 ) ) = { 0 , 1 }
149 148 eleq2i 
 |-  ( k e. ( 0 ... ( 0 + 1 ) ) <-> k e. { 0 , 1 } )
150 25 elpr 
 |-  ( k e. { 0 , 1 } <-> ( k = 0 \/ k = 1 ) )
151 149 150 bitri 
 |-  ( k e. ( 0 ... ( 0 + 1 ) ) <-> ( k = 0 \/ k = 1 ) )
152 52 79 jaodan 
 |-  ( ( X e. CC /\ ( k = 0 \/ k = 1 ) ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
153 151 152 sylan2b 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 0 + 1 ) ) ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) e. CC )
154 14 eqeq2i 
 |-  ( k = ( 0 + 1 ) <-> k = 1 )
155 154 65 sylbi 
 |-  ( k = ( 0 + 1 ) -> ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 3 x. ( ( 1 BernPoly X ) / 3 ) ) )
156 147 153 155 fsump1 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... 0 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( 3 x. ( ( 1 BernPoly X ) / 3 ) ) ) )
157 50 48 eqeltrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) e. CC )
158 42 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) )
159 11 157 158 sylancr 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 4 ) ) )
160 159 50 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( 1 / 4 ) )
161 160 76 oveq12d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 0 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( 3 x. ( ( 1 BernPoly X ) / 3 ) ) ) = ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) )
162 156 161 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) )
163 143 162 syl5eqr 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) )
164 163 oveq1d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) )
165 addcl 
 |-  ( ( ( 1 / 4 ) e. CC /\ ( X - ( 1 / 2 ) ) e. CC ) -> ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) e. CC )
166 48 71 165 sylancr 
 |-  ( X e. CC -> ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) e. CC )
167 166 131 133 addsub12d 
 |-  ( X e. CC -> ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) + ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) )
168 164 167 eqtrd 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) + ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) )
169 133 166 negsubdi2d 
 |-  ( X e. CC -> -u ( ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) - ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) ) = ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) )
170 subdi 
 |-  ( ( ( 3 / 2 ) e. CC /\ X e. CC /\ ( 1 / 6 ) e. CC ) -> ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) x. X ) - ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) )
171 108 118 170 mp3an13 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) x. X ) - ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) )
172 addsub12 
 |-  ( ( ( 1 / 4 ) e. CC /\ X e. CC /\ ( 1 / 2 ) e. CC ) -> ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) = ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) )
173 48 69 172 mp3an13 
 |-  ( X e. CC -> ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) = ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) )
174 171 173 oveq12d 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) - ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) ) = ( ( ( ( 3 / 2 ) x. X ) - ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) - ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) ) )
175 mulcl 
 |-  ( ( ( 3 / 2 ) e. CC /\ X e. CC ) -> ( ( 3 / 2 ) x. X ) e. CC )
176 108 175 mpan 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. X ) e. CC )
177 108 118 mulcli 
 |-  ( ( 3 / 2 ) x. ( 1 / 6 ) ) e. CC
178 negsub 
 |-  ( ( ( ( 3 / 2 ) x. X ) e. CC /\ ( ( 3 / 2 ) x. ( 1 / 6 ) ) e. CC ) -> ( ( ( 3 / 2 ) x. X ) + -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) x. X ) - ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) )
179 176 177 178 sylancl 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. X ) + -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) = ( ( ( 3 / 2 ) x. X ) - ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) )
180 179 oveq1d 
 |-  ( X e. CC -> ( ( ( ( 3 / 2 ) x. X ) + -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) - ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) ) = ( ( ( ( 3 / 2 ) x. X ) - ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) - ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) ) )
181 69 48 negsubdi2i 
 |-  -u ( ( 1 / 2 ) - ( 1 / 4 ) ) = ( ( 1 / 4 ) - ( 1 / 2 ) )
182 85 35 85 mul12i 
 |-  ( 2 x. ( 3 x. 2 ) ) = ( 3 x. ( 2 x. 2 ) )
183 3t2e6 
 |-  ( 3 x. 2 ) = 6
184 183 oveq2i 
 |-  ( 2 x. ( 3 x. 2 ) ) = ( 2 x. 6 )
185 2t2e4 
 |-  ( 2 x. 2 ) = 4
186 185 oveq2i 
 |-  ( 3 x. ( 2 x. 2 ) ) = ( 3 x. 4 )
187 182 184 186 3eqtr3i 
 |-  ( 2 x. 6 ) = ( 3 x. 4 )
188 187 oveq2i 
 |-  ( ( 3 x. 1 ) / ( 2 x. 6 ) ) = ( ( 3 x. 1 ) / ( 3 x. 4 ) )
189 46 47 pm3.2i 
 |-  ( 4 e. CC /\ 4 =/= 0 )
190 35 72 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
191 divcan5 
 |-  ( ( 1 e. CC /\ ( 4 e. CC /\ 4 =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 3 x. 1 ) / ( 3 x. 4 ) ) = ( 1 / 4 ) )
192 60 189 190 191 mp3an 
 |-  ( ( 3 x. 1 ) / ( 3 x. 4 ) ) = ( 1 / 4 )
193 188 192 eqtri 
 |-  ( ( 3 x. 1 ) / ( 2 x. 6 ) ) = ( 1 / 4 )
194 35 85 60 114 86 117 divmuldivi 
 |-  ( ( 3 / 2 ) x. ( 1 / 6 ) ) = ( ( 3 x. 1 ) / ( 2 x. 6 ) )
195 2t1e2 
 |-  ( 2 x. 1 ) = 2
196 195 5 eqtri 
 |-  ( 2 x. 1 ) = ( 1 + 1 )
197 196 185 oveq12i 
 |-  ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( ( 1 + 1 ) / 4 )
198 divcan5 
 |-  ( ( 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 ) )
199 60 104 104 198 mp3an 
 |-  ( ( 2 x. 1 ) / ( 2 x. 2 ) ) = ( 1 / 2 )
200 60 60 46 47 divdiri 
 |-  ( ( 1 + 1 ) / 4 ) = ( ( 1 / 4 ) + ( 1 / 4 ) )
201 197 199 200 3eqtr3ri 
 |-  ( ( 1 / 4 ) + ( 1 / 4 ) ) = ( 1 / 2 )
202 69 48 48 201 subaddrii 
 |-  ( ( 1 / 2 ) - ( 1 / 4 ) ) = ( 1 / 4 )
203 193 194 202 3eqtr4ri 
 |-  ( ( 1 / 2 ) - ( 1 / 4 ) ) = ( ( 3 / 2 ) x. ( 1 / 6 ) )
204 203 negeqi 
 |-  -u ( ( 1 / 2 ) - ( 1 / 4 ) ) = -u ( ( 3 / 2 ) x. ( 1 / 6 ) )
205 181 204 eqtr3i 
 |-  ( ( 1 / 4 ) - ( 1 / 2 ) ) = -u ( ( 3 / 2 ) x. ( 1 / 6 ) )
206 48 69 subcli 
 |-  ( ( 1 / 4 ) - ( 1 / 2 ) ) e. CC
207 177 negcli 
 |-  -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) e. CC
208 206 207 subeq0i 
 |-  ( ( ( ( 1 / 4 ) - ( 1 / 2 ) ) - -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) = 0 <-> ( ( 1 / 4 ) - ( 1 / 2 ) ) = -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) )
209 205 208 mpbir 
 |-  ( ( ( 1 / 4 ) - ( 1 / 2 ) ) - -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) = 0
210 209 oveq2i 
 |-  ( ( ( ( 3 / 2 ) x. X ) - X ) - ( ( ( 1 / 4 ) - ( 1 / 2 ) ) - -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) ) = ( ( ( ( 3 / 2 ) x. X ) - X ) - 0 )
211 id 
 |-  ( X e. CC -> X e. CC )
212 206 a1i 
 |-  ( X e. CC -> ( ( 1 / 4 ) - ( 1 / 2 ) ) e. CC )
213 207 a1i 
 |-  ( X e. CC -> -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) e. CC )
214 176 211 212 213 subadd4d 
 |-  ( X e. CC -> ( ( ( ( 3 / 2 ) x. X ) - X ) - ( ( ( 1 / 4 ) - ( 1 / 2 ) ) - -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) ) = ( ( ( ( 3 / 2 ) x. X ) + -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) - ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) ) )
215 subdir 
 |-  ( ( ( 3 / 2 ) e. CC /\ 1 e. CC /\ X e. CC ) -> ( ( ( 3 / 2 ) - 1 ) x. X ) = ( ( ( 3 / 2 ) x. X ) - ( 1 x. X ) ) )
216 108 60 215 mp3an12 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) - 1 ) x. X ) = ( ( ( 3 / 2 ) x. X ) - ( 1 x. X ) ) )
217 divsubdir 
 |-  ( ( 3 e. CC /\ 2 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( 3 - 2 ) / 2 ) = ( ( 3 / 2 ) - ( 2 / 2 ) ) )
218 35 85 104 217 mp3an 
 |-  ( ( 3 - 2 ) / 2 ) = ( ( 3 / 2 ) - ( 2 / 2 ) )
219 95 oveq1i 
 |-  ( ( 3 - 2 ) / 2 ) = ( 1 / 2 )
220 2div2e1 
 |-  ( 2 / 2 ) = 1
221 220 oveq2i 
 |-  ( ( 3 / 2 ) - ( 2 / 2 ) ) = ( ( 3 / 2 ) - 1 )
222 218 219 221 3eqtr3ri 
 |-  ( ( 3 / 2 ) - 1 ) = ( 1 / 2 )
223 222 oveq1i 
 |-  ( ( ( 3 / 2 ) - 1 ) x. X ) = ( ( 1 / 2 ) x. X )
224 223 a1i 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) - 1 ) x. X ) = ( ( 1 / 2 ) x. X ) )
225 mulid2 
 |-  ( X e. CC -> ( 1 x. X ) = X )
226 225 oveq2d 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. X ) - ( 1 x. X ) ) = ( ( ( 3 / 2 ) x. X ) - X ) )
227 216 224 226 3eqtr3rd 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. X ) - X ) = ( ( 1 / 2 ) x. X ) )
228 227 oveq1d 
 |-  ( X e. CC -> ( ( ( ( 3 / 2 ) x. X ) - X ) - 0 ) = ( ( ( 1 / 2 ) x. X ) - 0 ) )
229 mulcl 
 |-  ( ( ( 1 / 2 ) e. CC /\ X e. CC ) -> ( ( 1 / 2 ) x. X ) e. CC )
230 69 229 mpan 
 |-  ( X e. CC -> ( ( 1 / 2 ) x. X ) e. CC )
231 230 subid1d 
 |-  ( X e. CC -> ( ( ( 1 / 2 ) x. X ) - 0 ) = ( ( 1 / 2 ) x. X ) )
232 228 231 eqtrd 
 |-  ( X e. CC -> ( ( ( ( 3 / 2 ) x. X ) - X ) - 0 ) = ( ( 1 / 2 ) x. X ) )
233 210 214 232 3eqtr3a 
 |-  ( X e. CC -> ( ( ( ( 3 / 2 ) x. X ) + -u ( ( 3 / 2 ) x. ( 1 / 6 ) ) ) - ( X + ( ( 1 / 4 ) - ( 1 / 2 ) ) ) ) = ( ( 1 / 2 ) x. X ) )
234 174 180 233 3eqtr2d 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) - ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) ) = ( ( 1 / 2 ) x. X ) )
235 234 negeqd 
 |-  ( X e. CC -> -u ( ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) - ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) ) = -u ( ( 1 / 2 ) x. X ) )
236 169 235 eqtr3d 
 |-  ( X e. CC -> ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) = -u ( ( 1 / 2 ) x. X ) )
237 236 oveq2d 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) + ( ( ( 1 / 4 ) + ( X - ( 1 / 2 ) ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) + -u ( ( 1 / 2 ) x. X ) ) )
238 131 230 negsubd 
 |-  ( X e. CC -> ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) + -u ( ( 1 / 2 ) x. X ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 1 / 2 ) x. X ) ) )
239 168 237 238 3eqtrd 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 1 ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) + ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 3 / 2 ) x. ( X - ( 1 / 6 ) ) ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 1 / 2 ) x. X ) ) )
240 141 142 239 3eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 1 + 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 1 / 2 ) x. X ) ) )
241 8 240 syl5eq 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 3 - 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) = ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 1 / 2 ) x. X ) ) )
242 241 oveq2d 
 |-  ( X e. CC -> ( ( X ^ 3 ) - sum_ k e. ( 0 ... ( 3 - 1 ) ) ( ( 3 _C k ) x. ( ( k BernPoly X ) / ( ( 3 - k ) + 1 ) ) ) ) = ( ( X ^ 3 ) - ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 1 / 2 ) x. X ) ) ) )
243 expcl 
 |-  ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
244 1 243 mpan2 
 |-  ( X e. CC -> ( X ^ 3 ) e. CC )
245 244 131 230 subsubd 
 |-  ( X e. CC -> ( ( X ^ 3 ) - ( ( ( 3 / 2 ) x. ( X ^ 2 ) ) - ( ( 1 / 2 ) x. X ) ) ) = ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) )
246 3 242 245 3eqtrd 
 |-  ( X e. CC -> ( 3 BernPoly X ) = ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) )