Metamath Proof Explorer

Theorem fsumcube

Description: Express the sum of cubes in closed terms. (Contributed by Scott Fenton, 16-Jun-2015)

Ref Expression
Assertion fsumcube 
|- ( T e. NN0 -> sum_ k e. ( 0 ... T ) ( k ^ 3 ) = ( ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) / 4 ) )

Proof

Step Hyp Ref Expression
1 3nn0 
 |-  3 e. NN0
2 fsumkthpow 
 |-  ( ( 3 e. NN0 /\ T e. NN0 ) -> sum_ k e. ( 0 ... T ) ( k ^ 3 ) = ( ( ( ( 3 + 1 ) BernPoly ( T + 1 ) ) - ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) ) )
3 1 2 mpan 
 |-  ( T e. NN0 -> sum_ k e. ( 0 ... T ) ( k ^ 3 ) = ( ( ( ( 3 + 1 ) BernPoly ( T + 1 ) ) - ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) ) )
4 df-4 
 |-  4 = ( 3 + 1 )
5 4 oveq1i 
 |-  ( 4 BernPoly ( T + 1 ) ) = ( ( 3 + 1 ) BernPoly ( T + 1 ) )
6 4 oveq1i 
 |-  ( 4 BernPoly 0 ) = ( ( 3 + 1 ) BernPoly 0 )
7 5 6 oveq12i 
 |-  ( ( 4 BernPoly ( T + 1 ) ) - ( 4 BernPoly 0 ) ) = ( ( ( 3 + 1 ) BernPoly ( T + 1 ) ) - ( ( 3 + 1 ) BernPoly 0 ) )
8 7 4 oveq12i 
 |-  ( ( ( 4 BernPoly ( T + 1 ) ) - ( 4 BernPoly 0 ) ) / 4 ) = ( ( ( ( 3 + 1 ) BernPoly ( T + 1 ) ) - ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) )
9 nn0cn 
 |-  ( T e. NN0 -> T e. CC )
10 peano2cn 
 |-  ( T e. CC -> ( T + 1 ) e. CC )
11 9 10 syl 
 |-  ( T e. NN0 -> ( T + 1 ) e. CC )
12 bpoly4 
 |-  ( ( T + 1 ) e. CC -> ( 4 BernPoly ( T + 1 ) ) = ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) )
13 11 12 syl 
 |-  ( T e. NN0 -> ( 4 BernPoly ( T + 1 ) ) = ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) )
14 4nn 
 |-  4 e. NN
15 0exp 
 |-  ( 4 e. NN -> ( 0 ^ 4 ) = 0 )
16 14 15 ax-mp 
 |-  ( 0 ^ 4 ) = 0
17 3nn 
 |-  3 e. NN
18 0exp 
 |-  ( 3 e. NN -> ( 0 ^ 3 ) = 0 )
19 17 18 ax-mp 
 |-  ( 0 ^ 3 ) = 0
20 19 oveq2i 
 |-  ( 2 x. ( 0 ^ 3 ) ) = ( 2 x. 0 )
21 2t0e0 
 |-  ( 2 x. 0 ) = 0
22 20 21 eqtri 
 |-  ( 2 x. ( 0 ^ 3 ) ) = 0
23 16 22 oveq12i 
 |-  ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) = ( 0 - 0 )
24 0m0e0 
 |-  ( 0 - 0 ) = 0
25 23 24 eqtri 
 |-  ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) = 0
26 sq0 
 |-  ( 0 ^ 2 ) = 0
27 25 26 oveq12i 
 |-  ( ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) + ( 0 ^ 2 ) ) = ( 0 + 0 )
28 00id 
 |-  ( 0 + 0 ) = 0
29 27 28 eqtri 
 |-  ( ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) + ( 0 ^ 2 ) ) = 0
30 29 oveq1i 
 |-  ( ( ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) + ( 0 ^ 2 ) ) - ( 1 / ; 3 0 ) ) = ( 0 - ( 1 / ; 3 0 ) )
31 0cn 
 |-  0 e. CC
32 bpoly4 
 |-  ( 0 e. CC -> ( 4 BernPoly 0 ) = ( ( ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) + ( 0 ^ 2 ) ) - ( 1 / ; 3 0 ) ) )
