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} {(T + 1)}^{2}}{4}$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$⊢ 3 \in ℕ_{0}$
2		fsumkthpow	$⊢ (3 \in ℕ_{0} \land T \in ℕ_{0}) \to \sum_{k = 0}^{T} k^{3} = \frac{((3 + 1) BernPoly (T + 1)) - ((3 + 1) BernPoly 0)}{3 + 1}$
3	1 2	mpan	$⊢ T \in ℕ_{0} \to \sum_{k = 0}^{T} k^{3} = \frac{((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	$⊢ \frac{(4 BernPoly (T + 1)) - (4 BernPoly 0)}{4} = \frac{((3 + 1) BernPoly (T + 1)) - ((3 + 1) BernPoly 0)}{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 BernPoly (T + 1) = ({(T + 1)}^{4} - 2 {(T + 1)}^{3}) + {(T + 1)}^{2} - (\frac{1}{30})$
13	11 12	syl	$⊢ T \in ℕ_{0} \to 4 BernPoly (T + 1) = ({(T + 1)}^{4} - 2 {(T + 1)}^{3}) + {(T + 1)}^{2} - (\frac{1}{30})$
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	$⊢ (0^{4} - 2 0^{3}) + 0^{2} - (\frac{1}{30}) = 0 - (\frac{1}{30})$
31		0cn	$⊢ 0 \in ℂ$
32		bpoly4	$⊢ 0 \in ℂ \to 4 BernPoly 0 = (0^{4} - 2 0^{3}) + 0^{2} - (\frac{1}{30})$
33	31 32	ax-mp	$⊢ 4 BernPoly 0 = (0^{4} - 2 0^{3}) + 0^{2} - (\frac{1}{30})$
34		df-neg	$⊢ - \frac{1}{30} = 0 - (\frac{1}{30})$
35	30 33 34	3eqtr4i	$⊢ 4 BernPoly 0 = - \frac{1}{30}$
36	35	a1i	$⊢ T \in ℕ_{0} \to 4 BernPoly 0 = - \frac{1}{30}$
37	13 36	oveq12d	$⊢ T \in ℕ_{0} \to (4 BernPoly (T + 1)) - (4 BernPoly 0) = ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) - (- \frac{1}{30})$
38		4nn0	$⊢ 4 \in ℕ_{0}$
39		expcl	$⊢ (T + 1 \in ℂ \land 4 \in ℕ_{0}) \to {(T + 1)}^{4} \in ℂ$
40	38 39	mpan2	$⊢ T + 1 \in ℂ \to {(T + 1)}^{4} \in ℂ$
41		2cn	$⊢ 2 \in ℂ$
42		expcl	$⊢ (T + 1 \in ℂ \land 3 \in ℕ_{0}) \to {(T + 1)}^{3} \in ℂ$
43	1 42	mpan2	$⊢ T + 1 \in ℂ \to {(T + 1)}^{3} \in ℂ$
44		mulcl	$⊢ (2 \in ℂ \land {(T + 1)}^{3} \in ℂ) \to 2 {(T + 1)}^{3} \in ℂ$
45	41 43 44	sylancr	$⊢ T + 1 \in ℂ \to 2 {(T + 1)}^{3} \in ℂ$
46	40 45	subcld	$⊢ T + 1 \in ℂ \to {(T + 1)}^{4} - 2 {(T + 1)}^{3} \in ℂ$
47		sqcl	$⊢ T + 1 \in ℂ \to {(T + 1)}^{2} \in ℂ$
48	46 47	addcld	$⊢ T + 1 \in ℂ \to {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2} \in ℂ$
49	10 48	syl	$⊢ T \in ℂ \to {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2} \in ℂ$
50	9 49	syl	$⊢ T \in ℕ_{0} \to {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{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 \neq 0$
58	53 57	reccli	$⊢ \frac{1}{30} \in ℂ$
59		subcl	$⊢ ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2} \in ℂ \land \frac{1}{30} \in ℂ) \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3}) + {(T + 1)}^{2} - (\frac{1}{30}) \in ℂ$
60	50 58 59	sylancl	$⊢ T \in ℕ_{0} \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3}) + {(T + 1)}^{2} - (\frac{1}{30}) \in ℂ$
61		subneg	$⊢ (({(T + 1)}^{4} - 2 {(T + 1)}^{3}) + {(T + 1)}^{2} - (\frac{1}{30}) \in ℂ \land \frac{1}{30} \in ℂ) \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) - (- \frac{1}{30}) = ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) + (\frac{1}{30})$
62	60 58 61	sylancl	$⊢ T \in ℕ_{0} \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) - (- \frac{1}{30}) = ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) + (\frac{1}{30})$
63		npcan	$⊢ ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2} \in ℂ \land \frac{1}{30} \in ℂ) \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) + (\frac{1}{30}) = {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}$
64	49 58 63	sylancl	$⊢ T \in ℂ \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) + (\frac{1}{30}) = {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}$
65	9 64	syl	$⊢ T \in ℕ_{0} \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) + (\frac{1}{30}) = {(T + 1)}^{4} - 2 {(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 {(T + 1)}^{3} = 2 {(T + 1)}^{2 + 1}$
72	68 71	oveq12i	$⊢ {(T + 1)}^{4} - 2 {(T + 1)}^{3} = {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1}$
73	72	oveq1i	$⊢ {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2} = {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1} + {(T + 1)}^{2}$
74		2nn0	$⊢ 2 \in ℕ_{0}$
75		expadd	$⊢ (T + 1 \in ℂ \land 2 \in ℕ_{0} \land 2 \in ℕ_{0}) \to {(T + 1)}^{2 + 2} = {(T + 1)}^{2} {(T + 1)}^{2}$
76	74 74 75	mp3an23	$⊢ T + 1 \in ℂ \to {(T + 1)}^{2 + 2} = {(T + 1)}^{2} {(T + 1)}^{2}$
77		1nn0	$⊢ 1 \in ℕ_{0}$
78		expadd	$⊢ (T + 1 \in ℂ \land 2 \in ℕ_{0} \land 1 \in ℕ_{0}) \to {(T + 1)}^{2 + 1} = {(T + 1)}^{2} {(T + 1)}^{1}$
79	74 77 78	mp3an23	$⊢ T + 1 \in ℂ \to {(T + 1)}^{2 + 1} = {(T + 1)}^{2} {(T + 1)}^{1}$
80	79	oveq2d	$⊢ T + 1 \in ℂ \to 2 {(T + 1)}^{2 + 1} = 2 {(T + 1)}^{2} {(T + 1)}^{1}$
81	76 80	oveq12d	$⊢ T + 1 \in ℂ \to {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1} = {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1}$
82	10 81	syl	$⊢ T \in ℂ \to {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1} = {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1}$
83	10	sqcld	$⊢ T \in ℂ \to {(T + 1)}^{2} \in ℂ$
84	83	mulridd	$⊢ T \in ℂ \to {(T + 1)}^{2} \cdot 1 = {(T + 1)}^{2}$
85	84	eqcomd	$⊢ T \in ℂ \to {(T + 1)}^{2} = {(T + 1)}^{2} \cdot 1$
86	82 85	oveq12d	$⊢ T \in ℂ \to {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1} + {(T + 1)}^{2} = {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1} + {(T + 1)}^{2} \cdot 1$
87	10	exp1d	$⊢ T \in ℂ \to {(T + 1)}^{1} = T + 1$
88	87	oveq2d	$⊢ T \in ℂ \to 2 {(T + 1)}^{1} = 2 (T + 1)$
89	88	oveq2d	$⊢ T \in ℂ \to {(T + 1)}^{2} 2 {(T + 1)}^{1} = {(T + 1)}^{2} 2 (T + 1)$
90	89	oveq2d	$⊢ T \in ℂ \to {(T + 1)}^{2} {(T + 1)}^{2} - {(T + 1)}^{2} 2 {(T + 1)}^{1} = {(T + 1)}^{2} {(T + 1)}^{2} - {(T + 1)}^{2} 2 (T + 1)$
91	87 10	eqeltrd	$⊢ T \in ℂ \to {(T + 1)}^{1} \in ℂ$
92		mul12	$⊢ (2 \in ℂ \land {(T + 1)}^{2} \in ℂ \land {(T + 1)}^{1} \in ℂ) \to 2 {(T + 1)}^{2} {(T + 1)}^{1} = {(T + 1)}^{2} 2 {(T + 1)}^{1}$
93	41 83 91 92	mp3an2i	$⊢ T \in ℂ \to 2 {(T + 1)}^{2} {(T + 1)}^{1} = {(T + 1)}^{2} 2 {(T + 1)}^{1}$
94	93	oveq2d	$⊢ T \in ℂ \to {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1} = {(T + 1)}^{2} {(T + 1)}^{2} - {(T + 1)}^{2} 2 {(T + 1)}^{1}$
95		mulcl	$⊢ (2 \in ℂ \land T + 1 \in ℂ) \to 2 (T + 1) \in ℂ$
96	41 10 95	sylancr	$⊢ T \in ℂ \to 2 (T + 1) \in ℂ$
97	83 83 96	subdid	$⊢ T \in ℂ \to {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1)) = {(T + 1)}^{2} {(T + 1)}^{2} - {(T + 1)}^{2} 2 (T + 1)$
98	90 94 97	3eqtr4d	$⊢ T \in ℂ \to {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1} = {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1))$
99	98	oveq1d	$⊢ T \in ℂ \to {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1} + {(T + 1)}^{2} \cdot 1 = {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1)) + {(T + 1)}^{2} \cdot 1$
100	83 96	subcld	$⊢ T \in ℂ \to {(T + 1)}^{2} - 2 (T + 1) \in ℂ$
101		ax-1cn	$⊢ 1 \in ℂ$
102		adddi	$⊢ ({(T + 1)}^{2} \in ℂ \land {(T + 1)}^{2} - 2 (T + 1) \in ℂ \land 1 \in ℂ) \to {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1) + 1) = {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1)) + {(T + 1)}^{2} \cdot 1$
103	101 102	mp3an3	$⊢ ({(T + 1)}^{2} \in ℂ \land {(T + 1)}^{2} - 2 (T + 1) \in ℂ) \to {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1) + 1) = {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1)) + {(T + 1)}^{2} \cdot 1$
104	83 100 103	syl2anc	$⊢ T \in ℂ \to {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1) + 1) = {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1)) + {(T + 1)}^{2} \cdot 1$
105	99 104	eqtr4d	$⊢ T \in ℂ \to {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1} + {(T + 1)}^{2} \cdot 1 = {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1) + 1)$
106		adddi	$⊢ (2 \in ℂ \land T \in ℂ \land 1 \in ℂ) \to 2 (T + 1) = 2 T + 2 \cdot 1$
107	41 101 106	mp3an13	$⊢ T \in ℂ \to 2 (T + 1) = 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	eqtrdi	$⊢ T \in ℂ \to 2 (T + 1) = 2 T + 2$
111	110	oveq1d	$⊢ T \in ℂ \to 2 (T + 1) - 1 = 2 T + 2 - 1$
112		mulcl	$⊢ (2 \in ℂ \land T \in ℂ) \to 2 T \in ℂ$
113	41 112	mpan	$⊢ T \in ℂ \to 2 T \in ℂ$
114		addsubass	$⊢ (2 T \in ℂ \land 2 \in ℂ \land 1 \in ℂ) \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	eqtrdi	$⊢ T \in ℂ \to 2 T + 2 - 1 = 2 T + 1$
120	111 119	eqtrd	$⊢ T \in ℂ \to 2 (T + 1) - 1 = 2 T + 1$
121	120	oveq2d	$⊢ T \in ℂ \to {(T + 1)}^{2} - (2 (T + 1) - 1) = {(T + 1)}^{2} - (2 T + 1)$
122		subsub	$⊢ ({(T + 1)}^{2} \in ℂ \land 2 (T + 1) \in ℂ \land 1 \in ℂ) \to {(T + 1)}^{2} - (2 (T + 1) - 1) = {(T + 1)}^{2} - 2 (T + 1) + 1$
123	101 122	mp3an3	$⊢ ({(T + 1)}^{2} \in ℂ \land 2 (T + 1) \in ℂ) \to {(T + 1)}^{2} - (2 (T + 1) - 1) = {(T + 1)}^{2} - 2 (T + 1) + 1$
124	83 96 123	syl2anc	$⊢ T \in ℂ \to {(T + 1)}^{2} - (2 (T + 1) - 1) = {(T + 1)}^{2} - 2 (T + 1) + 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 {(T + 1)}^{2} = T^{2} + 2 T + 1$
129		addass	$⊢ (T^{2} \in ℂ \land 2 T \in ℂ \land 1 \in ℂ) \to T^{2} + 2 T + 1 = T^{2} + 2 T + 1$
130	101 129	mp3an3	$⊢ (T^{2} \in ℂ \land 2 T \in ℂ) \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 {(T + 1)}^{2} = T^{2} + 2 T + 1$
133	125 127 132	mvrraddd	$⊢ T \in ℂ \to {(T + 1)}^{2} - (2 T + 1) = T^{2}$
134	121 124 133	3eqtr3d	$⊢ T \in ℂ \to {(T + 1)}^{2} - 2 (T + 1) + 1 = T^{2}$
135	134	oveq2d	$⊢ T \in ℂ \to {(T + 1)}^{2} ({(T + 1)}^{2} - 2 (T + 1) + 1) = {(T + 1)}^{2} T^{2}$
136	83 125	mulcomd	$⊢ T \in ℂ \to {(T + 1)}^{2} T^{2} = T^{2} {(T + 1)}^{2}$
137	105 135 136	3eqtrd	$⊢ T \in ℂ \to {(T + 1)}^{2} {(T + 1)}^{2} - 2 {(T + 1)}^{2} {(T + 1)}^{1} + {(T + 1)}^{2} \cdot 1 = T^{2} {(T + 1)}^{2}$
138	86 137	eqtrd	$⊢ T \in ℂ \to {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1} + {(T + 1)}^{2} = T^{2} {(T + 1)}^{2}$
139	9 138	syl	$⊢ T \in ℕ_{0} \to {(T + 1)}^{2 + 2} - 2 {(T + 1)}^{2 + 1} + {(T + 1)}^{2} = T^{2} {(T + 1)}^{2}$
140	73 139	eqtrid	$⊢ T \in ℕ_{0} \to {(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2} = T^{2} {(T + 1)}^{2}$
141	65 140	eqtrd	$⊢ T \in ℕ_{0} \to ({(T + 1)}^{4} - 2 {(T + 1)}^{3} + {(T + 1)}^{2}) - (\frac{1}{30}) + (\frac{1}{30}) = T^{2} {(T + 1)}^{2}$
142	37 62 141	3eqtrd	$⊢ T \in ℕ_{0} \to (4 BernPoly (T + 1)) - (4 BernPoly 0) = T^{2} {(T + 1)}^{2}$
143	142	oveq1d	$⊢ T \in ℕ_{0} \to \frac{(4 BernPoly (T + 1)) - (4 BernPoly 0)}{4} = \frac{T^{2} {(T + 1)}^{2}}{4}$
144	8 143	eqtr3id	$⊢ T \in ℕ_{0} \to \frac{((3 + 1) BernPoly (T + 1)) - ((3 + 1) BernPoly 0)}{3 + 1} = \frac{T^{2} {(T + 1)}^{2}}{4}$
145	3 144	eqtrd	$⊢ T \in ℕ_{0} \to \sum_{k = 0}^{T} k^{3} = \frac{T^{2} {(T + 1)}^{2}}{4}$

Metamath Proof Explorer

Theorem fsumcube

Proof