Metamath Proof Explorer

Theorem bpoly4

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

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

Proof

Step Hyp Ref Expression
1 4nn0 
 |-  4 e. NN0
2 bpolyval 
 |-  ( ( 4 e. NN0 /\ X e. CC ) -> ( 4 BernPoly X ) = ( ( X ^ 4 ) - sum_ k e. ( 0 ... ( 4 - 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) ) )
3 1 2 mpan 
 |-  ( X e. CC -> ( 4 BernPoly X ) = ( ( X ^ 4 ) - sum_ k e. ( 0 ... ( 4 - 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) ) )
4 4m1e3 
 |-  ( 4 - 1 ) = 3
5 df-3 
 |-  3 = ( 2 + 1 )
6 4 5 eqtri 
 |-  ( 4 - 1 ) = ( 2 + 1 )
7 6 oveq2i 
 |-  ( 0 ... ( 4 - 1 ) ) = ( 0 ... ( 2 + 1 ) )
8 7 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 4 - 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... ( 2 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) )
9 2eluzge0 
 |-  2 e. ( ZZ>= ` 0 )
10 9 a1i 
 |-  ( X e. CC -> 2 e. ( ZZ>= ` 0 ) )
11 elfzelz 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> k e. ZZ )
12 bccl 
 |-  ( ( 4 e. NN0 /\ k e. ZZ ) -> ( 4 _C k ) e. NN0 )
13 1 11 12 sylancr 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( 4 _C k ) e. NN0 )
14 13 nn0cnd 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( 4 _C k ) e. CC )
15 14 adantl 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 2 + 1 ) ) ) -> ( 4 _C k ) e. CC )
16 elfznn0 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> k e. NN0 )
17 bpolycl 
 |-  ( ( k e. NN0 /\ X e. CC ) -> ( k BernPoly X ) e. CC )
18 16 17 sylan 
 |-  ( ( k e. ( 0 ... ( 2 + 1 ) ) /\ X e. CC ) -> ( k BernPoly X ) e. CC )
19 18 ancoms 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 2 + 1 ) ) ) -> ( k BernPoly X ) e. CC )
20 4re 
 |-  4 e. RR
21 20 a1i 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> 4 e. RR )
22 11 zred 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> k e. RR )
23 21 22 resubcld 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( 4 - k ) e. RR )
24 peano2re 
 |-  ( ( 4 - k ) e. RR -> ( ( 4 - k ) + 1 ) e. RR )
25 23 24 syl 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( ( 4 - k ) + 1 ) e. RR )
26 25 recnd 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( ( 4 - k ) + 1 ) e. CC )
27 26 adantl 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 2 + 1 ) ) ) -> ( ( 4 - k ) + 1 ) e. CC )
28 1red 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> 1 e. RR )
29 5 oveq2i 
 |-  ( 0 ... 3 ) = ( 0 ... ( 2 + 1 ) )
30 29 eleq2i 
 |-  ( k e. ( 0 ... 3 ) <-> k e. ( 0 ... ( 2 + 1 ) ) )
31 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
32 31 zred 
 |-  ( k e. ( 0 ... 3 ) -> k e. RR )
33 3re 
 |-  3 e. RR
34 33 a1i 
 |-  ( k e. ( 0 ... 3 ) -> 3 e. RR )
35 20 a1i 
 |-  ( k e. ( 0 ... 3 ) -> 4 e. RR )
36 elfzle2 
 |-  ( k e. ( 0 ... 3 ) -> k <_ 3 )
37 3lt4 
 |-  3 < 4
38 37 a1i 
 |-  ( k e. ( 0 ... 3 ) -> 3 < 4 )
39 32 34 35 36 38 lelttrd 
 |-  ( k e. ( 0 ... 3 ) -> k < 4 )
40 30 39 sylbir 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> k < 4 )
41 22 21 posdifd 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( k < 4 <-> 0 < ( 4 - k ) ) )
42 40 41 mpbid 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> 0 < ( 4 - k ) )
43 0lt1 
 |-  0 < 1
44 43 a1i 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> 0 < 1 )
45 23 28 42 44 addgt0d 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> 0 < ( ( 4 - k ) + 1 ) )
46 45 gt0ne0d 
 |-  ( k e. ( 0 ... ( 2 + 1 ) ) -> ( ( 4 - k ) + 1 ) =/= 0 )
47 46 adantl 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 2 + 1 ) ) ) -> ( ( 4 - k ) + 1 ) =/= 0 )
48 19 27 47 divcld 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 2 + 1 ) ) ) -> ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) e. CC )
49 15 48 mulcld 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 2 + 1 ) ) ) -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) e. CC )
50 5 eqeq2i 
 |-  ( k = 3 <-> k = ( 2 + 1 ) )
51 oveq2 
 |-  ( k = 3 -> ( 4 _C k ) = ( 4 _C 3 ) )
52 4bc3eq4 
 |-  ( 4 _C 3 ) = 4
53 51 52 eqtrdi 
 |-  ( k = 3 -> ( 4 _C k ) = 4 )
54 oveq1 
 |-  ( k = 3 -> ( k BernPoly X ) = ( 3 BernPoly X ) )
55 oveq2 
 |-  ( k = 3 -> ( 4 - k ) = ( 4 - 3 ) )