33 31 32 ax-mp 
 |-  ( 4 BernPoly 0 ) = ( ( ( ( 0 ^ 4 ) - ( 2 x. ( 0 ^ 3 ) ) ) + ( 0 ^ 2 ) ) - ( 1 / ; 3 0 ) )
34 df-neg 
 |-  -u ( 1 / ; 3 0 ) = ( 0 - ( 1 / ; 3 0 ) )
35 30 33 34 3eqtr4i 
 |-  ( 4 BernPoly 0 ) = -u ( 1 / ; 3 0 )
36 35 a1i 
 |-  ( T e. NN0 -> ( 4 BernPoly 0 ) = -u ( 1 / ; 3 0 ) )
37 13 36 oveq12d 
 |-  ( T e. NN0 -> ( ( 4 BernPoly ( T + 1 ) ) - ( 4 BernPoly 0 ) ) = ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) - -u ( 1 / ; 3 0 ) ) )
38 4nn0 
 |-  4 e. NN0
39 expcl 
 |-  ( ( ( T + 1 ) e. CC /\ 4 e. NN0 ) -> ( ( T + 1 ) ^ 4 ) e. CC )
40 38 39 mpan2 
 |-  ( ( T + 1 ) e. CC -> ( ( T + 1 ) ^ 4 ) e. CC )
41 2cn 
 |-  2 e. CC
42 expcl 
 |-  ( ( ( T + 1 ) e. CC /\ 3 e. NN0 ) -> ( ( T + 1 ) ^ 3 ) e. CC )
43 1 42 mpan2 
 |-  ( ( T + 1 ) e. CC -> ( ( T + 1 ) ^ 3 ) e. CC )
44 mulcl 
 |-  ( ( 2 e. CC /\ ( ( T + 1 ) ^ 3 ) e. CC ) -> ( 2 x. ( ( T + 1 ) ^ 3 ) ) e. CC )
45 41 43 44 sylancr 
 |-  ( ( T + 1 ) e. CC -> ( 2 x. ( ( T + 1 ) ^ 3 ) ) e. CC )
46 40 45 subcld 
 |-  ( ( T + 1 ) e. CC -> ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) e. CC )
47 sqcl 
 |-  ( ( T + 1 ) e. CC -> ( ( T + 1 ) ^ 2 ) e. CC )
48 46 47 addcld 
 |-  ( ( T + 1 ) e. CC -> ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) e. CC )
49 10 48 syl 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) e. CC )
50 9 49 syl 
 |-  ( T e. NN0 -> ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) e. CC )
51 0nn0 
 |-  0 e. NN0
52 1 51 deccl 
 |-  ; 3 0 e. NN0
53 52 nn0cni 
 |-  ; 3 0 e. CC
54 52 nn0rei 
 |-  ; 3 0 e. RR
55 10pos 
 |-  0 < ; 1 0
56 17 51 51 55 declti 
 |-  0 < ; 3 0
57 54 56 gt0ne0ii 
 |-  ; 3 0 =/= 0
58 53 57 reccli 
 |-  ( 1 / ; 3 0 ) e. CC
59 subcl 
 |-  ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) e. CC /\ ( 1 / ; 3 0 ) e. CC ) -> ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) e. CC )
60 50 58 59 sylancl 
 |-  ( T e. NN0 -> ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) e. CC )
61 subneg 
 |-  ( ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) e. CC /\ ( 1 / ; 3 0 ) e. CC ) -> ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) - -u ( 1 / ; 3 0 ) ) = ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) + ( 1 / ; 3 0 ) ) )
62 60 58 61 sylancl 
 |-  ( T e. NN0 -> ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) - -u ( 1 / ; 3 0 ) ) = ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) + ( 1 / ; 3 0 ) ) )
63 npcan 
 |-  ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) e. CC /\ ( 1 / ; 3 0 ) e. CC ) -> ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) + ( 1 / ; 3 0 ) ) = ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) )
64 49 58 63 sylancl 
 |-  ( T e. CC -> ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) + ( 1 / ; 3 0 ) ) = ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) )
65 9 64 syl 
 |-  ( T e. NN0 -> ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) + ( 1 / ; 3 0 ) ) = ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) )
66 2p2e4 
 |-  ( 2 + 2 ) = 4
