# 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}\in {ℕ}_{0}\to \sum _{{k}=0}^{{T}}{{k}}^{3}=\frac{{{T}}^{2}{\left({T}+1\right)}^{2}}{4}$

### Proof

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