56 55 oveq1d 
 |-  ( k = 3 -> ( ( 4 - k ) + 1 ) = ( ( 4 - 3 ) + 1 ) )
57 4cn 
 |-  4 e. CC
58 3cn 
 |-  3 e. CC
59 ax-1cn 
 |-  1 e. CC
60 3p1e4 
 |-  ( 3 + 1 ) = 4
61 57 58 59 60 subaddrii 
 |-  ( 4 - 3 ) = 1
62 61 oveq1i 
 |-  ( ( 4 - 3 ) + 1 ) = ( 1 + 1 )
63 df-2 
 |-  2 = ( 1 + 1 )
64 62 63 eqtr4i 
 |-  ( ( 4 - 3 ) + 1 ) = 2
65 56 64 eqtrdi 
 |-  ( k = 3 -> ( ( 4 - k ) + 1 ) = 2 )
66 54 65 oveq12d 
 |-  ( k = 3 -> ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) = ( ( 3 BernPoly X ) / 2 ) )
67 53 66 oveq12d 
 |-  ( k = 3 -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 4 x. ( ( 3 BernPoly X ) / 2 ) ) )
68 50 67 sylbir 
 |-  ( k = ( 2 + 1 ) -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 4 x. ( ( 3 BernPoly X ) / 2 ) ) )
69 10 49 68 fsump1 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 2 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... 2 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) + ( 4 x. ( ( 3 BernPoly X ) / 2 ) ) ) )
70 63 oveq2i 
 |-  ( 0 ... 2 ) = ( 0 ... ( 1 + 1 ) )
71 70 sumeq1i 
 |-  sum_ k e. ( 0 ... 2 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... ( 1 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) )
72 1eluzge0 
 |-  1 e. ( ZZ>= ` 0 )
73 72 a1i 
 |-  ( X e. CC -> 1 e. ( ZZ>= ` 0 ) )
74 fzssp1 
 |-  ( 0 ... ( 1 + 1 ) ) C_ ( 0 ... ( ( 1 + 1 ) + 1 ) )
75 63 oveq1i 
 |-  ( 2 + 1 ) = ( ( 1 + 1 ) + 1 )
76 75 oveq2i 
 |-  ( 0 ... ( 2 + 1 ) ) = ( 0 ... ( ( 1 + 1 ) + 1 ) )
77 74 76 sseqtrri 
 |-  ( 0 ... ( 1 + 1 ) ) C_ ( 0 ... ( 2 + 1 ) )
78 77 sseli 
 |-  ( k e. ( 0 ... ( 1 + 1 ) ) -> k e. ( 0 ... ( 2 + 1 ) ) )
79 78 49 sylan2 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 1 + 1 ) ) ) -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) e. CC )
80 63 eqeq2i 
 |-  ( k = 2 <-> k = ( 1 + 1 ) )
81 oveq2 
 |-  ( k = 2 -> ( 4 _C k ) = ( 4 _C 2 ) )
82 4bc2eq6 
 |-  ( 4 _C 2 ) = 6
83 81 82 eqtrdi 
 |-  ( k = 2 -> ( 4 _C k ) = 6 )
84 oveq1 
 |-  ( k = 2 -> ( k BernPoly X ) = ( 2 BernPoly X ) )
85 oveq2 
 |-  ( k = 2 -> ( 4 - k ) = ( 4 - 2 ) )
86 85 oveq1d 
 |-  ( k = 2 -> ( ( 4 - k ) + 1 ) = ( ( 4 - 2 ) + 1 ) )
87 2cn 
 |-  2 e. CC
88 2p2e4 
 |-  ( 2 + 2 ) = 4
89 57 87 87 88 subaddrii 
 |-  ( 4 - 2 ) = 2
90 89 oveq1i 
 |-  ( ( 4 - 2 ) + 1 ) = ( 2 + 1 )
91 90 5 eqtr4i 
 |-  ( ( 4 - 2 ) + 1 ) = 3
92 86 91 eqtrdi 
 |-  ( k = 2 -> ( ( 4 - k ) + 1 ) = 3 )
93 84 92 oveq12d 
 |-  ( k = 2 -> ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) = ( ( 2 BernPoly X ) / 3 ) )
94 83 93 oveq12d 
 |-  ( k = 2 -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 6 x. ( ( 2 BernPoly X ) / 3 ) ) )
95 80 94 sylbir 
 |-  ( k = ( 1 + 1 ) -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 6 x. ( ( 2 BernPoly X ) / 3 ) ) )
96 73 79 95 fsump1 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 1 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... 1 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) + ( 6 x. ( ( 2 BernPoly X ) / 3 ) ) ) )
97 0p1e1 
 |-  ( 0 + 1 ) = 1
98 97 oveq2i 
 |-  ( 0 ... ( 0 + 1 ) ) = ( 0 ... 1 )
99 98 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = sum_ k e. ( 0 ... 1 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) )
100 0nn0 
 |-  0 e. NN0
101 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
102 100 101 eleqtri 
 |-  0 e. ( ZZ>= ` 0 )
103 102 a1i 
 |-  ( X e. CC -> 0 e. ( ZZ>= ` 0 ) )
104 3nn 
 |-  3 e. NN
