Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bpoly4 Unicode version

Theorem bpoly4 24866
Description: The Bernoulli polynomials at four. (Contributed by Scott Fenton, 8-Jul-2015.)
Assertion
Ref Expression
bpoly4  |-  ( X  e.  CC  ->  (
4 BernPoly  X )  =  ( ( ( ( X ^ 4 )  -  ( 2  x.  ( X ^ 3 ) ) )  +  ( X ^ 2 ) )  -  ( 1  / ; 3 0 ) ) )

Proof of Theorem bpoly4
Dummy variable  k is distinct from all other variables.
StepHypRef Expression
1 4nn0 10000 . . 3  |-  4  e.  NN0
2 bpolyval 24856 . . 3  |-  ( ( 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 ) ) ) ) )
31, 2mpan 651 . 2  |-  ( 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 4cn 9836 . . . . . . . 8  |-  4  e.  CC
5 ax-1cn 8811 . . . . . . . 8  |-  1  e.  CC
6 3cn 9834 . . . . . . . 8  |-  3  e.  CC
7 3p1e4 9864 . . . . . . . . 9  |-  ( 3  +  1 )  =  4
86, 5, 7addcomli 9020 . . . . . . . 8  |-  ( 1  +  3 )  =  4
94, 5, 6, 8subaddrii 9151 . . . . . . 7  |-  ( 4  -  1 )  =  3
10 df-3 9821 . . . . . . 7  |-  3  =  ( 2  +  1 )
119, 10eqtri 2316 . . . . . 6  |-  ( 4  -  1 )  =  ( 2  +  1 )
1211oveq2i 5885 . . . . 5  |-  ( 0 ... ( 4  -  1 ) )  =  ( 0 ... (
2  +  1 ) )
1312sumeq1i 12187 . . . 4  |-  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 ) ) )
14 2nn0 9998 . . . . . . . 8  |-  2  e.  NN0
15 nn0uz 10278 . . . . . . . 8  |-  NN0  =  ( ZZ>= `  0 )
1614, 15eleqtri 2368 . . . . . . 7  |-  2  e.  ( ZZ>= `  0 )
1716a1i 10 . . . . . 6  |-  ( X  e.  CC  ->  2  e.  ( ZZ>= `  0 )
)
18 elfzelz 10814 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  e.  ZZ )
19 bccl 11350 . . . . . . . . . 10  |-  ( ( 4  e.  NN0  /\  k  e.  ZZ )  ->  ( 4  _C  k
)  e.  NN0 )
201, 18, 19sylancr 644 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
4  _C  k )  e.  NN0 )
2120nn0cnd 10036 . . . . . . . 8  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
4  _C  k )  e.  CC )
2221adantl 452 . . . . . . 7  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( 4  _C  k )  e.  CC )
23 elfznn0 10838 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  e.  NN0 )
24 bpolycl 24859 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  X  e.  CC )  ->  ( k BernPoly  X )  e.  CC )
2523, 24sylan 457 . . . . . . . . 9  |-  ( ( k  e.  ( 0 ... ( 2  +  1 ) )  /\  X  e.  CC )  ->  ( k BernPoly  X )  e.  CC )
2625ancoms 439 . . . . . . . 8  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( k BernPoly  X
)  e.  CC )
27 4re 9835 . . . . . . . . . . . . 13  |-  4  e.  RR
2827a1i 10 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  4  e.  RR )
2918zred 10133 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  e.  RR )
3028, 29resubcld 9227 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
4  -  k )  e.  RR )
31 peano2re 9001 . . . . . . . . . . 11  |-  ( ( 4  -  k )  e.  RR  ->  (
( 4  -  k
)  +  1 )  e.  RR )
3230, 31syl 15 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
( 4  -  k
)  +  1 )  e.  RR )
3332recnd 8877 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
( 4  -  k
)  +  1 )  e.  CC )
3433adantl 452 . . . . . . . 8  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( 4  -  k )  +  1 )  e.  CC )
35 1re 8853 . . . . . . . . . . . 12  |-  1  e.  RR
3635a1i 10 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  1  e.  RR )
3710oveq2i 5885 . . . . . . . . . . . . . 14  |-  ( 0 ... 3 )  =  ( 0 ... (
2  +  1 ) )
3837eleq2i 2360 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... 3 )  <->  k  e.  ( 0 ... (
2  +  1 ) ) )
39 elfzelz 10814 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... 3 )  ->  k  e.  ZZ )
4039zred 10133 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  k  e.  RR )
41 3re 9833 . . . . . . . . . . . . . . 15  |-  3  e.  RR
4241a1i 10 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  3  e.  RR )
4327a1i 10 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  4  e.  RR )
44 elfzle2 10816 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  k  <_  3 )
45 3lt4 9905 . . . . . . . . . . . . . . 15  |-  3  <  4
4645a1i 10 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  3  <  4 )
4740, 42, 43, 44, 46lelttrd 8990 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... 3 )  ->  k  <  4 )
4838, 47sylbir 204 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  <  4 )
4929, 28posdifd 9375 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
k  <  4  <->  0  <  ( 4  -  k ) ) )
5048, 49mpbid 201 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  0  <  ( 4  -  k
) )
51 0lt1 9312 . . . . . . . . . . . 12  |-  0  <  1
5251a1i 10 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  0  <  1 )
5330, 36, 50, 52addgt0d 9363 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  0  <  ( ( 4  -  k )  +  1 ) )
5453gt0ne0d 9353 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
( 4  -  k
)  +  1 )  =/=  0 )
5554adantl 452 . . . . . . . 8  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( 4  -  k )  +  1 )  =/=  0
)
5626, 34, 55divcld 9552 . . . . . . 7  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) )  e.  CC )
5722, 56mulcld 8871 . . . . . 6  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  e.  CC )
5810eqeq2i 2306 . . . . . . 7  |-  ( k  =  3  <->  k  =  ( 2  +  1 ) )
59 oveq2 5882 . . . . . . . . 9  |-  ( k  =  3  ->  (
4  _C  k )  =  ( 4  _C  3 ) )
60 4bc3eq4 24113 . . . . . . . . 9  |-  ( 4  _C  3 )  =  4
6159, 60syl6eq 2344 . . . . . . . 8  |-  ( k  =  3  ->  (
4  _C  k )  =  4 )
62 oveq1 5881 . . . . . . . . 9  |-  ( k  =  3  ->  (
k BernPoly  X )  =  ( 3 BernPoly  X ) )
63 oveq2 5882 . . . . . . . . . . 11  |-  ( k  =  3  ->  (
4  -  k )  =  ( 4  -  3 ) )
6463oveq1d 5889 . . . . . . . . . 10  |-  ( k  =  3  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  3 )  +  1 ) )
654, 6, 5, 7subaddrii 9151 . . . . . . . . . . . 12  |-  ( 4  -  3 )  =  1
6665oveq1i 5884 . . . . . . . . . . 11  |-  ( ( 4  -  3 )  +  1 )  =  ( 1  +  1 )
67 df-2 9820 . . . . . . . . . . 11  |-  2  =  ( 1  +  1 )
6866, 67eqtr4i 2319 . . . . . . . . . 10  |-  ( ( 4  -  3 )  +  1 )  =  2
6964, 68syl6eq 2344 . . . . . . . . 9  |-  ( k  =  3  ->  (
( 4  -  k
)  +  1 )  =  2 )
7062, 69oveq12d 5892 . . . . . . . 8  |-  ( k  =  3  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 3 BernPoly  X
)  /  2 ) )
7161, 70oveq12d 5892 . . . . . . 7  |-  ( k  =  3  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 3 BernPoly  X )  /  2
) ) )
7258, 71sylbir 204 . . . . . 6  |-  ( k  =  ( 2  +  1 )  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 3 BernPoly  X )  /  2
) ) )
7317, 57, 72fsump1 12235 . . . . 5  |-  ( 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
) ) ) )
7467oveq2i 5885 . . . . . . . 8  |-  ( 0 ... 2 )  =  ( 0 ... (
1  +  1 ) )
7574sumeq1i 12187 . . . . . . 7  |-  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 ) ) )
76 1nn0 9997 . . . . . . . . . . 11  |-  1  e.  NN0
7776, 15eleqtri 2368 . . . . . . . . . 10  |-  1  e.  ( ZZ>= `  0 )
7877a1i 10 . . . . . . . . 9  |-  ( X  e.  CC  ->  1  e.  ( ZZ>= `  0 )
)
79 fzssp1 10850 . . . . . . . . . . . 12  |-  ( 0 ... ( 1  +  1 ) )  C_  ( 0 ... (
( 1  +  1 )  +  1 ) )
8067oveq1i 5884 . . . . . . . . . . . . 13  |-  ( 2  +  1 )  =  ( ( 1  +  1 )  +  1 )
8180oveq2i 5885 . . . . . . . . . . . 12  |-  ( 0 ... ( 2  +  1 ) )  =  ( 0 ... (
( 1  +  1 )  +  1 ) )
8279, 81sseqtr4i 3224 . . . . . . . . . . 11  |-  ( 0 ... ( 1  +  1 ) )  C_  ( 0 ... (
2  +  1 ) )
8382sseli 3189 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 1  +  1 ) )  ->  k  e.  ( 0 ... (
2  +  1 ) ) )
8483, 57sylan2 460 . . . . . . . . 9  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 1  +  1 ) ) )  ->  ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  e.  CC )
8567eqeq2i 2306 . . . . . . . . . 10  |-  ( k  =  2  <->  k  =  ( 1  +  1 ) )
86 oveq2 5882 . . . . . . . . . . . 12  |-  ( k  =  2  ->  (
4  _C  k )  =  ( 4  _C  2 ) )
87 4bc2eq6 24114 . . . . . . . . . . . 12  |-  ( 4  _C  2 )  =  6
8886, 87syl6eq 2344 . . . . . . . . . . 11  |-  ( k  =  2  ->  (
4  _C  k )  =  6 )
89 oveq1 5881 . . . . . . . . . . . 12  |-  ( k  =  2  ->  (
k BernPoly  X )  =  ( 2 BernPoly  X ) )
90 oveq2 5882 . . . . . . . . . . . . . 14  |-  ( k  =  2  ->  (
4  -  k )  =  ( 4  -  2 ) )
9190oveq1d 5889 . . . . . . . . . . . . 13  |-  ( k  =  2  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  2 )  +  1 ) )
92 2cn 9832 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
93 2p2e4 9858 . . . . . . . . . . . . . . . 16  |-  ( 2  +  2 )  =  4
944, 92, 92, 93subaddrii 9151 . . . . . . . . . . . . . . 15  |-  ( 4  -  2 )  =  2
9594oveq1i 5884 . . . . . . . . . . . . . 14  |-  ( ( 4  -  2 )  +  1 )  =  ( 2  +  1 )
9695, 10eqtr4i 2319 . . . . . . . . . . . . 13  |-  ( ( 4  -  2 )  +  1 )  =  3
9791, 96syl6eq 2344 . . . . . . . . . . . 12  |-  ( k  =  2  ->  (
( 4  -  k
)  +  1 )  =  3 )
9889, 97oveq12d 5892 . . . . . . . . . . 11  |-  ( k  =  2  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 2 BernPoly  X
)  /  3 ) )
9988, 98oveq12d 5892 . . . . . . . . . 10  |-  ( k  =  2  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 6  x.  ( ( 2 BernPoly  X )  /  3
) ) )
10085, 99sylbir 204 . . . . . . . . 9  |-  ( k  =  ( 1  +  1 )  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 6  x.  ( ( 2 BernPoly  X )  /  3
) ) )
10178, 84, 100fsump1 12235 . . . . . . . 8  |-  ( 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
) ) ) )
102 0p1e1 9855 . . . . . . . . . . . 12  |-  ( 0  +  1 )  =  1
103102oveq2i 5885 . . . . . . . . . . 11  |-  ( 0 ... ( 0  +  1 ) )  =  ( 0 ... 1
)
104103sumeq1i 12187 . . . . . . . . . 10  |-  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 ) ) )
105 0nn0 9996 . . . . . . . . . . . . . 14  |-  0  e.  NN0
106105, 15eleqtri 2368 . . . . . . . . . . . . 13  |-  0  e.  ( ZZ>= `  0 )
107106a1i 10 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  0  e.  ( ZZ>= `  0 )
)
108 3nn 9894 . . . . . . . . . . . . . . . . 17  |-  3  e.  NN
109 nnuz 10279 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
110108, 109eleqtri 2368 . . . . . . . . . . . . . . . 16  |-  3  e.  ( ZZ>= `  1 )
111 fzss2 10847 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  ( ZZ>= `  1
)  ->  ( 0 ... 1 )  C_  ( 0 ... 3
) )
112110, 111ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 0 ... 1 )  C_  ( 0 ... 3
)
113 2p1e3 9863 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  3
114113oveq2i 5885 . . . . . . . . . . . . . . 15  |-  ( 0 ... ( 2  +  1 ) )  =  ( 0 ... 3
)
115112, 103, 1143sstr4i 3230 . . . . . . . . . . . . . 14  |-  ( 0 ... ( 0  +  1 ) )  C_  ( 0 ... (
2  +  1 ) )
116115sseli 3189 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... ( 0  +  1 ) )  ->  k  e.  ( 0 ... (
2  +  1 ) ) )
117116, 57sylan2 460 . . . . . . . . . . . 12  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 0  +  1 ) ) )  ->  ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  e.  CC )
118102eqeq2i 2306 . . . . . . . . . . . . 13  |-  ( k  =  ( 0  +  1 )  <->  k  = 
1 )
119 oveq2 5882 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
4  _C  k )  =  ( 4  _C  1 ) )
120 bcn1 11341 . . . . . . . . . . . . . . . 16  |-  ( 4  e.  NN0  ->  ( 4  _C  1 )  =  4 )
1211, 120ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 4  _C  1 )  =  4
122119, 121syl6eq 2344 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
4  _C  k )  =  4 )
123 oveq1 5881 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k BernPoly  X )  =  ( 1 BernPoly  X ) )
124 oveq2 5882 . . . . . . . . . . . . . . . . 17  |-  ( k  =  1  ->  (
4  -  k )  =  ( 4  -  1 ) )
125124oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( k  =  1  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  1 )  +  1 ) )
1269oveq1i 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( 4  -  1 )  +  1 )  =  ( 3  +  1 )
127 df-4 9822 . . . . . . . . . . . . . . . . 17  |-  4  =  ( 3  +  1 )
128126, 127eqtr4i 2319 . . . . . . . . . . . . . . . 16  |-  ( ( 4  -  1 )  +  1 )  =  4
129125, 128syl6eq 2344 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
( 4  -  k
)  +  1 )  =  4 )
130123, 129oveq12d 5892 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 1 BernPoly  X
)  /  4 ) )
131122, 130oveq12d 5892 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 1 BernPoly  X )  /  4
) ) )
132118, 131sylbi 187 . . . . . . . . . . . 12  |-  ( k  =  ( 0  +  1 )  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 1 BernPoly  X )  /  4
) ) )
133107, 117, 132fsump1 12235 . . . . . . . . . . 11  |-  ( 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
) ) ) )
134 0z 10051 . . . . . . . . . . . . . 14  |-  0  e.  ZZ
1355a1i 10 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  1  e.  CC )
136 bpolycl 24859 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  NN0  /\  X  e.  CC )  ->  ( 0 BernPoly  X )  e.  CC )
137105, 136mpan 651 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  (
0 BernPoly  X )  e.  CC )
138 5re 9837 . . . . . . . . . . . . . . . . . 18  |-  5  e.  RR
139138recni 8865 . . . . . . . . . . . . . . . . 17  |-  5  e.  CC
140139a1i 10 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  5  e.  CC )
141 0re 8854 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
142 5pos 9849 . . . . . . . . . . . . . . . . . 18  |-  0  <  5
143141, 142gtneii 8946 . . . . . . . . . . . . . . . . 17  |-  5  =/=  0
144143a1i 10 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  5  =/=  0 )
145137, 140, 144divcld 9552 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 0 BernPoly  X )  /  5 )  e.  CC )
146135, 145mulcld 8871 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
1  x.  ( ( 0 BernPoly  X )  /  5
) )  e.  CC )
147 oveq2 5882 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  (
4  _C  k )  =  ( 4  _C  0 ) )
148 bcn0 11339 . . . . . . . . . . . . . . . . . 18  |-  ( 4  e.  NN0  ->  ( 4  _C  0 )  =  1 )
1491, 148ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( 4  _C  0 )  =  1
150147, 149syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
4  _C  k )  =  1 )
151 oveq1 5881 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  (
k BernPoly  X )  =  ( 0 BernPoly  X ) )
152 oveq2 5882 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  (
4  -  k )  =  ( 4  -  0 ) )
153152oveq1d 5889 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  0 )  +  1 ) )
1544subid1i 9134 . . . . . . . . . . . . . . . . . . . 20  |-  ( 4  -  0 )  =  4
155154oveq1i 5884 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 4  -  0 )  +  1 )  =  ( 4  +  1 )
156 4p1e5 9865 . . . . . . . . . . . . . . . . . . 19  |-  ( 4  +  1 )  =  5
157155, 156eqtri 2316 . . . . . . . . . . . . . . . . . 18  |-  ( ( 4  -  0 )  +  1 )  =  5
158153, 157syl6eq 2344 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  (
( 4  -  k
)  +  1 )  =  5 )
159151, 158oveq12d 5892 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 0 BernPoly  X
)  /  5 ) )
160150, 159oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 1  x.  ( ( 0 BernPoly  X )  /  5
) ) )
161160fsum1 12230 . . . . . . . . . . . . . 14  |-  ( ( 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
) ) )
162134, 146, 161sylancr 644 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  sum_ k  e.  ( 0 ... 0
) ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  =  ( 1  x.  ( ( 0 BernPoly  X )  /  5
) ) )
163 bpoly0 24857 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  (
0 BernPoly  X )  =  1 )
164163oveq1d 5889 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 0 BernPoly  X )  /  5 )  =  ( 1  /  5
) )
165164oveq2d 5890 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
1  x.  ( ( 0 BernPoly  X )  /  5
) )  =  ( 1  x.  ( 1  /  5 ) ) )
166139, 143reccli 9506 . . . . . . . . . . . . . . 15  |-  ( 1  /  5 )  e.  CC
167166mulid2i 8856 . . . . . . . . . . . . . 14  |-  ( 1  x.  ( 1  / 
5 ) )  =  ( 1  /  5
)
168165, 167syl6eq 2344 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
1  x.  ( ( 0 BernPoly  X )  /  5
) )  =  ( 1  /  5 ) )
169162, 168eqtrd 2328 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  sum_ k  e.  ( 0 ... 0
) ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  =  ( 1  /  5 ) )
170 bpolycl 24859 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  NN0  /\  X  e.  CC )  ->  ( 1 BernPoly  X )  e.  CC )
17176, 170mpan 651 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
1 BernPoly  X )  e.  CC )
172 nn0cn 9991 . . . . . . . . . . . . . . 15  |-  ( 4  e.  NN0  ->  4  e.  CC )
1731, 172mp1i 11 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  4  e.  CC )
174 4pos 9848 . . . . . . . . . . . . . . . 16  |-  0  <  4
175141, 174gtneii 8946 . . . . . . . . . . . . . . 15  |-  4  =/=  0
176175a1i 10 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  4  =/=  0 )
177171, 173, 176divcan2d 9554 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
4  x.  ( ( 1 BernPoly  X )  /  4
) )  =  ( 1 BernPoly  X ) )
178 bpoly1 24858 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
1 BernPoly  X )  =  ( X  -  ( 1  /  2 ) ) )
179177, 178eqtrd 2328 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
4  x.  ( ( 1 BernPoly  X )  /  4
) )  =  ( X  -  ( 1  /  2 ) ) )
180169, 179oveq12d 5892 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
181133, 180eqtrd 2328 . . . . . . . . . 10  |-  ( X  e.  CC  ->  sum_ k  e.  ( 0 ... (
0  +  1 ) ) ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  =  ( ( 1  /  5 )  +  ( X  -  ( 1  /  2
) ) ) )
182104, 181syl5eqr 2342 . . . . . . . . 9  |-  ( X  e.  CC  ->  sum_ k  e.  ( 0 ... 1
) ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  =  ( ( 1  /  5 )  +  ( X  -  ( 1  /  2
) ) ) )
183 6re 9838 . . . . . . . . . . . . 13  |-  6  e.  RR
184183recni 8865 . . . . . . . . . . . 12  |-  6  e.  CC
185184a1i 10 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  6  e.  CC )
186 bpolycl 24859 . . . . . . . . . . . 12  |-  ( ( 2  e.  NN0  /\  X  e.  CC )  ->  ( 2 BernPoly  X )  e.  CC )
18714, 186mpan 651 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
2 BernPoly  X )  e.  CC )
1886a1i 10 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  3  e.  CC )
189 3ne0 9847 . . . . . . . . . . . 12  |-  3  =/=  0
190189a1i 10 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  3  =/=  0 )
191185, 187, 188, 190div12d 9588 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
6  x.  ( ( 2 BernPoly  X )  /  3
) )  =  ( ( 2 BernPoly  X )  x.  ( 6  / 
3 ) ) )
192 3t2e6 9888 . . . . . . . . . . . . 13  |-  ( 3  x.  2 )  =  6
193184, 6, 92, 189divmuli 9530 . . . . . . . . . . . . 13  |-  ( ( 6  /  3 )  =  2  <->  ( 3  x.  2 )  =  6 )
194192, 193mpbir 200 . . . . . . . . . . . 12  |-  ( 6  /  3 )  =  2
195194oveq2i 5885 . . . . . . . . . . 11  |-  ( ( 2 BernPoly  X )  x.  (
6  /  3 ) )  =  ( ( 2 BernPoly  X )  x.  2 )
19692a1i 10 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  2  e.  CC )
197187, 196mulcomd 8872 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 2 BernPoly  X )  x.  2 )  =  ( 2  x.  ( 2 BernPoly  X ) ) )
198 bpoly2 24864 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
2 BernPoly  X )  =  ( ( ( X ^
2 )  -  X
)  +  ( 1  /  6 ) ) )
199198oveq2d 5890 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
2  x.  ( 2 BernPoly  X ) )  =  ( 2  x.  (
( ( X ^
2 )  -  X
)  +  ( 1  /  6 ) ) ) )
200197, 199eqtrd 2328 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( 2 BernPoly  X )  x.  2 )  =  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) ) )
201195, 200syl5eq 2340 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( 2 BernPoly  X )  x.  ( 6  /  3
) )  =  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) ) )
202191, 201eqtrd 2328 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
6  x.  ( ( 2 BernPoly  X )  /  3
) )  =  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) ) )
203182, 202oveq12d 5892 . . . . . . . 8  |-  ( 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 ) ) ) ) )
204101, 203eqtrd 2328 . . . . . . 7  |-  ( 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 ) ) ) ) )
20575, 204syl5eq 2340 . . . . . 6  |-  ( 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 ) ) ) ) )
206 3nn0 9999 . . . . . . . . 9  |-  3  e.  NN0
207 bpolycl 24859 . . . . . . . . 9  |-  ( ( 3  e.  NN0  /\  X  e.  CC )  ->  ( 3 BernPoly  X )  e.  CC )
208206, 207mpan 651 . . . . . . . 8  |-  ( X  e.  CC  ->  (
3 BernPoly  X )  e.  CC )
209 2ne0 9845 . . . . . . . . 9  |-  2  =/=  0
210209a1i 10 . . . . . . . 8  |-  ( X  e.  CC  ->  2  =/=  0 )
211173, 208, 196, 210div12d 9588 . . . . . . 7  |-  ( X  e.  CC  ->  (
4  x.  ( ( 3 BernPoly  X )  /  2
) )  =  ( ( 3 BernPoly  X )  x.  ( 4  / 
2 ) ) )
212 4d2e2 9892 . . . . . . . . 9  |-  ( 4  /  2 )  =  2
213212oveq2i 5885 . . . . . . . 8  |-  ( ( 3 BernPoly  X )  x.  (
4  /  2 ) )  =  ( ( 3 BernPoly  X )  x.  2 )
214208, 196mulcomd 8872 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( 3 BernPoly  X )  x.  2 )  =  ( 2  x.  ( 3 BernPoly  X ) ) )
215 bpoly3 24865 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
3 BernPoly  X )  =  ( ( ( X ^
3 )  -  (
( 3  /  2
)  x.  ( X ^ 2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) )
216215oveq2d 5890 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
2  x.  ( 3 BernPoly  X ) )  =  ( 2  x.  (
( ( X ^
3 )  -  (
( 3  /  2
)  x.  ( X ^ 2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) ) )
217214, 216eqtrd 2328 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( 3 BernPoly  X )  x.  2 )  =  ( 2  x.  ( ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) ) )
218213, 217syl5eq 2340 . . . . . . 7  |-  ( X  e.  CC  ->  (
( 3 BernPoly  X )  x.  ( 4  /  2
) )  =  ( 2  x.  ( ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) ) )
219211, 218eqtrd 2328 . . . . . 6  |-  ( X  e.  CC  ->  (
4  x.  ( ( 3 BernPoly  X )  /  2
) )  =  ( 2  x.  ( ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) ) )
220205, 219oveq12d 5892 . . . . 5  |-  ( 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 ) ) ) ) )
22173, 220eqtrd 2328 . . . 4  |-  ( 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 ) ) ) ) )
22213, 221syl5eq 2340 . . 3  |-  ( 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 ) ) ) ) )
223222oveq2d 5890 . 2  |-  ( 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 ) ) ) ) ) )
224 expcl 11137 . . . . 5  |-  ( ( X  e.  CC  /\  4  e.  NN0 )  -> 
( X ^ 4 )  e.  CC )
2251, 224mpan2 652 . . . 4  |-  ( X  e.  CC  ->  ( X ^ 4 )  e.  CC )
226 expcl 11137 . . . . . 6  |-  ( ( X  e.  CC  /\  3  e.  NN0 )  -> 
( X ^ 3 )  e.  CC )
227206, 226mpan2 652 . . . . 5  |-  ( X  e.  CC  ->  ( X ^ 3 )  e.  CC )
228196, 227mulcld 8871 . . . 4  |-  ( X  e.  CC  ->  (
2  x.  ( X ^ 3 ) )  e.  CC )
229 sqcl 11182 . . . . 5  |-  ( X  e.  CC  ->  ( X ^ 2 )  e.  CC )
230206, 105deccl 10154 . . . . . . . 8  |- ; 3 0  e.  NN0
231230nn0cni 9993 . . . . . . 7  |- ; 3 0  e.  CC
232 df-dec 10141 . . . . . . . . 9  |- ; 3 0  =  ( ( 10  x.  3 )  +  0 )
233 10re 9842 . . . . . . . . . . . 12  |-  10  e.  RR
234233recni 8865 . . . . . . . . . . 11  |-  10  e.  CC
235234, 6mulcli 8858 . . . . . . . . . 10  |-  ( 10  x.  3 )  e.  CC
236235addid1i 9015 . . . . . . . . 9  |-  ( ( 10  x.  3 )  +  0 )  =  ( 10  x.  3 )
237232, 236eqtri 2316 . . . . . . . 8  |- ; 3 0  =  ( 10  x.  3 )
238 10pos 9854 . . . . . . . . . 10  |-  0  <  10
239141, 238gtneii 8946 . . . . . . . . 9  |-  10  =/=  0
240234, 6, 239, 189mulne0i 9427 . . . . . . . 8  |-  ( 10  x.  3 )  =/=  0
241237, 240eqnetri 2476 . . . . . . 7  |- ; 3 0  =/=  0
242231, 241reccli 9506 . . . . . 6  |-  ( 1  / ; 3 0 )  e.  CC
243242a1i 10 . . . . 5  |-  ( X  e.  CC  ->  (
1  / ; 3 0 )  e.  CC )
244229, 243subcld 9173 . . . 4  |-  ( X  e.  CC  ->  (
( X ^ 2 )  -  ( 1  / ; 3 0 ) )  e.  CC )
245225, 228, 244subsubd 9201 . . 3  |-  ( 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 ) ) ) )
246166a1i 10 . . . . . . . 8  |-  ( X  e.  CC  ->  (
1  /  5 )  e.  CC )
247 id 19 . . . . . . . . 9  |-  ( X  e.  CC  ->  X  e.  CC )
24892, 209reccli 9506 . . . . . . . . . 10  |-  ( 1  /  2 )  e.  CC
249248a1i 10 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
1  /  2 )  e.  CC )
250247, 249subcld 9173 . . . . . . . 8  |-  ( X  e.  CC  ->  ( X  -  ( 1  /  2 ) )  e.  CC )
251246, 250addcld 8870 . . . . . . 7  |-  ( X  e.  CC  ->  (
( 1  /  5
)  +  ( X  -  ( 1  / 
2 ) ) )  e.  CC )
252229, 247subcld 9173 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( X ^ 2 )  -  X )  e.  CC )
253 6pos 9850 . . . . . . . . . . . 12  |-  0  <  6
254141, 253gtneii 8946 . . . . . . . . . . 11  |-  6  =/=  0
255184, 254reccli 9506 . . . . . . . . . 10  |-  ( 1  /  6 )  e.  CC
256255a1i 10 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
1  /  6 )  e.  CC )
257252, 256addcld 8870 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( ( X ^
2 )  -  X
)  +  ( 1  /  6 ) )  e.  CC )
258196, 257mulcld 8871 . . . . . . 7  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) )  e.  CC )
259251, 258addcld 8870 . . . . . 6  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  +  ( X  -  ( 1  /  2 ) ) )  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6
) ) ) )  e.  CC )
2606, 92, 209divcli 9518 . . . . . . . . . . 11  |-  ( 3  /  2 )  e.  CC
261260a1i 10 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
3  /  2 )  e.  CC )
262261, 229mulcld 8871 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( 3  /  2
)  x.  ( X ^ 2 ) )  e.  CC )
263227, 262subcld 9173 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  e.  CC )
264249, 247mulcld 8871 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( 1  /  2
)  x.  X )  e.  CC )
265263, 264addcld 8870 . . . . . . 7  |-  ( X  e.  CC  ->  (
( ( X ^
3 )  -  (
( 3  /  2
)  x.  ( X ^ 2 ) ) )  +  ( ( 1  /  2 )  x.  X ) )  e.  CC )
266196, 265mulcld 8871 . . . . . 6  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) )  e.  CC )
267259, 266addcomd 9030 . . . . 5  |-  ( 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 ) ) ) ) ) )
268196, 263, 264adddid 8875 . . . . . . 7  |-  ( 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 ) ) ) )
269196, 227, 262subdid 9251 . . . . . . . 8  |-  ( X  e.  CC  ->  (
2  x.  ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^ 2 ) ) ) )  =  ( ( 2  x.  ( X ^
3 ) )  -  ( 2  x.  (
( 3  /  2
)  x.  ( X ^ 2 ) ) ) ) )
27092, 209recidi 9507 . . . . . . . . . 10  |-  ( 2  x.  ( 1  / 
2 ) )  =  1
271270oveq1i 5884 . . . . . . . . 9  |-  ( ( 2  x.  ( 1  /  2 ) )  x.  X )  =  ( 1  x.  X
)
272196, 249, 247mulassd 8874 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( 2  x.  (
1  /  2 ) )  x.  X )  =  ( 2  x.  ( ( 1  / 
2 )  x.  X
) ) )
273 mulid2 8852 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
1  x.  X )  =  X )
274271, 272, 2733eqtr3a 2352 . . . . . . . 8  |-  ( X  e.  CC  ->  (
2  x.  ( ( 1  /  2 )  x.  X ) )  =  X )
275269, 274oveq12d 5892 . . . . . . 7  |-  ( 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
) )
276268, 275eqtrd 2328 . . . . . 6  |-  ( 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
) )
277276oveq1d 5889 . . . . 5  |-  ( 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 ) ) ) ) ) )
278196, 262mulcld 8871 . . . . . . . 8  |-  ( X  e.  CC  ->  (
2  x.  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  e.  CC )
279228, 278subcld 9173 . . . . . . 7  |-  ( X  e.  CC  ->  (
( 2  x.  ( X ^ 3 ) )  -  ( 2  x.  ( ( 3  / 
2 )  x.  ( X ^ 2 ) ) ) )  e.  CC )
280279, 247, 259addassd 8873 . . . . . 6  |-  ( 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 ) ) ) ) ) ) )
281247, 259addcld 8870 . . . . . . 7  |-  ( X  e.  CC  ->  ( X  +  ( (
( 1  /  5
)  +  ( X  -  ( 1  / 
2 ) ) )  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6 ) ) ) ) )  e.  CC )
282228, 278, 281subsubd 9201 . . . . . 6  |-  ( 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 ) ) ) ) ) ) )
2836, 92, 209divcan2i 9519 . . . . . . . . . . 11  |-  ( 2  x.  ( 3  / 
2 ) )  =  3
284283oveq1i 5884 . . . . . . . . . 10  |-  ( ( 2  x.  ( 3  /  2 ) )  x.  ( X ^
2 ) )  =  ( 3  x.  ( X ^ 2 ) )
285196, 261, 229mulassd 8874 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( 2  x.  (
3  /  2 ) )  x.  ( X ^ 2 ) )  =  ( 2  x.  ( ( 3  / 
2 )  x.  ( X ^ 2 ) ) ) )
286284, 285syl5reqr 2343 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
2  x.  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  =  ( 3  x.  ( X ^ 2 ) ) )
287286oveq1d 5889 . . . . . . . 8  |-  ( 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
) ) ) ) ) ) )
288247, 251, 258add12d 9049 . . . . . . . . . 10  |-  ( 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 ) ) ) ) ) )
289196, 252, 256adddid 8875 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) )  =  ( ( 2  x.  ( ( X ^ 2 )  -  X ) )  +  ( 2  x.  (
1  /  6 ) ) ) )
290196, 229, 247subdid 9251 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
2  x.  ( ( X ^ 2 )  -  X ) )  =  ( ( 2  x.  ( X ^
2 ) )  -  ( 2  x.  X
) ) )
291192oveq2i 5885 . . . . . . . . . . . . . . . . 17  |-  ( 2  /  ( 3  x.  2 ) )  =  ( 2  /  6
)
2926, 189reccli 9506 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  3 )  e.  CC
2936, 92, 292mul32i 9024 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  x.  2 )  x.  ( 1  / 
3 ) )  =  ( ( 3  x.  ( 1  /  3
) )  x.  2 )
2946, 189recidi 9507 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 3  x.  ( 1  / 
3 ) )  =  1
295294oveq1i 5884 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 3  x.  ( 1  /  3 ) )  x.  2 )  =  ( 1  x.  2 )
29692mulid2i 8856 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  x.  2 )  =  2
297295, 296eqtri 2316 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  x.  ( 1  /  3 ) )  x.  2 )  =  2
298293, 297eqtri 2316 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  x.  2 )  x.  ( 1  / 
3 ) )  =  2
299192, 184eqeltri 2366 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  x.  2 )  e.  CC
300192, 254eqnetri 2476 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  x.  2 )  =/=  0
30192, 299, 292, 300divmuli 9530 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  /  ( 3  x.  2 ) )  =  ( 1  / 
3 )  <->  ( (
3  x.  2 )  x.  ( 1  / 
3 ) )  =  2 )
302298, 301mpbir 200 . . . . . . . . . . . . . . . . 17  |-  ( 2  /  ( 3  x.  2 ) )  =  ( 1  /  3
)
30392, 184, 254divreci 9521 . . . . . . . . . . . . . . . . 17  |-  ( 2  /  6 )  =  ( 2  x.  (
1  /  6 ) )
304291, 302, 3033eqtr3ri 2325 . . . . . . . . . . . . . . . 16  |-  ( 2  x.  ( 1  / 
6 ) )  =  ( 1  /  3
)
305304a1i 10 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
2  x.  ( 1  /  6 ) )  =  ( 1  / 
3 ) )
306290, 305oveq12d 5892 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
( 2  x.  (
( X ^ 2 )  -  X ) )  +  ( 2  x.  ( 1  / 
6 ) ) )  =  ( ( ( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) )  +  ( 1  /  3
) ) )
307289, 306eqtrd 2328 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) )  =  ( ( ( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) )  +  ( 1  /  3
) ) )
308307oveq2d 5890 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  ( X  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6
) ) ) )  =  ( X  +  ( ( ( 2  x.  ( X ^
2 ) )  -  ( 2  x.  X
) )  +  ( 1  /  3 ) ) ) )
309196, 229mulcld 8871 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
2  x.  ( X ^ 2 ) )  e.  CC )
310196, 247mulcld 8871 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
2  x.  X )  e.  CC )
311309, 310subcld 9173 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) )  e.  CC )
312292a1i 10 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
1  /  3 )  e.  CC )
313247, 311, 312addassd 8873 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( X  +  ( ( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) ) )  +  ( 1  / 
3 ) )  =  ( X  +  ( ( ( 2  x.  ( X ^ 2 ) )  -  (
2  x.  X ) )  +  ( 1  /  3 ) ) ) )
314247, 309, 310addsub12d 9196 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  ( X  +  ( (
2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) ) )  =  ( ( 2  x.  ( X ^
2 ) )  +  ( X  -  (
2  x.  X ) ) ) )
315314oveq1d 5889 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( X  +  ( ( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) ) )  +  ( 1  / 
3 ) )  =  ( ( ( 2  x.  ( X ^
2 ) )  +  ( X  -  (
2  x.  X ) ) )  +  ( 1  /  3 ) ) )
316308, 313, 3153eqtr2d 2334 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  ( X  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6
) ) ) )  =  ( ( ( 2  x.  ( X ^ 2 ) )  +  ( X  -  ( 2  x.  X
) ) )  +  ( 1  /  3
) ) )
317316oveq2d 5890 . . . . . . . . . 10  |-  ( 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 ) ) ) )
318288, 317eqtrd 2328 . . . . . . . . 9  |-  ( 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 ) ) ) )
319318oveq2d 5890 . . . . . . . 8  |-  ( 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
) ) ) ) )
320247, 310subcld 9173 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  ( X  -  ( 2  x.  X ) )  e.  CC )
321309, 320addcld 8870 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 2  x.  ( X ^ 2 ) )  +  ( X  -  ( 2  x.  X
) ) )  e.  CC )
322246, 250, 321, 312add4d 9051 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
323246, 309, 320add12d 9049 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 1  /  5
)  +  ( ( 2  x.  ( X ^ 2 ) )  +  ( X  -  ( 2  x.  X
) ) ) )  =  ( ( 2  x.  ( X ^
2 ) )  +  ( ( 1  / 
5 )  +  ( X  -  ( 2  x.  X ) ) ) ) )
324323oveq1d 5889 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
325246, 320addcld 8870 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 1  /  5
)  +  ( X  -  ( 2  x.  X ) ) )  e.  CC )
326250, 312addcld 8870 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( X  -  (
1  /  2 ) )  +  ( 1  /  3 ) )  e.  CC )
327309, 325, 326addassd 8873 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
328322, 324, 3273eqtrd 2332 . . . . . . . . . 10  |-  ( 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 ) ) ) ) )
329328oveq2d 5890 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
330188, 229mulcld 8871 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
3  x.  ( X ^ 2 ) )  e.  CC )
331325, 326addcld 8870 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  +  ( X  -  ( 2  x.  X ) ) )  +  ( ( X  -  ( 1  /  2 ) )  +  ( 1  / 
3 ) ) )  e.  CC )
332330, 309, 331subsub4d 9204 . . . . . . . . 9  |-  ( 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 ) ) ) ) ) )
3336, 92, 5, 113subaddrii 9151 . . . . . . . . . . . 12  |-  ( 3  -  2 )  =  1
334333oveq1i 5884 . . . . . . . . . . 11  |-  ( ( 3  -  2 )  x.  ( X ^
2 ) )  =  ( 1  x.  ( X ^ 2 ) )
335188, 196, 229subdird 9252 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( 3  -  2 )  x.  ( X ^ 2 ) )  =  ( ( 3  x.  ( X ^
2 ) )  -  ( 2  x.  ( X ^ 2 ) ) ) )
336229mulid2d 8869 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
1  x.  ( X ^ 2 ) )  =  ( X ^
2 ) )
337334, 335, 3363eqtr3a 2352 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( 3  x.  ( X ^ 2 ) )  -  ( 2  x.  ( X ^ 2 ) ) )  =  ( X ^ 2 ) )
338246, 310, 247subsubd 9201 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 1  /  5
)  -  ( ( 2  x.  X )  -  X ) )  =  ( ( ( 1  /  5 )  -  ( 2  x.  X ) )  +  X ) )
339273oveq2d 5890 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 2  x.  X
)  -  ( 1  x.  X ) )  =  ( ( 2  x.  X )  -  X ) )
340 1p1e2 9856 . . . . . . . . . . . . . . . . . 18  |-  ( 1  +  1 )  =  2
34192, 5, 5, 340subaddrii 9151 . . . . . . . . . . . . . . . . 17  |-  ( 2  -  1 )  =  1
342341oveq1i 5884 . . . . . . . . . . . . . . . 16  |-  ( ( 2  -  1 )  x.  X )  =  ( 1  x.  X
)
343196, 135, 247subdird 9252 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  (
( 2  -  1 )  x.  X )  =  ( ( 2  x.  X )  -  ( 1  x.  X
) ) )
344342, 343, 2733eqtr3a 2352 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 2  x.  X
)  -  ( 1  x.  X ) )  =  X )
345339, 344eqtr3d 2330 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
( 2  x.  X
)  -  X )  =  X )
346345oveq2d 5890 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 1  /  5
)  -  ( ( 2  x.  X )  -  X ) )  =  ( ( 1  /  5 )  -  X ) )
347246, 310, 247subadd23d 9195 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  (
2  x.  X ) )  +  X )  =  ( ( 1  /  5 )  +  ( X  -  (
2  x.  X ) ) ) )
348338, 346, 3473eqtr3d 2336 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 1  /  5
)  -  X )  =  ( ( 1  /  5 )  +  ( X  -  (
2  x.  X ) ) ) )
349247, 249, 312subsubd 9201 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  ( X  -  ( (
1  /  2 )  -  ( 1  / 
3 ) ) )  =  ( ( X  -  ( 1  / 
2 ) )  +  ( 1  /  3
) ) )
350348, 349oveq12d 5892 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  X
)  +  ( X  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) ) )  =  ( ( ( 1  /  5 )  +  ( X  -  ( 2  x.  X
) ) )  +  ( ( X  -  ( 1  /  2
) )  +  ( 1  /  3 ) ) ) )
351248, 292subcli 9138 . . . . . . . . . . . . . 14  |-  ( ( 1  /  2 )  -  ( 1  / 
3 ) )  e.  CC
352351a1i 10 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 1  /  2
)  -  ( 1  /  3 ) )  e.  CC )
353246, 247, 352npncand 9197 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  X
)  +  ( X  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) ) )  =  ( ( 1  /  5 )  -  ( ( 1  / 
2 )  -  (
1  /  3 ) ) ) )
354 halfthird 24115 . . . . . . . . . . . . . 14  |-  ( ( 1  /  2 )  -  ( 1  / 
3 ) )  =  ( 1  /  6
)
355354oveq2i 5885 . . . . . . . . . . . . 13  |-  ( ( 1  /  5 )  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) )  =  ( ( 1  / 
5 )  -  (
1  /  6 ) )
356 5recm6rec 24116 . . . . . . . . . . . . 13  |-  ( ( 1  /  5 )  -  ( 1  / 
6 ) )  =  ( 1  / ; 3 0 )
357355, 356eqtri 2316 . . . . . . . . . . . 12  |-  ( ( 1  /  5 )  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) )  =  ( 1  / ; 3 0 )
358353, 357syl6eq 2344 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  X
)  +  ( X  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) ) )  =  ( 1  / ; 3 0 ) )
359350, 358eqtr3d 2330 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  +  ( X  -  ( 2  x.  X ) ) )  +  ( ( X  -  ( 1  /  2 ) )  +  ( 1  / 
3 ) ) )  =  ( 1  / ; 3 0 ) )
360337, 359oveq12d 5892 . . . . . . . . 9  |-  ( 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 ) ) )
361329, 332, 3603eqtr2d 2334 . . . . . . . 8  |-  ( 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 ) ) )
362287, 319, 3613eqtrd 2332 . . . . . . 7  |-  ( 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 ) ) )
363362oveq2d 5890 . . . . . 6  |-  ( 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 ) ) ) )
364280, 282, 3633eqtr2d 2334 . . . . 5  |-  ( 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 ) ) ) )
365267, 277, 3643eqtrd 2332 . . . 4  |-  ( 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 ) ) ) )
366365oveq2d 5890 . . 3  |-  ( 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 ) ) ) ) )
367225, 228subcld 9173 . . . 4  |-  ( X  e.  CC  ->  (
( X ^ 4 )  -  ( 2  x.  ( X ^
3 ) ) )  e.  CC )
368367, 229, 243addsubassd 9193 . . 3  |-  ( 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 ) ) ) )
369245, 366, 3683eqtr4d 2338 . 2  |-  ( 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 ) ) )
3703, 223, 3693eqtrd 2332 1  |-  ( X  e.  CC  ->  (
4 BernPoly  X )  =  ( ( ( ( X ^ 4 )  -  ( 2  x.  ( X ^ 3 ) ) )  +  ( X ^ 2 ) )  -  ( 1  / ; 3 0 ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459    C_ wss 3165   class class class wbr 4039   ` cfv 5271  (class class class)co 5874   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    < clt 8883    - cmin 9053    / cdiv 9439   NNcn 9762   2c2 9811   3c3 9812   4c4 9813   5c5 9814   6c6 9815   10c10 9819   NN0cn0 9981   ZZcz 10040  ;cdc 10140   ZZ>=cuz 10246   ...cfz 10798   ^cexp 11120    _C cbc 11331   sum_csu 12174   BernPoly cbp 24853
This theorem is referenced by:  fsumcube  24867
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-oadd 6499  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-sup 7210  df-oi 7241  df-card 7588  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-4 9822  df-5 9823  df-6 9824  df-7 9825  df-8 9826  df-9 9827  df-10 9828  df-n0 9982  df-z 10041  df-dec 10141  df-uz 10247  df-rp 10371  df-fz 10799  df-fzo 10887  df-seq 11063  df-exp 11121  df-fac 11305  df-bc 11332  df-hash 11354  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-clim 11978  df-sum 12175  df-pred 24239  df-bpoly 24854
  Copyright terms: Public domain W3C validator