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 ( 𝑇 ∈ ℕ0 → Σ 𝑘 ∈ ( 0 ... 𝑇 ) ( 𝑘 ↑ 3 ) = ( ( ( 𝑇 ↑ 2 ) · ( ( 𝑇 + 1 ) ↑ 2 ) ) / 4 ) )

Proof

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