105 nnuz 
 |-  NN = ( ZZ>= ` 1 )
106 104 105 eleqtri 
 |-  3 e. ( ZZ>= ` 1 )
107 fzss2 
 |-  ( 3 e. ( ZZ>= ` 1 ) -> ( 0 ... 1 ) C_ ( 0 ... 3 ) )
108 106 107 ax-mp 
 |-  ( 0 ... 1 ) C_ ( 0 ... 3 )
109 2p1e3 
 |-  ( 2 + 1 ) = 3
110 109 oveq2i 
 |-  ( 0 ... ( 2 + 1 ) ) = ( 0 ... 3 )
111 108 98 110 3sstr4i 
 |-  ( 0 ... ( 0 + 1 ) ) C_ ( 0 ... ( 2 + 1 ) )
112 111 sseli 
 |-  ( k e. ( 0 ... ( 0 + 1 ) ) -> k e. ( 0 ... ( 2 + 1 ) ) )
113 112 49 sylan2 
 |-  ( ( X e. CC /\ k e. ( 0 ... ( 0 + 1 ) ) ) -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) e. CC )
114 97 eqeq2i 
 |-  ( k = ( 0 + 1 ) <-> k = 1 )
115 oveq2 
 |-  ( k = 1 -> ( 4 _C k ) = ( 4 _C 1 ) )
116 bcn1 
 |-  ( 4 e. NN0 -> ( 4 _C 1 ) = 4 )
117 1 116 ax-mp 
 |-  ( 4 _C 1 ) = 4
118 115 117 eqtrdi 
 |-  ( k = 1 -> ( 4 _C k ) = 4 )
119 oveq1 
 |-  ( k = 1 -> ( k BernPoly X ) = ( 1 BernPoly X ) )
120 oveq2 
 |-  ( k = 1 -> ( 4 - k ) = ( 4 - 1 ) )
121 120 oveq1d 
 |-  ( k = 1 -> ( ( 4 - k ) + 1 ) = ( ( 4 - 1 ) + 1 ) )
122 4 oveq1i 
 |-  ( ( 4 - 1 ) + 1 ) = ( 3 + 1 )
123 df-4 
 |-  4 = ( 3 + 1 )
124 122 123 eqtr4i 
 |-  ( ( 4 - 1 ) + 1 ) = 4
125 121 124 eqtrdi 
 |-  ( k = 1 -> ( ( 4 - k ) + 1 ) = 4 )
126 119 125 oveq12d 
 |-  ( k = 1 -> ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) = ( ( 1 BernPoly X ) / 4 ) )
127 118 126 oveq12d 
 |-  ( k = 1 -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 4 x. ( ( 1 BernPoly X ) / 4 ) ) )
128 114 127 sylbi 
 |-  ( k = ( 0 + 1 ) -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 4 x. ( ( 1 BernPoly X ) / 4 ) ) )
129 103 113 128 fsump1 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... 0 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) + ( 4 x. ( ( 1 BernPoly X ) / 4 ) ) ) )
130 0z 
 |-  0 e. ZZ
131 59 a1i 
 |-  ( X e. CC -> 1 e. CC )
132 bpolycl 
 |-  ( ( 0 e. NN0 /\ X e. CC ) -> ( 0 BernPoly X ) e. CC )
133 100 132 mpan 
 |-  ( X e. CC -> ( 0 BernPoly X ) e. CC )
134 5cn 
 |-  5 e. CC
135 134 a1i 
 |-  ( X e. CC -> 5 e. CC )
136 0re 
 |-  0 e. RR
137 5pos 
 |-  0 < 5
138 136 137 gtneii 
 |-  5 =/= 0
139 138 a1i 
 |-  ( X e. CC -> 5 =/= 0 )
140 133 135 139 divcld 
 |-  ( X e. CC -> ( ( 0 BernPoly X ) / 5 ) e. CC )
141 131 140 mulcld 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) e. CC )
142 oveq2 
 |-  ( k = 0 -> ( 4 _C k ) = ( 4 _C 0 ) )
143 bcn0 
 |-  ( 4 e. NN0 -> ( 4 _C 0 ) = 1 )
144 1 143 ax-mp 
 |-  ( 4 _C 0 ) = 1
145 142 144 eqtrdi 
 |-  ( k = 0 -> ( 4 _C k ) = 1 )
146 oveq1 
 |-  ( k = 0 -> ( k BernPoly X ) = ( 0 BernPoly X ) )
147 oveq2 
 |-  ( k = 0 -> ( 4 - k ) = ( 4 - 0 ) )
148 147 oveq1d 
 |-  ( k = 0 -> ( ( 4 - k ) + 1 ) = ( ( 4 - 0 ) + 1 ) )
149 57 subid1i 
 |-  ( 4 - 0 ) = 4
150 149 oveq1i 
 |-  ( ( 4 - 0 ) + 1 ) = ( 4 + 1 )
151 4p1e5 
 |-  ( 4 + 1 ) = 5
152 150 151 eqtri 
 |-  ( ( 4 - 0 ) + 1 ) = 5
153 148 152 eqtrdi 
 |-  ( k = 0 -> ( ( 4 - k ) + 1 ) = 5 )
154 146 153 oveq12d 
 |-  ( k = 0 -> ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) = ( ( 0 BernPoly X ) / 5 ) )
155 145 154 oveq12d 
 |-  ( k = 0 -> ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) )
156 155 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) )
157 130 141 156 sylancr 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) )
158 bpoly0 
 |-  ( X e. CC -> ( 0 BernPoly X ) = 1 )
159 158 oveq1d 
 |-  ( X e. CC -> ( ( 0 BernPoly X ) / 5 ) = ( 1 / 5 ) )
160 159 oveq2d 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) = ( 1 x. ( 1 / 5 ) ) )
161 134 138 reccli 
 |-  ( 1 / 5 ) e. CC
162 161 mulid2i 
 |-  ( 1 x. ( 1 / 5 ) ) = ( 1 / 5 )
163 160 162 eqtrdi 
 |-  ( X e. CC -> ( 1 x. ( ( 0 BernPoly X ) / 5 ) ) = ( 1 / 5 ) )
164 157 163 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 0 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( 1 / 5 ) )
165 1nn0 
 |-  1 e. NN0
166 bpolycl 
 |-  ( ( 1 e. NN0 /\ X e. CC ) -> ( 1 BernPoly X ) e. CC )
167 165 166 mpan 
 |-  ( X e. CC -> ( 1 BernPoly X ) e. CC )
168 nn0cn 
 |-  ( 4 e. NN0 -> 4 e. CC )
169 1 168 mp1i 
 |-  ( X e. CC -> 4 e. CC )
170 4ne0 
 |-  4 =/= 0
171 170 a1i 
 |-  ( X e. CC -> 4 =/= 0 )
172 167 169 171 divcan2d 
 |-  ( X e. CC -> ( 4 x. ( ( 1 BernPoly X ) / 4 ) ) = ( 1 BernPoly X ) )
173 bpoly1 
 |-  ( X e. CC -> ( 1 BernPoly X ) = ( X - ( 1 / 2 ) ) )
174 172 173 eqtrd 
 |-  ( X e. CC -> ( 4 x. ( ( 1 BernPoly X ) / 4 ) ) = ( X - ( 1 / 2 ) ) )
175 164 174 oveq12d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 0 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) + ( 4 x. ( ( 1 BernPoly X ) / 4 ) ) ) = ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) )
176 129 175 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) )
177 99 176 eqtr3id 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 1 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) )
178 6cn 
 |-  6 e. CC
179 178 a1i 
 |-  ( X e. CC -> 6 e. CC )
180 2nn0 
 |-  2 e. NN0
181 bpolycl 
 |-  ( ( 2 e. NN0 /\ X e. CC ) -> ( 2 BernPoly X ) e. CC )
182 180 181 mpan 
 |-  ( X e. CC -> ( 2 BernPoly X ) e. CC )
183 58 a1i 
 |-  ( X e. CC -> 3 e. CC )
184 3ne0 
 |-  3 =/= 0
185 184 a1i 
 |-  ( X e. CC -> 3 =/= 0 )
186 179 182 183 185 div12d 
 |-  ( X e. CC -> ( 6 x. ( ( 2 BernPoly X ) / 3 ) ) = ( ( 2 BernPoly X ) x. ( 6 / 3 ) ) )
187 3t2e6 
 |-  ( 3 x. 2 ) = 6
188 178 58 87 184 divmuli 
 |-  ( ( 6 / 3 ) = 2 <-> ( 3 x. 2 ) = 6 )
189 187 188 mpbir 
 |-  ( 6 / 3 ) = 2
190 189 oveq2i 
 |-  ( ( 2 BernPoly X ) x. ( 6 / 3 ) ) = ( ( 2 BernPoly X ) x. 2 )
191 87 a1i 
 |-  ( X e. CC -> 2 e. CC )
192 182 191 mulcomd 
 |-  ( X e. CC -> ( ( 2 BernPoly X ) x. 2 ) = ( 2 x. ( 2 BernPoly X ) ) )
193 bpoly2 
 |-  ( X e. CC -> ( 2 BernPoly X ) = ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) )
194 193 oveq2d 
 |-  ( X e. CC -> ( 2 x. ( 2 BernPoly X ) ) = ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) )
195 192 194 eqtrd 
 |-  ( X e. CC -> ( ( 2 BernPoly X ) x. 2 ) = ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) )
196 190 195 eqtrid 
 |-  ( X e. CC -> ( ( 2 BernPoly X ) x. ( 6 / 3 ) ) = ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) )
197 186 196 eqtrd 
 |-  ( X e. CC -> ( 6 x. ( ( 2 BernPoly X ) / 3 ) ) = ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) )
198 177 197 oveq12d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 1 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) + ( 6 x. ( ( 2 BernPoly X ) / 3 ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) )
199 96 198 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 1 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) )
200 71 199 eqtrid 
 |-  ( X e. CC -> sum_ k e. ( 0 ... 2 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) )
201 3nn0 
 |-  3 e. NN0
202 bpolycl 
 |-  ( ( 3 e. NN0 /\ X e. CC ) -> ( 3 BernPoly X ) e. CC )
203 201 202 mpan 
 |-  ( X e. CC -> ( 3 BernPoly X ) e. CC )
204 2ne0 
 |-  2 =/= 0
205 204 a1i 
 |-  ( X e. CC -> 2 =/= 0 )
206 169 203 191 205 div12d 
 |-  ( X e. CC -> ( 4 x. ( ( 3 BernPoly X ) / 2 ) ) = ( ( 3 BernPoly X ) x. ( 4 / 2 ) ) )
207 4d2e2 
 |-  ( 4 / 2 ) = 2
208 207 oveq2i 
 |-  ( ( 3 BernPoly X ) x. ( 4 / 2 ) ) = ( ( 3 BernPoly X ) x. 2 )
209 203 191 mulcomd 
 |-  ( X e. CC -> ( ( 3 BernPoly X ) x. 2 ) = ( 2 x. ( 3 BernPoly X ) ) )
210 bpoly3 
 |-  ( X e. CC -> ( 3 BernPoly X ) = ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) )
211 210 oveq2d 
 |-  ( X e. CC -> ( 2 x. ( 3 BernPoly X ) ) = ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) )
212 209 211 eqtrd 
 |-  ( X e. CC -> ( ( 3 BernPoly X ) x. 2 ) = ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) )
213 208 212 eqtrid 
 |-  ( X e. CC -> ( ( 3 BernPoly X ) x. ( 4 / 2 ) ) = ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) )
214 206 213 eqtrd 
 |-  ( X e. CC -> ( 4 x. ( ( 3 BernPoly X ) / 2 ) ) = ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) )
215 200 214 oveq12d 
 |-  ( X e. CC -> ( sum_ k e. ( 0 ... 2 ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) + ( 4 x. ( ( 3 BernPoly X ) / 2 ) ) ) = ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) )
216 69 215 eqtrd 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 2 + 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) )
217 8 216 eqtrid 
 |-  ( X e. CC -> sum_ k e. ( 0 ... ( 4 - 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) = ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) )
218 217 oveq2d 
 |-  ( X e. CC -> ( ( X ^ 4 ) - sum_ k e. ( 0 ... ( 4 - 1 ) ) ( ( 4 _C k ) x. ( ( k BernPoly X ) / ( ( 4 - k ) + 1 ) ) ) ) = ( ( X ^ 4 ) - ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) ) )
219 expcl 
 |-  ( ( X e. CC /\ 4 e. NN0 ) -> ( X ^ 4 ) e. CC )
220 1 219 mpan2 
 |-  ( X e. CC -> ( X ^ 4 ) e. CC )
221 expcl 
 |-  ( ( X e. CC /\ 3 e. NN0 ) -> ( X ^ 3 ) e. CC )
222 201 221 mpan2 
 |-  ( X e. CC -> ( X ^ 3 ) e. CC )
223 191 222 mulcld 
 |-  ( X e. CC -> ( 2 x. ( X ^ 3 ) ) e. CC )
224 sqcl 
 |-  ( X e. CC -> ( X ^ 2 ) e. CC )
225 201 100 deccl 
 |-  ; 3 0 e. NN0
226 225 nn0cni 
 |-  ; 3 0 e. CC
227 dfdec10 
 |-  ; 3 0 = ( ( ; 1 0 x. 3 ) + 0 )
228 10re 
 |-  ; 1 0 e. RR
229 228 recni 
 |-  ; 1 0 e. CC
230 229 58 mulcli 
 |-  ( ; 1 0 x. 3 ) e. CC
231 230 addid1i 
 |-  ( ( ; 1 0 x. 3 ) + 0 ) = ( ; 1 0 x. 3 )
232 227 231 eqtri 
 |-  ; 3 0 = ( ; 1 0 x. 3 )
233 10pos 
 |-  0 < ; 1 0
234 136 233 gtneii 
 |-  ; 1 0 =/= 0
235 229 58 234 184 mulne0i 
 |-  ( ; 1 0 x. 3 ) =/= 0
236 232 235 eqnetri 
 |-  ; 3 0 =/= 0
237 226 236 reccli 
 |-  ( 1 / ; 3 0 ) e. CC
238 237 a1i 
 |-  ( X e. CC -> ( 1 / ; 3 0 ) e. CC )
239 224 238 subcld 
 |-  ( X e. CC -> ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) e. CC )
240 220 223 239 subsubd 
 |-  ( X e. CC -> ( ( X ^ 4 ) - ( ( 2 x. ( X ^ 3 ) ) - ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) ) = ( ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) + ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) )
241 161 a1i 
 |-  ( X e. CC -> ( 1 / 5 ) e. CC )
242 id 
 |-  ( X e. CC -> X e. CC )
243 87 204 reccli 
 |-  ( 1 / 2 ) e. CC
244 243 a1i 
 |-  ( X e. CC -> ( 1 / 2 ) e. CC )
245 242 244 subcld 
 |-  ( X e. CC -> ( X - ( 1 / 2 ) ) e. CC )
246 241 245 addcld 
 |-  ( X e. CC -> ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) e. CC )
247 224 242 subcld 
 |-  ( X e. CC -> ( ( X ^ 2 ) - X ) e. CC )
248 6pos 
 |-  0 < 6
249 136 248 gtneii 
 |-  6 =/= 0
250 178 249 reccli 
 |-  ( 1 / 6 ) e. CC
251 250 a1i 
 |-  ( X e. CC -> ( 1 / 6 ) e. CC )
252 247 251 addcld 
 |-  ( X e. CC -> ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) e. CC )
253 191 252 mulcld 
 |-  ( X e. CC -> ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) e. CC )
254 246 253 addcld 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) e. CC )
255 58 87 204 divcli 
 |-  ( 3 / 2 ) e. CC
256 255 a1i 
 |-  ( X e. CC -> ( 3 / 2 ) e. CC )
257 256 224 mulcld 
 |-  ( X e. CC -> ( ( 3 / 2 ) x. ( X ^ 2 ) ) e. CC )
258 222 257 subcld 
 |-  ( X e. CC -> ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) e. CC )
259 244 242 mulcld 
 |-  ( X e. CC -> ( ( 1 / 2 ) x. X ) e. CC )
260 258 259 addcld 
 |-  ( X e. CC -> ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) e. CC )
261 191 260 mulcld 
 |-  ( X e. CC -> ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) e. CC )
262 254 261 addcomd 
 |-  ( X e. CC -> ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) = ( ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) )
263 191 258 259 adddid 
 |-  ( X e. CC -> ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) = ( ( 2 x. ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + ( 2 x. ( ( 1 / 2 ) x. X ) ) ) )
264 191 222 257 subdid 
 |-  ( X e. CC -> ( 2 x. ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) = ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) )
265 87 204 recidi 
 |-  ( 2 x. ( 1 / 2 ) ) = 1
266 265 oveq1i 
 |-  ( ( 2 x. ( 1 / 2 ) ) x. X ) = ( 1 x. X )
267 191 244 242 mulassd 
 |-  ( X e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. X ) = ( 2 x. ( ( 1 / 2 ) x. X ) ) )
268 mulid2 
 |-  ( X e. CC -> ( 1 x. X ) = X )
269 266 267 268 3eqtr3a 
 |-  ( X e. CC -> ( 2 x. ( ( 1 / 2 ) x. X ) ) = X )
270 264 269 oveq12d 
 |-  ( X e. CC -> ( ( 2 x. ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + ( 2 x. ( ( 1 / 2 ) x. X ) ) ) = ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + X ) )
271 263 270 eqtrd 
 |-  ( X e. CC -> ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) = ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + X ) )
272 271 oveq1d 
 |-  ( X e. CC -> ( ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) = ( ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + X ) + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) )
273 191 257 mulcld 
 |-  ( X e. CC -> ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) e. CC )
274 223 273 subcld 
 |-  ( X e. CC -> ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) e. CC )
275 274 242 254 addassd 
 |-  ( X e. CC -> ( ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + X ) + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) )
276 242 254 addcld 
 |-  ( X e. CC -> ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) e. CC )
277 223 273 276 subsubd 
 |-  ( X e. CC -> ( ( 2 x. ( X ^ 3 ) ) - ( ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) - ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) ) = ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) )
278 191 256 224 mulassd 
 |-  ( X e. CC -> ( ( 2 x. ( 3 / 2 ) ) x. ( X ^ 2 ) ) = ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) )
279 58 87 204 divcan2i 
 |-  ( 2 x. ( 3 / 2 ) ) = 3
280 279 oveq1i 
 |-  ( ( 2 x. ( 3 / 2 ) ) x. ( X ^ 2 ) ) = ( 3 x. ( X ^ 2 ) )
281 278 280 eqtr3di 
 |-  ( X e. CC -> ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) = ( 3 x. ( X ^ 2 ) ) )
282 281 oveq1d 
 |-  ( X e. CC -> ( ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) - ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) = ( ( 3 x. ( X ^ 2 ) ) - ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) )
283 242 246 253 add12d 
 |-  ( X e. CC -> ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( X + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) )
284 191 247 251 adddid 
 |-  ( X e. CC -> ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) = ( ( 2 x. ( ( X ^ 2 ) - X ) ) + ( 2 x. ( 1 / 6 ) ) ) )
285 191 224 242 subdid 
 |-  ( X e. CC -> ( 2 x. ( ( X ^ 2 ) - X ) ) = ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) )
286 187 oveq2i 
 |-  ( 2 / ( 3 x. 2 ) ) = ( 2 / 6 )
287 58 184 reccli 
 |-  ( 1 / 3 ) e. CC
288 58 87 287 mul32i 
 |-  ( ( 3 x. 2 ) x. ( 1 / 3 ) ) = ( ( 3 x. ( 1 / 3 ) ) x. 2 )
289 58 184 recidi 
 |-  ( 3 x. ( 1 / 3 ) ) = 1
290 289 oveq1i 
 |-  ( ( 3 x. ( 1 / 3 ) ) x. 2 ) = ( 1 x. 2 )
291 87 mulid2i 
 |-  ( 1 x. 2 ) = 2
292 290 291 eqtri 
 |-  ( ( 3 x. ( 1 / 3 ) ) x. 2 ) = 2
293 288 292 eqtri 
 |-  ( ( 3 x. 2 ) x. ( 1 / 3 ) ) = 2
294 187 178 eqeltri 
 |-  ( 3 x. 2 ) e. CC
295 187 249 eqnetri 
 |-  ( 3 x. 2 ) =/= 0
296 87 294 287 295 divmuli 
 |-  ( ( 2 / ( 3 x. 2 ) ) = ( 1 / 3 ) <-> ( ( 3 x. 2 ) x. ( 1 / 3 ) ) = 2 )
297 293 296 mpbir 
 |-  ( 2 / ( 3 x. 2 ) ) = ( 1 / 3 )
298 87 178 249 divreci 
 |-  ( 2 / 6 ) = ( 2 x. ( 1 / 6 ) )
299 286 297 298 3eqtr3ri 
 |-  ( 2 x. ( 1 / 6 ) ) = ( 1 / 3 )
300 299 a1i 
 |-  ( X e. CC -> ( 2 x. ( 1 / 6 ) ) = ( 1 / 3 ) )
301 285 300 oveq12d 
 |-  ( X e. CC -> ( ( 2 x. ( ( X ^ 2 ) - X ) ) + ( 2 x. ( 1 / 6 ) ) ) = ( ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) + ( 1 / 3 ) ) )
302 284 301 eqtrd 
 |-  ( X e. CC -> ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) = ( ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) + ( 1 / 3 ) ) )
303 302 oveq2d 
 |-  ( X e. CC -> ( X + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) = ( X + ( ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) + ( 1 / 3 ) ) ) )
304 191 224 mulcld 
 |-  ( X e. CC -> ( 2 x. ( X ^ 2 ) ) e. CC )
305 191 242 mulcld 
 |-  ( X e. CC -> ( 2 x. X ) e. CC )
306 304 305 subcld 
 |-  ( X e. CC -> ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) e. CC )
307 287 a1i 
 |-  ( X e. CC -> ( 1 / 3 ) e. CC )
308 242 306 307 addassd 
 |-  ( X e. CC -> ( ( X + ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) ) + ( 1 / 3 ) ) = ( X + ( ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) + ( 1 / 3 ) ) ) )
309 242 304 305 addsub12d 
 |-  ( X e. CC -> ( X + ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) ) = ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) )
310 309 oveq1d 
 |-  ( X e. CC -> ( ( X + ( ( 2 x. ( X ^ 2 ) ) - ( 2 x. X ) ) ) + ( 1 / 3 ) ) = ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) )
311 303 308 310 3eqtr2d 
 |-  ( X e. CC -> ( X + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) = ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) )
312 311 oveq2d 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( X + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) )
313 283 312 eqtrd 
 |-  ( X e. CC -> ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) )
314 313 oveq2d 
 |-  ( X e. CC -> ( ( 3 x. ( X ^ 2 ) ) - ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) = ( ( 3 x. ( X ^ 2 ) ) - ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) ) )
315 242 305 subcld 
 |-  ( X e. CC -> ( X - ( 2 x. X ) ) e. CC )
316 304 315 addcld 
 |-  ( X e. CC -> ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) e. CC )
317 241 245 316 307 add4d 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) = ( ( ( 1 / 5 ) + ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) )
318 241 304 315 add12d 
 |-  ( X e. CC -> ( ( 1 / 5 ) + ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) ) = ( ( 2 x. ( X ^ 2 ) ) + ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) ) )
319 318 oveq1d 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) = ( ( ( 2 x. ( X ^ 2 ) ) + ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) )
320 241 315 addcld 
 |-  ( X e. CC -> ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) e. CC )
321 245 307 addcld 
 |-  ( X e. CC -> ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) e. CC )
322 304 320 321 addassd 
 |-  ( X e. CC -> ( ( ( 2 x. ( X ^ 2 ) ) + ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) = ( ( 2 x. ( X ^ 2 ) ) + ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) )
323 317 319 322 3eqtrd 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) = ( ( 2 x. ( X ^ 2 ) ) + ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) )
324 323 oveq2d 
 |-  ( X e. CC -> ( ( 3 x. ( X ^ 2 ) ) - ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) ) = ( ( 3 x. ( X ^ 2 ) ) - ( ( 2 x. ( X ^ 2 ) ) + ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) ) )
325 183 224 mulcld 
 |-  ( X e. CC -> ( 3 x. ( X ^ 2 ) ) e. CC )
326 320 321 addcld 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) e. CC )
327 325 304 326 subsub4d 
 |-  ( X e. CC -> ( ( ( 3 x. ( X ^ 2 ) ) - ( 2 x. ( X ^ 2 ) ) ) - ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) = ( ( 3 x. ( X ^ 2 ) ) - ( ( 2 x. ( X ^ 2 ) ) + ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) ) )
328 58 87 59 109 subaddrii 
 |-  ( 3 - 2 ) = 1
329 328 oveq1i 
 |-  ( ( 3 - 2 ) x. ( X ^ 2 ) ) = ( 1 x. ( X ^ 2 ) )
330 183 191 224 subdird 
 |-  ( X e. CC -> ( ( 3 - 2 ) x. ( X ^ 2 ) ) = ( ( 3 x. ( X ^ 2 ) ) - ( 2 x. ( X ^ 2 ) ) ) )
331 224 mulid2d 
 |-  ( X e. CC -> ( 1 x. ( X ^ 2 ) ) = ( X ^ 2 ) )
332 329 330 331 3eqtr3a 
 |-  ( X e. CC -> ( ( 3 x. ( X ^ 2 ) ) - ( 2 x. ( X ^ 2 ) ) ) = ( X ^ 2 ) )
333 241 305 242 subsubd 
 |-  ( X e. CC -> ( ( 1 / 5 ) - ( ( 2 x. X ) - X ) ) = ( ( ( 1 / 5 ) - ( 2 x. X ) ) + X ) )
334 2txmxeqx 
 |-  ( X e. CC -> ( ( 2 x. X ) - X ) = X )
335 334 oveq2d 
 |-  ( X e. CC -> ( ( 1 / 5 ) - ( ( 2 x. X ) - X ) ) = ( ( 1 / 5 ) - X ) )
336 241 305 242 subadd23d 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) - ( 2 x. X ) ) + X ) = ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) )
337 333 335 336 3eqtr3d 
 |-  ( X e. CC -> ( ( 1 / 5 ) - X ) = ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) )
338 242 244 307 subsubd 
 |-  ( X e. CC -> ( X - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) )
339 337 338 oveq12d 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) - X ) + ( X - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) ) = ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) )
340 243 287 subcli 
 |-  ( ( 1 / 2 ) - ( 1 / 3 ) ) e. CC
341 340 a1i 
 |-  ( X e. CC -> ( ( 1 / 2 ) - ( 1 / 3 ) ) e. CC )
342 241 242 341 npncand 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) - X ) + ( X - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) ) = ( ( 1 / 5 ) - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) )
343 halfthird 
 |-  ( ( 1 / 2 ) - ( 1 / 3 ) ) = ( 1 / 6 )
344 343 oveq2i 
 |-  ( ( 1 / 5 ) - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( ( 1 / 5 ) - ( 1 / 6 ) )
345 5recm6rec 
 |-  ( ( 1 / 5 ) - ( 1 / 6 ) ) = ( 1 / ; 3 0 )
346 344 345 eqtri 
 |-  ( ( 1 / 5 ) - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) = ( 1 / ; 3 0 )
347 342 346 eqtrdi 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) - X ) + ( X - ( ( 1 / 2 ) - ( 1 / 3 ) ) ) ) = ( 1 / ; 3 0 ) )
348 339 347 eqtr3d 
 |-  ( X e. CC -> ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) = ( 1 / ; 3 0 ) )
349 332 348 oveq12d 
 |-  ( X e. CC -> ( ( ( 3 x. ( X ^ 2 ) ) - ( 2 x. ( X ^ 2 ) ) ) - ( ( ( 1 / 5 ) + ( X - ( 2 x. X ) ) ) + ( ( X - ( 1 / 2 ) ) + ( 1 / 3 ) ) ) ) = ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) )
350 324 327 349 3eqtr2d 
 |-  ( X e. CC -> ( ( 3 x. ( X ^ 2 ) ) - ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( ( ( 2 x. ( X ^ 2 ) ) + ( X - ( 2 x. X ) ) ) + ( 1 / 3 ) ) ) ) = ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) )
351 282 314 350 3eqtrd 
 |-  ( X e. CC -> ( ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) - ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) = ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) )
352 351 oveq2d 
 |-  ( X e. CC -> ( ( 2 x. ( X ^ 3 ) ) - ( ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) - ( X + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) ) ) = ( ( 2 x. ( X ^ 3 ) ) - ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) )
353 275 277 352 3eqtr2d 
 |-  ( X e. CC -> ( ( ( ( 2 x. ( X ^ 3 ) ) - ( 2 x. ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) ) + X ) + ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) ) = ( ( 2 x. ( X ^ 3 ) ) - ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) )
354 262 272 353 3eqtrd 
 |-  ( X e. CC -> ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) = ( ( 2 x. ( X ^ 3 ) ) - ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) )
355 354 oveq2d 
 |-  ( X e. CC -> ( ( X ^ 4 ) - ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) ) = ( ( X ^ 4 ) - ( ( 2 x. ( X ^ 3 ) ) - ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) ) )
356 220 223 subcld 
 |-  ( X e. CC -> ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) e. CC )
357 356 224 238 addsubassd 
 |-  ( X e. CC -> ( ( ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) + ( X ^ 2 ) ) - ( 1 / ; 3 0 ) ) = ( ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) + ( ( X ^ 2 ) - ( 1 / ; 3 0 ) ) ) )
358 240 355 357 3eqtr4d 
 |-  ( X e. CC -> ( ( X ^ 4 ) - ( ( ( ( 1 / 5 ) + ( X - ( 1 / 2 ) ) ) + ( 2 x. ( ( ( X ^ 2 ) - X ) + ( 1 / 6 ) ) ) ) + ( 2 x. ( ( ( X ^ 3 ) - ( ( 3 / 2 ) x. ( X ^ 2 ) ) ) + ( ( 1 / 2 ) x. X ) ) ) ) ) = ( ( ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) + ( X ^ 2 ) ) - ( 1 / ; 3 0 ) ) )
359 3 218 358 3eqtrd 
 |-  ( X e. CC -> ( 4 BernPoly X ) = ( ( ( ( X ^ 4 ) - ( 2 x. ( X ^ 3 ) ) ) + ( X ^ 2 ) ) - ( 1 / ; 3 0 ) ) )