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

Theorem bpoly4 26106
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 10241 . . 3  |-  4  e.  NN0
2 bpolyval 26096 . . 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 653 . 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 10075 . . . . . . . 8  |-  4  e.  CC
5 ax-1cn 9049 . . . . . . . 8  |-  1  e.  CC
6 3cn 10073 . . . . . . . 8  |-  3  e.  CC
7 3p1e4 10105 . . . . . . . . 9  |-  ( 3  +  1 )  =  4
86, 5, 7addcomli 9259 . . . . . . . 8  |-  ( 1  +  3 )  =  4
94, 5, 6, 8subaddrii 9390 . . . . . . 7  |-  ( 4  -  1 )  =  3
10 df-3 10060 . . . . . . 7  |-  3  =  ( 2  +  1 )
119, 10eqtri 2457 . . . . . 6  |-  ( 4  -  1 )  =  ( 2  +  1 )
1211oveq2i 6093 . . . . 5  |-  ( 0 ... ( 4  -  1 ) )  =  ( 0 ... (
2  +  1 ) )
1312sumeq1i 12493 . . . 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 10239 . . . . . . . 8  |-  2  e.  NN0
15 nn0uz 10521 . . . . . . . 8  |-  NN0  =  ( ZZ>= `  0 )
1614, 15eleqtri 2509 . . . . . . 7  |-  2  e.  ( ZZ>= `  0 )
1716a1i 11 . . . . . 6  |-  ( X  e.  CC  ->  2  e.  ( ZZ>= `  0 )
)
18 elfzelz 11060 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  e.  ZZ )
19 bccl 11614 . . . . . . . . . 10  |-  ( ( 4  e.  NN0  /\  k  e.  ZZ )  ->  ( 4  _C  k
)  e.  NN0 )
201, 18, 19sylancr 646 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
4  _C  k )  e.  NN0 )
2120nn0cnd 10277 . . . . . . . 8  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
4  _C  k )  e.  CC )
2221adantl 454 . . . . . . 7  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( 4  _C  k )  e.  CC )
23 elfznn0 11084 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  e.  NN0 )
24 bpolycl 26099 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  X  e.  CC )  ->  ( k BernPoly  X )  e.  CC )
2523, 24sylan 459 . . . . . . . . 9  |-  ( ( k  e.  ( 0 ... ( 2  +  1 ) )  /\  X  e.  CC )  ->  ( k BernPoly  X )  e.  CC )
2625ancoms 441 . . . . . . . 8  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( k BernPoly  X
)  e.  CC )
27 4re 10074 . . . . . . . . . . . . 13  |-  4  e.  RR
2827a1i 11 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  4  e.  RR )
2918zred 10376 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  e.  RR )
3028, 29resubcld 9466 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
4  -  k )  e.  RR )
31 peano2re 9240 . . . . . . . . . . 11  |-  ( ( 4  -  k )  e.  RR  ->  (
( 4  -  k
)  +  1 )  e.  RR )
3230, 31syl 16 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
( 4  -  k
)  +  1 )  e.  RR )
3332recnd 9115 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
( 4  -  k
)  +  1 )  e.  CC )
3433adantl 454 . . . . . . . 8  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( 4  -  k )  +  1 )  e.  CC )
35 1re 9091 . . . . . . . . . . . 12  |-  1  e.  RR
3635a1i 11 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  1  e.  RR )
3710oveq2i 6093 . . . . . . . . . . . . . 14  |-  ( 0 ... 3 )  =  ( 0 ... (
2  +  1 ) )
3837eleq2i 2501 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... 3 )  <->  k  e.  ( 0 ... (
2  +  1 ) ) )
39 elfzelz 11060 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( 0 ... 3 )  ->  k  e.  ZZ )
4039zred 10376 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  k  e.  RR )
41 3re 10072 . . . . . . . . . . . . . . 15  |-  3  e.  RR
4241a1i 11 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  3  e.  RR )
4327a1i 11 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  4  e.  RR )
44 elfzle2 11062 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  k  <_  3 )
45 3lt4 10146 . . . . . . . . . . . . . . 15  |-  3  <  4
4645a1i 11 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... 3 )  ->  3  <  4 )
4740, 42, 43, 44, 46lelttrd 9229 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... 3 )  ->  k  <  4 )
4838, 47sylbir 206 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  k  <  4 )
4929, 28posdifd 9614 . . . . . . . . . . . 12  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
k  <  4  <->  0  <  ( 4  -  k ) ) )
5048, 49mpbid 203 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  0  <  ( 4  -  k
) )
51 0lt1 9551 . . . . . . . . . . . 12  |-  0  <  1
5251a1i 11 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  0  <  1 )
5330, 36, 50, 52addgt0d 9602 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  0  <  ( ( 4  -  k )  +  1 ) )
5453gt0ne0d 9592 . . . . . . . . 9  |-  ( k  e.  ( 0 ... ( 2  +  1 ) )  ->  (
( 4  -  k
)  +  1 )  =/=  0 )
5554adantl 454 . . . . . . . 8  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( 4  -  k )  +  1 )  =/=  0
)
5626, 34, 55divcld 9791 . . . . . . 7  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) )  e.  CC )
5722, 56mulcld 9109 . . . . . 6  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 2  +  1 ) ) )  ->  ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  e.  CC )
5810eqeq2i 2447 . . . . . . 7  |-  ( k  =  3  <->  k  =  ( 2  +  1 ) )
59 oveq2 6090 . . . . . . . . 9  |-  ( k  =  3  ->  (
4  _C  k )  =  ( 4  _C  3 ) )
60 4bc3eq4 25204 . . . . . . . . 9  |-  ( 4  _C  3 )  =  4
6159, 60syl6eq 2485 . . . . . . . 8  |-  ( k  =  3  ->  (
4  _C  k )  =  4 )
62 oveq1 6089 . . . . . . . . 9  |-  ( k  =  3  ->  (
k BernPoly  X )  =  ( 3 BernPoly  X ) )
63 oveq2 6090 . . . . . . . . . . 11  |-  ( k  =  3  ->  (
4  -  k )  =  ( 4  -  3 ) )
6463oveq1d 6097 . . . . . . . . . 10  |-  ( k  =  3  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  3 )  +  1 ) )
654, 6, 5, 7subaddrii 9390 . . . . . . . . . . . 12  |-  ( 4  -  3 )  =  1
6665oveq1i 6092 . . . . . . . . . . 11  |-  ( ( 4  -  3 )  +  1 )  =  ( 1  +  1 )
67 df-2 10059 . . . . . . . . . . 11  |-  2  =  ( 1  +  1 )
6866, 67eqtr4i 2460 . . . . . . . . . 10  |-  ( ( 4  -  3 )  +  1 )  =  2
6964, 68syl6eq 2485 . . . . . . . . 9  |-  ( k  =  3  ->  (
( 4  -  k
)  +  1 )  =  2 )
7062, 69oveq12d 6100 . . . . . . . 8  |-  ( k  =  3  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 3 BernPoly  X
)  /  2 ) )
7161, 70oveq12d 6100 . . . . . . 7  |-  ( k  =  3  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 3 BernPoly  X )  /  2
) ) )
7258, 71sylbir 206 . . . . . 6  |-  ( k  =  ( 2  +  1 )  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 3 BernPoly  X )  /  2
) ) )
7317, 57, 72fsump1 12541 . . . . 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 6093 . . . . . . . 8  |-  ( 0 ... 2 )  =  ( 0 ... (
1  +  1 ) )
7574sumeq1i 12493 . . . . . . 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 10238 . . . . . . . . . . 11  |-  1  e.  NN0
7776, 15eleqtri 2509 . . . . . . . . . 10  |-  1  e.  ( ZZ>= `  0 )
7877a1i 11 . . . . . . . . 9  |-  ( X  e.  CC  ->  1  e.  ( ZZ>= `  0 )
)
79 fzssp1 11096 . . . . . . . . . . . 12  |-  ( 0 ... ( 1  +  1 ) )  C_  ( 0 ... (
( 1  +  1 )  +  1 ) )
8067oveq1i 6092 . . . . . . . . . . . . 13  |-  ( 2  +  1 )  =  ( ( 1  +  1 )  +  1 )
8180oveq2i 6093 . . . . . . . . . . . 12  |-  ( 0 ... ( 2  +  1 ) )  =  ( 0 ... (
( 1  +  1 )  +  1 ) )
8279, 81sseqtr4i 3382 . . . . . . . . . . 11  |-  ( 0 ... ( 1  +  1 ) )  C_  ( 0 ... (
2  +  1 ) )
8382sseli 3345 . . . . . . . . . 10  |-  ( k  e.  ( 0 ... ( 1  +  1 ) )  ->  k  e.  ( 0 ... (
2  +  1 ) ) )
8483, 57sylan2 462 . . . . . . . . 9  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 1  +  1 ) ) )  ->  ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  e.  CC )
8567eqeq2i 2447 . . . . . . . . . 10  |-  ( k  =  2  <->  k  =  ( 1  +  1 ) )
86 oveq2 6090 . . . . . . . . . . . 12  |-  ( k  =  2  ->  (
4  _C  k )  =  ( 4  _C  2 ) )
87 4bc2eq6 25205 . . . . . . . . . . . 12  |-  ( 4  _C  2 )  =  6
8886, 87syl6eq 2485 . . . . . . . . . . 11  |-  ( k  =  2  ->  (
4  _C  k )  =  6 )
89 oveq1 6089 . . . . . . . . . . . 12  |-  ( k  =  2  ->  (
k BernPoly  X )  =  ( 2 BernPoly  X ) )
90 oveq2 6090 . . . . . . . . . . . . . 14  |-  ( k  =  2  ->  (
4  -  k )  =  ( 4  -  2 ) )
9190oveq1d 6097 . . . . . . . . . . . . 13  |-  ( k  =  2  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  2 )  +  1 ) )
92 2cn 10071 . . . . . . . . . . . . . . . 16  |-  2  e.  CC
93 2p2e4 10099 . . . . . . . . . . . . . . . 16  |-  ( 2  +  2 )  =  4
944, 92, 92, 93subaddrii 9390 . . . . . . . . . . . . . . 15  |-  ( 4  -  2 )  =  2
9594oveq1i 6092 . . . . . . . . . . . . . 14  |-  ( ( 4  -  2 )  +  1 )  =  ( 2  +  1 )
9695, 10eqtr4i 2460 . . . . . . . . . . . . 13  |-  ( ( 4  -  2 )  +  1 )  =  3
9791, 96syl6eq 2485 . . . . . . . . . . . 12  |-  ( k  =  2  ->  (
( 4  -  k
)  +  1 )  =  3 )
9889, 97oveq12d 6100 . . . . . . . . . . 11  |-  ( k  =  2  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 2 BernPoly  X
)  /  3 ) )
9988, 98oveq12d 6100 . . . . . . . . . 10  |-  ( k  =  2  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 6  x.  ( ( 2 BernPoly  X )  /  3
) ) )
10085, 99sylbir 206 . . . . . . . . 9  |-  ( k  =  ( 1  +  1 )  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 6  x.  ( ( 2 BernPoly  X )  /  3
) ) )
10178, 84, 100fsump1 12541 . . . . . . . 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 10094 . . . . . . . . . . . 12  |-  ( 0  +  1 )  =  1
103102oveq2i 6093 . . . . . . . . . . 11  |-  ( 0 ... ( 0  +  1 ) )  =  ( 0 ... 1
)
104103sumeq1i 12493 . . . . . . . . . 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 10237 . . . . . . . . . . . . . 14  |-  0  e.  NN0
106105, 15eleqtri 2509 . . . . . . . . . . . . 13  |-  0  e.  ( ZZ>= `  0 )
107106a1i 11 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  0  e.  ( ZZ>= `  0 )
)
108 3nn 10135 . . . . . . . . . . . . . . . . 17  |-  3  e.  NN
109 nnuz 10522 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
110108, 109eleqtri 2509 . . . . . . . . . . . . . . . 16  |-  3  e.  ( ZZ>= `  1 )
111 fzss2 11093 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  ( ZZ>= `  1
)  ->  ( 0 ... 1 )  C_  ( 0 ... 3
) )
112110, 111ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 0 ... 1 )  C_  ( 0 ... 3
)
113 2p1e3 10104 . . . . . . . . . . . . . . . 16  |-  ( 2  +  1 )  =  3
114113oveq2i 6093 . . . . . . . . . . . . . . 15  |-  ( 0 ... ( 2  +  1 ) )  =  ( 0 ... 3
)
115112, 103, 1143sstr4i 3388 . . . . . . . . . . . . . 14  |-  ( 0 ... ( 0  +  1 ) )  C_  ( 0 ... (
2  +  1 ) )
116115sseli 3345 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... ( 0  +  1 ) )  ->  k  e.  ( 0 ... (
2  +  1 ) ) )
117116, 57sylan2 462 . . . . . . . . . . . 12  |-  ( ( X  e.  CC  /\  k  e.  ( 0 ... ( 0  +  1 ) ) )  ->  ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  e.  CC )
118102eqeq2i 2447 . . . . . . . . . . . . 13  |-  ( k  =  ( 0  +  1 )  <->  k  = 
1 )
119 oveq2 6090 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
4  _C  k )  =  ( 4  _C  1 ) )
120 bcn1 11605 . . . . . . . . . . . . . . . 16  |-  ( 4  e.  NN0  ->  ( 4  _C  1 )  =  4 )
1211, 120ax-mp 8 . . . . . . . . . . . . . . 15  |-  ( 4  _C  1 )  =  4
122119, 121syl6eq 2485 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
4  _C  k )  =  4 )
123 oveq1 6089 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
k BernPoly  X )  =  ( 1 BernPoly  X ) )
124 oveq2 6090 . . . . . . . . . . . . . . . . 17  |-  ( k  =  1  ->  (
4  -  k )  =  ( 4  -  1 ) )
125124oveq1d 6097 . . . . . . . . . . . . . . . 16  |-  ( k  =  1  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  1 )  +  1 ) )
1269oveq1i 6092 . . . . . . . . . . . . . . . . 17  |-  ( ( 4  -  1 )  +  1 )  =  ( 3  +  1 )
127 df-4 10061 . . . . . . . . . . . . . . . . 17  |-  4  =  ( 3  +  1 )
128126, 127eqtr4i 2460 . . . . . . . . . . . . . . . 16  |-  ( ( 4  -  1 )  +  1 )  =  4
129125, 128syl6eq 2485 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  (
( 4  -  k
)  +  1 )  =  4 )
130123, 129oveq12d 6100 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 1 BernPoly  X
)  /  4 ) )
131122, 130oveq12d 6100 . . . . . . . . . . . . 13  |-  ( k  =  1  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 1 BernPoly  X )  /  4
) ) )
132118, 131sylbi 189 . . . . . . . . . . . 12  |-  ( k  =  ( 0  +  1 )  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 4  x.  ( ( 1 BernPoly  X )  /  4
) ) )
133107, 117, 132fsump1 12541 . . . . . . . . . . 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 10294 . . . . . . . . . . . . . 14  |-  0  e.  ZZ
1355a1i 11 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  1  e.  CC )
136 bpolycl 26099 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  e.  NN0  /\  X  e.  CC )  ->  ( 0 BernPoly  X )  e.  CC )
137105, 136mpan 653 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  (
0 BernPoly  X )  e.  CC )
138 5re 10076 . . . . . . . . . . . . . . . . . 18  |-  5  e.  RR
139138recni 9103 . . . . . . . . . . . . . . . . 17  |-  5  e.  CC
140139a1i 11 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  5  e.  CC )
141 0re 9092 . . . . . . . . . . . . . . . . . 18  |-  0  e.  RR
142 5pos 10088 . . . . . . . . . . . . . . . . . 18  |-  0  <  5
143141, 142gtneii 9186 . . . . . . . . . . . . . . . . 17  |-  5  =/=  0
144143a1i 11 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  5  =/=  0 )
145137, 140, 144divcld 9791 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 0 BernPoly  X )  /  5 )  e.  CC )
146135, 145mulcld 9109 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
1  x.  ( ( 0 BernPoly  X )  /  5
) )  e.  CC )
147 oveq2 6090 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  (
4  _C  k )  =  ( 4  _C  0 ) )
148 bcn0 11602 . . . . . . . . . . . . . . . . . 18  |-  ( 4  e.  NN0  ->  ( 4  _C  0 )  =  1 )
1491, 148ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  ( 4  _C  0 )  =  1
150147, 149syl6eq 2485 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
4  _C  k )  =  1 )
151 oveq1 6089 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  (
k BernPoly  X )  =  ( 0 BernPoly  X ) )
152 oveq2 6090 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  (
4  -  k )  =  ( 4  -  0 ) )
153152oveq1d 6097 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  (
( 4  -  k
)  +  1 )  =  ( ( 4  -  0 )  +  1 ) )
1544subid1i 9373 . . . . . . . . . . . . . . . . . . . 20  |-  ( 4  -  0 )  =  4
155154oveq1i 6092 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 4  -  0 )  +  1 )  =  ( 4  +  1 )
156 4p1e5 10106 . . . . . . . . . . . . . . . . . . 19  |-  ( 4  +  1 )  =  5
157155, 156eqtri 2457 . . . . . . . . . . . . . . . . . 18  |-  ( ( 4  -  0 )  +  1 )  =  5
158153, 157syl6eq 2485 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  (
( 4  -  k
)  +  1 )  =  5 )
159151, 158oveq12d 6100 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
( k BernPoly  X )  /  ( ( 4  -  k )  +  1 ) )  =  ( ( 0 BernPoly  X
)  /  5 ) )
160150, 159oveq12d 6100 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
( 4  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( 4  -  k
)  +  1 ) ) )  =  ( 1  x.  ( ( 0 BernPoly  X )  /  5
) ) )
161160fsum1 12536 . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . 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 26097 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  (
0 BernPoly  X )  =  1 )
164163oveq1d 6097 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 0 BernPoly  X )  /  5 )  =  ( 1  /  5
) )
165164oveq2d 6098 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
1  x.  ( ( 0 BernPoly  X )  /  5
) )  =  ( 1  x.  ( 1  /  5 ) ) )
166139, 143reccli 9745 . . . . . . . . . . . . . . 15  |-  ( 1  /  5 )  e.  CC
167166mulid2i 9094 . . . . . . . . . . . . . 14  |-  ( 1  x.  ( 1  / 
5 ) )  =  ( 1  /  5
)
168165, 167syl6eq 2485 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
1  x.  ( ( 0 BernPoly  X )  /  5
) )  =  ( 1  /  5 ) )
169162, 168eqtrd 2469 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  sum_ k  e.  ( 0 ... 0
) ( ( 4  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( 4  -  k )  +  1 ) ) )  =  ( 1  /  5 ) )
170 bpolycl 26099 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  NN0  /\  X  e.  CC )  ->  ( 1 BernPoly  X )  e.  CC )
17176, 170mpan 653 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
1 BernPoly  X )  e.  CC )
172 nn0cn 10232 . . . . . . . . . . . . . . 15  |-  ( 4  e.  NN0  ->  4  e.  CC )
1731, 172mp1i 12 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  4  e.  CC )
174 4pos 10087 . . . . . . . . . . . . . . . 16  |-  0  <  4
175141, 174gtneii 9186 . . . . . . . . . . . . . . 15  |-  4  =/=  0
176175a1i 11 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  4  =/=  0 )
177171, 173, 176divcan2d 9793 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
4  x.  ( ( 1 BernPoly  X )  /  4
) )  =  ( 1 BernPoly  X ) )
178 bpoly1 26098 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
1 BernPoly  X )  =  ( X  -  ( 1  /  2 ) ) )
179177, 178eqtrd 2469 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
4  x.  ( ( 1 BernPoly  X )  /  4
) )  =  ( X  -  ( 1  /  2 ) ) )
180169, 179oveq12d 6100 . . . . . . . . . . 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 2469 . . . . . . . . . 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 2483 . . . . . . . . 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 10077 . . . . . . . . . . . . 13  |-  6  e.  RR
184183recni 9103 . . . . . . . . . . . 12  |-  6  e.  CC
185184a1i 11 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  6  e.  CC )
186 bpolycl 26099 . . . . . . . . . . . 12  |-  ( ( 2  e.  NN0  /\  X  e.  CC )  ->  ( 2 BernPoly  X )  e.  CC )
18714, 186mpan 653 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
2 BernPoly  X )  e.  CC )
1886a1i 11 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  3  e.  CC )
189 3ne0 10086 . . . . . . . . . . . 12  |-  3  =/=  0
190189a1i 11 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  3  =/=  0 )
191185, 187, 188, 190div12d 9827 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
6  x.  ( ( 2 BernPoly  X )  /  3
) )  =  ( ( 2 BernPoly  X )  x.  ( 6  / 
3 ) ) )
192 3t2e6 10129 . . . . . . . . . . . . 13  |-  ( 3  x.  2 )  =  6
193184, 6, 92, 189divmuli 9769 . . . . . . . . . . . . 13  |-  ( ( 6  /  3 )  =  2  <->  ( 3  x.  2 )  =  6 )
194192, 193mpbir 202 . . . . . . . . . . . 12  |-  ( 6  /  3 )  =  2
195194oveq2i 6093 . . . . . . . . . . 11  |-  ( ( 2 BernPoly  X )  x.  (
6  /  3 ) )  =  ( ( 2 BernPoly  X )  x.  2 )
19692a1i 11 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  2  e.  CC )
197187, 196mulcomd 9110 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 2 BernPoly  X )  x.  2 )  =  ( 2  x.  ( 2 BernPoly  X ) ) )
198 bpoly2 26104 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
2 BernPoly  X )  =  ( ( ( X ^
2 )  -  X
)  +  ( 1  /  6 ) ) )
199198oveq2d 6098 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
2  x.  ( 2 BernPoly  X ) )  =  ( 2  x.  (
( ( X ^
2 )  -  X
)  +  ( 1  /  6 ) ) ) )
200197, 199eqtrd 2469 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( 2 BernPoly  X )  x.  2 )  =  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) ) )
201195, 200syl5eq 2481 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( 2 BernPoly  X )  x.  ( 6  /  3
) )  =  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) ) )
202191, 201eqtrd 2469 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
6  x.  ( ( 2 BernPoly  X )  /  3
) )  =  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) ) )
203182, 202oveq12d 6100 . . . . . . . 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 2469 . . . . . . 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 2481 . . . . . 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 10240 . . . . . . . . 9  |-  3  e.  NN0
207 bpolycl 26099 . . . . . . . . 9  |-  ( ( 3  e.  NN0  /\  X  e.  CC )  ->  ( 3 BernPoly  X )  e.  CC )
208206, 207mpan 653 . . . . . . . 8  |-  ( X  e.  CC  ->  (
3 BernPoly  X )  e.  CC )
209 2ne0 10084 . . . . . . . . 9  |-  2  =/=  0
210209a1i 11 . . . . . . . 8  |-  ( X  e.  CC  ->  2  =/=  0 )
211173, 208, 196, 210div12d 9827 . . . . . . 7  |-  ( X  e.  CC  ->  (
4  x.  ( ( 3 BernPoly  X )  /  2
) )  =  ( ( 3 BernPoly  X )  x.  ( 4  / 
2 ) ) )
212 4d2e2 10133 . . . . . . . . 9  |-  ( 4  /  2 )  =  2
213212oveq2i 6093 . . . . . . . 8  |-  ( ( 3 BernPoly  X )  x.  (
4  /  2 ) )  =  ( ( 3 BernPoly  X )  x.  2 )
214208, 196mulcomd 9110 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( 3 BernPoly  X )  x.  2 )  =  ( 2  x.  ( 3 BernPoly  X ) ) )
215 bpoly3 26105 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
3 BernPoly  X )  =  ( ( ( X ^
3 )  -  (
( 3  /  2
)  x.  ( X ^ 2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) )
216215oveq2d 6098 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
2  x.  ( 3 BernPoly  X ) )  =  ( 2  x.  (
( ( X ^
3 )  -  (
( 3  /  2
)  x.  ( X ^ 2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) ) )
217214, 216eqtrd 2469 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( 3 BernPoly  X )  x.  2 )  =  ( 2  x.  ( ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) ) )
218213, 217syl5eq 2481 . . . . . . 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 2469 . . . . . 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 6100 . . . . 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 2469 . . . 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 2481 . . 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 6098 . 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 11400 . . . . 5  |-  ( ( X  e.  CC  /\  4  e.  NN0 )  -> 
( X ^ 4 )  e.  CC )
2251, 224mpan2 654 . . . 4  |-  ( X  e.  CC  ->  ( X ^ 4 )  e.  CC )
226 expcl 11400 . . . . . 6  |-  ( ( X  e.  CC  /\  3  e.  NN0 )  -> 
( X ^ 3 )  e.  CC )
227206, 226mpan2 654 . . . . 5  |-  ( X  e.  CC  ->  ( X ^ 3 )  e.  CC )
228196, 227mulcld 9109 . . . 4  |-  ( X  e.  CC  ->  (
2  x.  ( X ^ 3 ) )  e.  CC )
229 sqcl 11445 . . . . 5  |-  ( X  e.  CC  ->  ( X ^ 2 )  e.  CC )
230206, 105deccl 10397 . . . . . . . 8  |- ; 3 0  e.  NN0
231230nn0cni 10234 . . . . . . 7  |- ; 3 0  e.  CC
232 df-dec 10384 . . . . . . . . 9  |- ; 3 0  =  ( ( 10  x.  3 )  +  0 )
233 10re 10081 . . . . . . . . . . . 12  |-  10  e.  RR
234233recni 9103 . . . . . . . . . . 11  |-  10  e.  CC
235234, 6mulcli 9096 . . . . . . . . . 10  |-  ( 10  x.  3 )  e.  CC
236235addid1i 9254 . . . . . . . . 9  |-  ( ( 10  x.  3 )  +  0 )  =  ( 10  x.  3 )
237232, 236eqtri 2457 . . . . . . . 8  |- ; 3 0  =  ( 10  x.  3 )
238 10pos 10093 . . . . . . . . . 10  |-  0  <  10
239141, 238gtneii 9186 . . . . . . . . 9  |-  10  =/=  0
240234, 6, 239, 189mulne0i 9666 . . . . . . . 8  |-  ( 10  x.  3 )  =/=  0
241237, 240eqnetri 2619 . . . . . . 7  |- ; 3 0  =/=  0
242231, 241reccli 9745 . . . . . 6  |-  ( 1  / ; 3 0 )  e.  CC
243242a1i 11 . . . . 5  |-  ( X  e.  CC  ->  (
1  / ; 3 0 )  e.  CC )
244229, 243subcld 9412 . . . 4  |-  ( X  e.  CC  ->  (
( X ^ 2 )  -  ( 1  / ; 3 0 ) )  e.  CC )
245225, 228, 244subsubd 9440 . . 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 11 . . . . . . . 8  |-  ( X  e.  CC  ->  (
1  /  5 )  e.  CC )
247 id 21 . . . . . . . . 9  |-  ( X  e.  CC  ->  X  e.  CC )
24892, 209reccli 9745 . . . . . . . . . 10  |-  ( 1  /  2 )  e.  CC
249248a1i 11 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
1  /  2 )  e.  CC )
250247, 249subcld 9412 . . . . . . . 8  |-  ( X  e.  CC  ->  ( X  -  ( 1  /  2 ) )  e.  CC )
251246, 250addcld 9108 . . . . . . 7  |-  ( X  e.  CC  ->  (
( 1  /  5
)  +  ( X  -  ( 1  / 
2 ) ) )  e.  CC )
252229, 247subcld 9412 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( X ^ 2 )  -  X )  e.  CC )
253 6pos 10089 . . . . . . . . . . . 12  |-  0  <  6
254141, 253gtneii 9186 . . . . . . . . . . 11  |-  6  =/=  0
255184, 254reccli 9745 . . . . . . . . . 10  |-  ( 1  /  6 )  e.  CC
256255a1i 11 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
1  /  6 )  e.  CC )
257252, 256addcld 9108 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( ( X ^
2 )  -  X
)  +  ( 1  /  6 ) )  e.  CC )
258196, 257mulcld 9109 . . . . . . 7  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) )  e.  CC )
259251, 258addcld 9108 . . . . . 6  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  +  ( X  -  ( 1  /  2 ) ) )  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6
) ) ) )  e.  CC )
2606, 92, 209divcli 9757 . . . . . . . . . . 11  |-  ( 3  /  2 )  e.  CC
261260a1i 11 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
3  /  2 )  e.  CC )
262261, 229mulcld 9109 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( 3  /  2
)  x.  ( X ^ 2 ) )  e.  CC )
263227, 262subcld 9412 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  e.  CC )
264249, 247mulcld 9109 . . . . . . . 8  |-  ( X  e.  CC  ->  (
( 1  /  2
)  x.  X )  e.  CC )
265263, 264addcld 9108 . . . . . . 7  |-  ( X  e.  CC  ->  (
( ( X ^
3 )  -  (
( 3  /  2
)  x.  ( X ^ 2 ) ) )  +  ( ( 1  /  2 )  x.  X ) )  e.  CC )
266196, 265mulcld 9109 . . . . . 6  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 3 )  -  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  +  ( ( 1  /  2 )  x.  X ) ) )  e.  CC )
267259, 266addcomd 9269 . . . . 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 9113 . . . . . . 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 9490 . . . . . . . 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 9746 . . . . . . . . . 10  |-  ( 2  x.  ( 1  / 
2 ) )  =  1
271270oveq1i 6092 . . . . . . . . 9  |-  ( ( 2  x.  ( 1  /  2 ) )  x.  X )  =  ( 1  x.  X
)
272196, 249, 247mulassd 9112 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
( 2  x.  (
1  /  2 ) )  x.  X )  =  ( 2  x.  ( ( 1  / 
2 )  x.  X
) ) )
273 mulid2 9090 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
1  x.  X )  =  X )
274271, 272, 2733eqtr3a 2493 . . . . . . . 8  |-  ( X  e.  CC  ->  (
2  x.  ( ( 1  /  2 )  x.  X ) )  =  X )
275269, 274oveq12d 6100 . . . . . . 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 2469 . . . . . 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 6097 . . . . 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 9109 . . . . . . . 8  |-  ( X  e.  CC  ->  (
2  x.  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  e.  CC )
279228, 278subcld 9412 . . . . . . 7  |-  ( X  e.  CC  ->  (
( 2  x.  ( X ^ 3 ) )  -  ( 2  x.  ( ( 3  / 
2 )  x.  ( X ^ 2 ) ) ) )  e.  CC )
280279, 247, 259addassd 9111 . . . . . 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 9108 . . . . . . 7  |-  ( X  e.  CC  ->  ( X  +  ( (
( 1  /  5
)  +  ( X  -  ( 1  / 
2 ) ) )  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6 ) ) ) ) )  e.  CC )
282228, 278, 281subsubd 9440 . . . . . 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 9758 . . . . . . . . . . 11  |-  ( 2  x.  ( 3  / 
2 ) )  =  3
284283oveq1i 6092 . . . . . . . . . 10  |-  ( ( 2  x.  ( 3  /  2 ) )  x.  ( X ^
2 ) )  =  ( 3  x.  ( X ^ 2 ) )
285196, 261, 229mulassd 9112 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( 2  x.  (
3  /  2 ) )  x.  ( X ^ 2 ) )  =  ( 2  x.  ( ( 3  / 
2 )  x.  ( X ^ 2 ) ) ) )
286284, 285syl5reqr 2484 . . . . . . . . 9  |-  ( X  e.  CC  ->  (
2  x.  ( ( 3  /  2 )  x.  ( X ^
2 ) ) )  =  ( 3  x.  ( X ^ 2 ) ) )
287286oveq1d 6097 . . . . . . . 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 9288 . . . . . . . . . 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 9113 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) )  =  ( ( 2  x.  ( ( X ^ 2 )  -  X ) )  +  ( 2  x.  (
1  /  6 ) ) ) )
290196, 229, 247subdid 9490 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
2  x.  ( ( X ^ 2 )  -  X ) )  =  ( ( 2  x.  ( X ^
2 ) )  -  ( 2  x.  X
) ) )
291192oveq2i 6093 . . . . . . . . . . . . . . . . 17  |-  ( 2  /  ( 3  x.  2 ) )  =  ( 2  /  6
)
2926, 189reccli 9745 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  3 )  e.  CC
2936, 92, 292mul32i 9263 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  x.  2 )  x.  ( 1  / 
3 ) )  =  ( ( 3  x.  ( 1  /  3
) )  x.  2 )
2946, 189recidi 9746 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 3  x.  ( 1  / 
3 ) )  =  1
295294oveq1i 6092 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 3  x.  ( 1  /  3 ) )  x.  2 )  =  ( 1  x.  2 )
29692mulid2i 9094 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  x.  2 )  =  2
297295, 296eqtri 2457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 3  x.  ( 1  /  3 ) )  x.  2 )  =  2
298293, 297eqtri 2457 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  x.  2 )  x.  ( 1  / 
3 ) )  =  2
299192, 184eqeltri 2507 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  x.  2 )  e.  CC
300192, 254eqnetri 2619 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  x.  2 )  =/=  0
30192, 299, 292, 300divmuli 9769 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  /  ( 3  x.  2 ) )  =  ( 1  / 
3 )  <->  ( (
3  x.  2 )  x.  ( 1  / 
3 ) )  =  2 )
302298, 301mpbir 202 . . . . . . . . . . . . . . . . 17  |-  ( 2  /  ( 3  x.  2 ) )  =  ( 1  /  3
)
30392, 184, 254divreci 9760 . . . . . . . . . . . . . . . . 17  |-  ( 2  /  6 )  =  ( 2  x.  (
1  /  6 ) )
304291, 302, 3033eqtr3ri 2466 . . . . . . . . . . . . . . . 16  |-  ( 2  x.  ( 1  / 
6 ) )  =  ( 1  /  3
)
305304a1i 11 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
2  x.  ( 1  /  6 ) )  =  ( 1  / 
3 ) )
306290, 305oveq12d 6100 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
( 2  x.  (
( X ^ 2 )  -  X ) )  +  ( 2  x.  ( 1  / 
6 ) ) )  =  ( ( ( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) )  +  ( 1  /  3
) ) )
307289, 306eqtrd 2469 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  / 
6 ) ) )  =  ( ( ( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) )  +  ( 1  /  3
) ) )
308307oveq2d 6098 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  ( X  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6
) ) ) )  =  ( X  +  ( ( ( 2  x.  ( X ^
2 ) )  -  ( 2  x.  X
) )  +  ( 1  /  3 ) ) ) )
309196, 229mulcld 9109 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
2  x.  ( X ^ 2 ) )  e.  CC )
310196, 247mulcld 9109 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
2  x.  X )  e.  CC )
311309, 310subcld 9412 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) )  e.  CC )
312292a1i 11 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
1  /  3 )  e.  CC )
313247, 311, 312addassd 9111 . . . . . . . . . . . 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 9435 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  ( X  +  ( (
2  x.  ( X ^ 2 ) )  -  ( 2  x.  X ) ) )  =  ( ( 2  x.  ( X ^
2 ) )  +  ( X  -  (
2  x.  X ) ) ) )
315314oveq1d 6097 . . . . . . . . . . . 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 2475 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  ( X  +  ( 2  x.  ( ( ( X ^ 2 )  -  X )  +  ( 1  /  6
) ) ) )  =  ( ( ( 2  x.  ( X ^ 2 ) )  +  ( X  -  ( 2  x.  X
) ) )  +  ( 1  /  3
) ) )
317316oveq2d 6098 . . . . . . . . . 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 2469 . . . . . . . . 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 6098 . . . . . . . 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 9412 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  ( X  -  ( 2  x.  X ) )  e.  CC )
321309, 320addcld 9108 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 2  x.  ( X ^ 2 ) )  +  ( X  -  ( 2  x.  X
) ) )  e.  CC )
322246, 250, 321, 312add4d 9290 . . . . . . . . . . 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 9288 . . . . . . . . . . . 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 6097 . . . . . . . . . . 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 9108 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 1  /  5
)  +  ( X  -  ( 2  x.  X ) ) )  e.  CC )
326250, 312addcld 9108 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( X  -  (
1  /  2 ) )  +  ( 1  /  3 ) )  e.  CC )
327309, 325, 326addassd 9111 . . . . . . . . . . 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 2473 . . . . . . . . . 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 6098 . . . . . . . . 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 9109 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
3  x.  ( X ^ 2 ) )  e.  CC )
331325, 326addcld 9108 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  +  ( X  -  ( 2  x.  X ) ) )  +  ( ( X  -  ( 1  /  2 ) )  +  ( 1  / 
3 ) ) )  e.  CC )
332330, 309, 331subsub4d 9443 . . . . . . . . 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 9390 . . . . . . . . . . . 12  |-  ( 3  -  2 )  =  1
334333oveq1i 6092 . . . . . . . . . . 11  |-  ( ( 3  -  2 )  x.  ( X ^
2 ) )  =  ( 1  x.  ( X ^ 2 ) )
335188, 196, 229subdird 9491 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( 3  -  2 )  x.  ( X ^ 2 ) )  =  ( ( 3  x.  ( X ^
2 ) )  -  ( 2  x.  ( X ^ 2 ) ) ) )
336229mulid2d 9107 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
1  x.  ( X ^ 2 ) )  =  ( X ^
2 ) )
337334, 335, 3363eqtr3a 2493 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( 3  x.  ( X ^ 2 ) )  -  ( 2  x.  ( X ^ 2 ) ) )  =  ( X ^ 2 ) )
338246, 310, 247subsubd 9440 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 1  /  5
)  -  ( ( 2  x.  X )  -  X ) )  =  ( ( ( 1  /  5 )  -  ( 2  x.  X ) )  +  X ) )
339273oveq2d 6098 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 2  x.  X
)  -  ( 1  x.  X ) )  =  ( ( 2  x.  X )  -  X ) )
340 2m1e1 10096 . . . . . . . . . . . . . . . . 17  |-  ( 2  -  1 )  =  1
341340oveq1i 6092 . . . . . . . . . . . . . . . 16  |-  ( ( 2  -  1 )  x.  X )  =  ( 1  x.  X
)
342196, 135, 247subdird 9491 . . . . . . . . . . . . . . . 16  |-  ( X  e.  CC  ->  (
( 2  -  1 )  x.  X )  =  ( ( 2  x.  X )  -  ( 1  x.  X
) ) )
343341, 342, 2733eqtr3a 2493 . . . . . . . . . . . . . . 15  |-  ( X  e.  CC  ->  (
( 2  x.  X
)  -  ( 1  x.  X ) )  =  X )
344339, 343eqtr3d 2471 . . . . . . . . . . . . . 14  |-  ( X  e.  CC  ->  (
( 2  x.  X
)  -  X )  =  X )
345344oveq2d 6098 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 1  /  5
)  -  ( ( 2  x.  X )  -  X ) )  =  ( ( 1  /  5 )  -  X ) )
346246, 310, 247subadd23d 9434 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  (
2  x.  X ) )  +  X )  =  ( ( 1  /  5 )  +  ( X  -  (
2  x.  X ) ) ) )
347338, 345, 3463eqtr3d 2477 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( 1  /  5
)  -  X )  =  ( ( 1  /  5 )  +  ( X  -  (
2  x.  X ) ) ) )
348247, 249, 312subsubd 9440 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  ( X  -  ( (
1  /  2 )  -  ( 1  / 
3 ) ) )  =  ( ( X  -  ( 1  / 
2 ) )  +  ( 1  /  3
) ) )
349347, 348oveq12d 6100 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  X
)  +  ( X  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) ) )  =  ( ( ( 1  /  5 )  +  ( X  -  ( 2  x.  X
) ) )  +  ( ( X  -  ( 1  /  2
) )  +  ( 1  /  3 ) ) ) )
350248, 292subcli 9377 . . . . . . . . . . . . . 14  |-  ( ( 1  /  2 )  -  ( 1  / 
3 ) )  e.  CC
351350a1i 11 . . . . . . . . . . . . 13  |-  ( X  e.  CC  ->  (
( 1  /  2
)  -  ( 1  /  3 ) )  e.  CC )
352246, 247, 351npncand 9436 . . . . . . . . . . . 12  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  X
)  +  ( X  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) ) )  =  ( ( 1  /  5 )  -  ( ( 1  / 
2 )  -  (
1  /  3 ) ) ) )
353 halfthird 25206 . . . . . . . . . . . . . 14  |-  ( ( 1  /  2 )  -  ( 1  / 
3 ) )  =  ( 1  /  6
)
354353oveq2i 6093 . . . . . . . . . . . . 13  |-  ( ( 1  /  5 )  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) )  =  ( ( 1  / 
5 )  -  (
1  /  6 ) )
355 5recm6rec 25207 . . . . . . . . . . . . 13  |-  ( ( 1  /  5 )  -  ( 1  / 
6 ) )  =  ( 1  / ; 3 0 )
356354, 355eqtri 2457 . . . . . . . . . . . 12  |-  ( ( 1  /  5 )  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) )  =  ( 1  / ; 3 0 )
357352, 356syl6eq 2485 . . . . . . . . . . 11  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  -  X
)  +  ( X  -  ( ( 1  /  2 )  -  ( 1  /  3
) ) ) )  =  ( 1  / ; 3 0 ) )
358349, 357eqtr3d 2471 . . . . . . . . . 10  |-  ( X  e.  CC  ->  (
( ( 1  / 
5 )  +  ( X  -  ( 2  x.  X ) ) )  +  ( ( X  -  ( 1  /  2 ) )  +  ( 1  / 
3 ) ) )  =  ( 1  / ; 3 0 ) )
359337, 358oveq12d 6100 . . . . . . . . 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 ) ) )
360329, 332, 3593eqtr2d 2475 . . . . . . . 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 ) ) )
361287, 319, 3603eqtrd 2473 . . . . . . 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 ) ) )
362361oveq2d 6098 . . . . . 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 ) ) ) )
363280, 282, 3623eqtr2d 2475 . . . . 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 ) ) ) )
364267, 277, 3633eqtrd 2473 . . . 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 ) ) ) )
365364oveq2d 6098 . . 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 ) ) ) ) )
366225, 228subcld 9412 . . . 4  |-  ( X  e.  CC  ->  (
( X ^ 4 )  -  ( 2  x.  ( X ^
3 ) ) )  e.  CC )
367366, 229, 243addsubassd 9432 . . 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 ) ) ) )
368245, 365, 3673eqtr4d 2479 . 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 ) ) )
3693, 223, 3683eqtrd 2473 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 360    = wceq 1653    e. wcel 1726    =/= wne 2600    C_ wss 3321   class class class wbr 4213   ` cfv 5455  (class class class)co 6082   CCcc 8989   RRcr 8990   0cc0 8991   1c1 8992    + caddc 8994    x. cmul 8996    < clt 9121    - cmin 9292    / cdiv 9678   NNcn 10001   2c2 10050   3c3 10051   4c4 10052   5c5 10053   6c6 10054   10c10 10058   NN0cn0 10222   ZZcz 10283  ;cdc 10383   ZZ>=cuz 10489   ...cfz 11044   ^cexp 11383    _C cbc 11594   sum_csu 12480   BernPoly cbp 26093
This theorem is referenced by:  fsumcube  26107
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-oadd 6729  df-er 6906  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-sup 7447  df-oi 7480  df-card 7827  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-4 10061  df-5 10062  df-6 10063  df-7 10064  df-8 10065  df-9 10066  df-10 10067  df-n0 10223  df-z 10284  df-dec 10384  df-uz 10490  df-rp 10614  df-fz 11045  df-fzo 11137  df-seq 11325  df-exp 11384  df-fac 11568  df-bc 11595  df-hash 11620  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-clim 12283  df-sum 12481  df-pred 25440  df-wrecs 25532  df-bpoly 26094
  Copyright terms: Public domain W3C validator