67 66 eqcomi 
 |-  4 = ( 2 + 2 )
68 67 oveq2i 
 |-  ( ( T + 1 ) ^ 4 ) = ( ( T + 1 ) ^ ( 2 + 2 ) )
69 df-3 
 |-  3 = ( 2 + 1 )
70 69 oveq2i 
 |-  ( ( T + 1 ) ^ 3 ) = ( ( T + 1 ) ^ ( 2 + 1 ) )
71 70 oveq2i 
 |-  ( 2 x. ( ( T + 1 ) ^ 3 ) ) = ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) )
72 68 71 oveq12i 
 |-  ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) = ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) )
73 72 oveq1i 
 |-  ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) = ( ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) ) + ( ( T + 1 ) ^ 2 ) )
74 2nn0 
 |-  2 e. NN0
75 expadd 
 |-  ( ( ( T + 1 ) e. CC /\ 2 e. NN0 /\ 2 e. NN0 ) -> ( ( T + 1 ) ^ ( 2 + 2 ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
76 74 74 75 mp3an23 
 |-  ( ( T + 1 ) e. CC -> ( ( T + 1 ) ^ ( 2 + 2 ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
77 1nn0 
 |-  1 e. NN0
78 expadd 
 |-  ( ( ( T + 1 ) e. CC /\ 2 e. NN0 /\ 1 e. NN0 ) -> ( ( T + 1 ) ^ ( 2 + 1 ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) )
79 74 77 78 mp3an23 
 |-  ( ( T + 1 ) e. CC -> ( ( T + 1 ) ^ ( 2 + 1 ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) )
80 79 oveq2d 
 |-  ( ( T + 1 ) e. CC -> ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) = ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) )
81 76 80 oveq12d 
 |-  ( ( T + 1 ) e. CC -> ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) )
82 10 81 syl 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) )
83 10 sqcld 
 |-  ( T e. CC -> ( ( T + 1 ) ^ 2 ) e. CC )
84 83 mulid1d 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) x. 1 ) = ( ( T + 1 ) ^ 2 ) )
85 84 eqcomd 
 |-  ( T e. CC -> ( ( T + 1 ) ^ 2 ) = ( ( ( T + 1 ) ^ 2 ) x. 1 ) )
86 82 85 oveq12d 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) ) + ( ( T + 1 ) ^ 2 ) ) = ( ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) )
87 10 exp1d 
 |-  ( T e. CC -> ( ( T + 1 ) ^ 1 ) = ( T + 1 ) )
88 87 oveq2d 
 |-  ( T e. CC -> ( 2 x. ( ( T + 1 ) ^ 1 ) ) = ( 2 x. ( T + 1 ) ) )
89 88 oveq2d 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( ( T + 1 ) ^ 1 ) ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( T + 1 ) ) ) )
90 89 oveq2d 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( ( T + 1 ) ^ 1 ) ) ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( T + 1 ) ) ) ) )
91 87 10 eqeltrd 
 |-  ( T e. CC -> ( ( T + 1 ) ^ 1 ) e. CC )
92 mul12 
 |-  ( ( 2 e. CC /\ ( ( T + 1 ) ^ 2 ) e. CC /\ ( ( T + 1 ) ^ 1 ) e. CC ) -> ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( ( T + 1 ) ^ 1 ) ) ) )
93 41 83 91 92 mp3an2i 
 |-  ( T e. CC -> ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( ( T + 1 ) ^ 1 ) ) ) )
94 93 oveq2d 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( ( T + 1 ) ^ 1 ) ) ) ) )
95 mulcl 
 |-  ( ( 2 e. CC /\ ( T + 1 ) e. CC ) -> ( 2 x. ( T + 1 ) ) e. CC )
96 41 10 95 sylancr 
 |-  ( T e. CC -> ( 2 x. ( T + 1 ) ) e. CC )
97 83 83 96 subdid 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) x. ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( ( ( T + 1 ) ^ 2 ) x. ( 2 x. ( T + 1 ) ) ) ) )
98 90 94 97 3eqtr4d 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) ) )
99 98 oveq1d 
 |-  ( T e. CC -> ( ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) )
100 83 96 subcld 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) e. CC )
101 ax-1cn 
 |-  1 e. CC
102 adddi 
 |-  ( ( ( ( T + 1 ) ^ 2 ) e. CC /\ ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) e. CC /\ 1 e. CC ) -> ( ( ( T + 1 ) ^ 2 ) x. ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) )
103 101 102 mp3an3 
 |-  ( ( ( ( T + 1 ) ^ 2 ) e. CC /\ ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) e. CC ) -> ( ( ( T + 1 ) ^ 2 ) x. ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) )
104 83 100 103 syl2anc 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) x. ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) x. ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) )
105 99 104 eqtr4d 
 |-  ( T e. CC -> ( ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) ) )
106 adddi 
 |-  ( ( 2 e. CC /\ T e. CC /\ 1 e. CC ) -> ( 2 x. ( T + 1 ) ) = ( ( 2 x. T ) + ( 2 x. 1 ) ) )
107 41 101 106 mp3an13 
 |-  ( T e. CC -> ( 2 x. ( T + 1 ) ) = ( ( 2 x. T ) + ( 2 x. 1 ) ) )
108 2t1e2 
 |-  ( 2 x. 1 ) = 2
109 108 oveq2i 
 |-  ( ( 2 x. T ) + ( 2 x. 1 ) ) = ( ( 2 x. T ) + 2 )
110 107 109 eqtrdi 
 |-  ( T e. CC -> ( 2 x. ( T + 1 ) ) = ( ( 2 x. T ) + 2 ) )
111 110 oveq1d 
 |-  ( T e. CC -> ( ( 2 x. ( T + 1 ) ) - 1 ) = ( ( ( 2 x. T ) + 2 ) - 1 ) )
112 mulcl 
 |-  ( ( 2 e. CC /\ T e. CC ) -> ( 2 x. T ) e. CC )
113 41 112 mpan 
 |-  ( T e. CC -> ( 2 x. T ) e. CC )
114 addsubass 
 |-  ( ( ( 2 x. T ) e. CC /\ 2 e. CC /\ 1 e. CC ) -> ( ( ( 2 x. T ) + 2 ) - 1 ) = ( ( 2 x. T ) + ( 2 - 1 ) ) )
115 41 101 114 mp3an23 
 |-  ( ( 2 x. T ) e. CC -> ( ( ( 2 x. T ) + 2 ) - 1 ) = ( ( 2 x. T ) + ( 2 - 1 ) ) )
116 113 115 syl 
 |-  ( T e. CC -> ( ( ( 2 x. T ) + 2 ) - 1 ) = ( ( 2 x. T ) + ( 2 - 1 ) ) )
117 2m1e1 
 |-  ( 2 - 1 ) = 1
118 117 oveq2i 
 |-  ( ( 2 x. T ) + ( 2 - 1 ) ) = ( ( 2 x. T ) + 1 )
119 116 118 eqtrdi 
 |-  ( T e. CC -> ( ( ( 2 x. T ) + 2 ) - 1 ) = ( ( 2 x. T ) + 1 ) )
120 111 119 eqtrd 
 |-  ( T e. CC -> ( ( 2 x. ( T + 1 ) ) - 1 ) = ( ( 2 x. T ) + 1 ) )
121 120 oveq2d 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) - ( ( 2 x. ( T + 1 ) ) - 1 ) ) = ( ( ( T + 1 ) ^ 2 ) - ( ( 2 x. T ) + 1 ) ) )
122 subsub 
 |-  ( ( ( ( T + 1 ) ^ 2 ) e. CC /\ ( 2 x. ( T + 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ( T + 1 ) ^ 2 ) - ( ( 2 x. ( T + 1 ) ) - 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) )
123 101 122 mp3an3 
 |-  ( ( ( ( T + 1 ) ^ 2 ) e. CC /\ ( 2 x. ( T + 1 ) ) e. CC ) -> ( ( ( T + 1 ) ^ 2 ) - ( ( 2 x. ( T + 1 ) ) - 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) )
124 83 96 123 syl2anc 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) - ( ( 2 x. ( T + 1 ) ) - 1 ) ) = ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) )
125 sqcl 
 |-  ( T e. CC -> ( T ^ 2 ) e. CC )
126 peano2cn 
 |-  ( ( 2 x. T ) e. CC -> ( ( 2 x. T ) + 1 ) e. CC )
127 113 126 syl 
 |-  ( T e. CC -> ( ( 2 x. T ) + 1 ) e. CC )
128 binom21 
 |-  ( T e. CC -> ( ( T + 1 ) ^ 2 ) = ( ( ( T ^ 2 ) + ( 2 x. T ) ) + 1 ) )
129 addass 
 |-  ( ( ( T ^ 2 ) e. CC /\ ( 2 x. T ) e. CC /\ 1 e. CC ) -> ( ( ( T ^ 2 ) + ( 2 x. T ) ) + 1 ) = ( ( T ^ 2 ) + ( ( 2 x. T ) + 1 ) ) )
130 101 129 mp3an3 
 |-  ( ( ( T ^ 2 ) e. CC /\ ( 2 x. T ) e. CC ) -> ( ( ( T ^ 2 ) + ( 2 x. T ) ) + 1 ) = ( ( T ^ 2 ) + ( ( 2 x. T ) + 1 ) ) )
131 125 113 130 syl2anc 
 |-  ( T e. CC -> ( ( ( T ^ 2 ) + ( 2 x. T ) ) + 1 ) = ( ( T ^ 2 ) + ( ( 2 x. T ) + 1 ) ) )
132 128 131 eqtrd 
 |-  ( T e. CC -> ( ( T + 1 ) ^ 2 ) = ( ( T ^ 2 ) + ( ( 2 x. T ) + 1 ) ) )
133 125 127 132 mvrraddd 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) - ( ( 2 x. T ) + 1 ) ) = ( T ^ 2 ) )
134 121 124 133 3eqtr3d 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) = ( T ^ 2 ) )
135 134 oveq2d 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) x. ( ( ( ( T + 1 ) ^ 2 ) - ( 2 x. ( T + 1 ) ) ) + 1 ) ) = ( ( ( T + 1 ) ^ 2 ) x. ( T ^ 2 ) ) )
136 83 125 mulcomd 
 |-  ( T e. CC -> ( ( ( T + 1 ) ^ 2 ) x. ( T ^ 2 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
137 105 135 136 3eqtrd 
 |-  ( T e. CC -> ( ( ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) - ( 2 x. ( ( ( T + 1 ) ^ 2 ) x. ( ( T + 1 ) ^ 1 ) ) ) ) + ( ( ( T + 1 ) ^ 2 ) x. 1 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
138 86 137 eqtrd 
 |-  ( T e. CC -> ( ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) ) + ( ( T + 1 ) ^ 2 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
139 9 138 syl 
 |-  ( T e. NN0 -> ( ( ( ( T + 1 ) ^ ( 2 + 2 ) ) - ( 2 x. ( ( T + 1 ) ^ ( 2 + 1 ) ) ) ) + ( ( T + 1 ) ^ 2 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
140 73 139 eqtrid 
 |-  ( T e. NN0 -> ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
141 65 140 eqtrd 
 |-  ( T e. NN0 -> ( ( ( ( ( ( T + 1 ) ^ 4 ) - ( 2 x. ( ( T + 1 ) ^ 3 ) ) ) + ( ( T + 1 ) ^ 2 ) ) - ( 1 / ; 3 0 ) ) + ( 1 / ; 3 0 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
142 37 62 141 3eqtrd 
 |-  ( T e. NN0 -> ( ( 4 BernPoly ( T + 1 ) ) - ( 4 BernPoly 0 ) ) = ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) )
143 142 oveq1d 
 |-  ( T e. NN0 -> ( ( ( 4 BernPoly ( T + 1 ) ) - ( 4 BernPoly 0 ) ) / 4 ) = ( ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) / 4 ) )
144 8 143 eqtr3id 
 |-  ( T e. NN0 -> ( ( ( ( 3 + 1 ) BernPoly ( T + 1 ) ) - ( ( 3 + 1 ) BernPoly 0 ) ) / ( 3 + 1 ) ) = ( ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) / 4 ) )
145 3 144 eqtrd 
 |-  ( T e. NN0 -> sum_ k e. ( 0 ... T ) ( k ^ 3 ) = ( ( ( T ^ 2 ) x. ( ( T + 1 ) ^ 2 ) ) / 4 ) )