fsumcube - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fsumcube		Structured version Visualization version GIF version

Theorem fsumcube 16139

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

**Assertion**
Ref	Expression
fsumcube	⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))

Distinct variable group: 𝑇,𝑘

**Proof of Theorem fsumcube**
Step	Hyp	Ref	Expression
1		3nn0 12540	. . 3 ⊢ 3 ∈ ℕ₀
2		fsumkthpow 16135	. . 3 ⊢ ((3 ∈ ℕ₀ ∧ 𝑇 ∈ ℕ₀) → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)))
3	1, 2	mpan 703	. 2 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)))
4		df-4 12323	. . . . . 6 ⊢ 4 = (3 + 1)
5	4	oveq1i 7433	. . . . 5 ⊢ (4 BernPoly (𝑇 + 1)) = ((3 + 1) BernPoly (𝑇 + 1))
6	4	oveq1i 7433	. . . . 5 ⊢ (4 BernPoly 0) = ((3 + 1) BernPoly 0)
7	5, 6	oveq12i 7435	. . . 4 ⊢ ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = (((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0))
8	7, 4	oveq12i 7435	. . 3 ⊢ (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1))
9		nn0cn 12532	. . . . . . . 8 ⊢ (𝑇 ∈ ℕ₀ → 𝑇 ∈ ℂ)
10		peano2cn 11400	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 + 1) ∈ ℂ)
11	9, 10	syl 18	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → (𝑇 + 1) ∈ ℂ)
12		bpoly4 16138	. . . . . . 7 ⊢ ((𝑇 + 1) ∈ ℂ → (4 BernPoly (𝑇 + 1)) = (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)))
13	11, 12	syl 18	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (4 BernPoly (𝑇 + 1)) = (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)))
14		4nn 12342	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℕ
15		0exp 14153	. . . . . . . . . . . . . 14 ⊢ (4 ∈ ℕ → (0↑4) = 0)
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0↑4) = 0
17		3nn 12338	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ
18		0exp 14153	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℕ → (0↑3) = 0)
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (0↑3) = 0
20	19	oveq2i 7434	. . . . . . . . . . . . . 14 ⊢ (2 · (0↑3)) = (2 · 0)
21		2t0e0 12429	. . . . . . . . . . . . . 14 ⊢ (2 · 0) = 0
22	20, 21	eqtri 2789	. . . . . . . . . . . . 13 ⊢ (2 · (0↑3)) = 0
23	16, 22	oveq12i 7435	. . . . . . . . . . . 12 ⊢ ((0↑4) − (2 · (0↑3))) = (0 − 0)
24		0m0e0 12377	. . . . . . . . . . . 12 ⊢ (0 − 0) = 0
25	23, 24	eqtri 2789	. . . . . . . . . . 11 ⊢ ((0↑4) − (2 · (0↑3))) = 0
26		sq0 14248	. . . . . . . . . . 11 ⊢ (0↑2) = 0
27	25, 26	oveq12i 7435	. . . . . . . . . 10 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = (0 + 0)
28		00id 11403	. . . . . . . . . 10 ⊢ (0 + 0) = 0
29	27, 28	eqtri 2789	. . . . . . . . 9 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = 0
30	29	oveq1i 7433	. . . . . . . 8 ⊢ ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30)) = (0 − (1 / ;30))
31		0cn 11216	. . . . . . . . 9 ⊢ 0 ∈ ℂ
32		bpoly4 16138	. . . . . . . . 9 ⊢ (0 ∈ ℂ → (4 BernPoly 0) = ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30)))
33	31, 32	ax-mp 5	. . . . . . . 8 ⊢ (4 BernPoly 0) = ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30))
34		df-neg 11462	. . . . . . . 8 ⊢ -(1 / ;30) = (0 − (1 / ;30))
35	30, 33, 34	3eqtr4i 2799	. . . . . . 7 ⊢ (4 BernPoly 0) = -(1 / ;30)
36	35	a1i 11	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (4 BernPoly 0) = -(1 / ;30))
37	13, 36	oveq12d 7441	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)))
38		4nn0 12541	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
39		expcl 14135	. . . . . . . . . . . 12 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 4 ∈ ℕ₀) → ((𝑇 + 1)↑4) ∈ ℂ)
40	38, 39	mpan2 704	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑4) ∈ ℂ)
41		2cn 12334	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
42		expcl 14135	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑇 + 1)↑3) ∈ ℂ)
43	1, 42	mpan2 704	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑3) ∈ ℂ)
44		mulcl 11202	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑3) ∈ ℂ) → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
45	41, 43, 44	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
46	40, 45	subcld 11587	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) ∈ ℂ)
47		sqcl 14174	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
48	46, 47	addcld 11246	. . . . . . . . 9 ⊢ ((𝑇 + 1) ∈ ℂ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ)
49	10, 48	syl 18	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ)
50	9, 49	syl 18	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ)
51		0nn0 12537	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
52	1, 51	deccl 12744	. . . . . . . . 9 ⊢ ;30 ∈ ℕ₀
53	52	nn0cni 12534	. . . . . . . 8 ⊢ ;30 ∈ ℂ
54	52	nn0rei 12533	. . . . . . . . 9 ⊢ ;30 ∈ ℝ
55		10pos 12750	. . . . . . . . . 10 ⊢ 0 < ;10
56	17, 51, 51, 55	declti 12772	. . . . . . . . 9 ⊢ 0 < ;30
57	54, 56	gt0ne0ii 11768	. . . . . . . 8 ⊢ ;30 ≠ 0
58	53, 57	reccli 11963	. . . . . . 7 ⊢ (1 / ;30) ∈ ℂ
59		subcl 11474	. . . . . . 7 ⊢ ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ ∧ (1 / ;30) ∈ ℂ) → (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ)
60	50, 58, 59	sylancl 598	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ)
61		subneg 11525	. . . . . 6 ⊢ (((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ ∧ (1 / ;30) ∈ ℂ) → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)))
62	60, 58, 61	sylancl 598	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)))
63		npcan 11484	. . . . . . . 8 ⊢ ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ ∧ (1 / ;30) ∈ ℂ) → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)))
64	49, 58, 63	sylancl 598	. . . . . . 7 ⊢ (𝑇 ∈ ℂ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)))
65	9, 64	syl 18	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)))
66		2p2e4 12393	. . . . . . . . . . 11 ⊢ (2 + 2) = 4
67	66	eqcomi 2775	. . . . . . . . . 10 ⊢ 4 = (2 + 2)
68	67	oveq2i 7434	. . . . . . . . 9 ⊢ ((𝑇 + 1)↑4) = ((𝑇 + 1)↑(2 + 2))
69		df-3 12322	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
70	69	oveq2i 7434	. . . . . . . . . 10 ⊢ ((𝑇 + 1)↑3) = ((𝑇 + 1)↑(2 + 1))
71	70	oveq2i 7434	. . . . . . . . 9 ⊢ (2 · ((𝑇 + 1)↑3)) = (2 · ((𝑇 + 1)↑(2 + 1)))
72	68, 71	oveq12i 7435	. . . . . . . 8 ⊢ (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) = (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1))))
73	72	oveq1i 7433	. . . . . . 7 ⊢ ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2))
74		2nn0 12539	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
75		expadd 14160	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → ((𝑇 + 1)↑(2 + 2)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)))
76	74, 74, 75	mp3an23 1482	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑(2 + 2)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)))
77		1nn0 12538	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
78		expadd 14160	. . . . . . . . . . . . . 14 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → ((𝑇 + 1)↑(2 + 1)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))
79	74, 77, 78	mp3an23 1482	. . . . . . . . . . . . 13 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑(2 + 1)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))
80	79	oveq2d 7439	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑(2 + 1))) = (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))))
81	76, 80	oveq12d 7441	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))))
82	10, 81	syl 18	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))))
83	10	sqcld 14200	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
84	83	mulridd 11244	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · 1) = ((𝑇 + 1)↑2))
85	84	eqcomd 2772	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇 + 1)↑2) · 1))
86	82, 85	oveq12d 7441	. . . . . . . . 9 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2)) = (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)))
87	10	exp1d 14197	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) = (𝑇 + 1))
88	87	oveq2d 7439	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · ((𝑇 + 1)↑1)) = (2 · (𝑇 + 1)))
89	88	oveq2d 7439	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · (𝑇 + 1))))
90	89	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
91	87, 10	eqeltrd 2866	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) ∈ ℂ)
92		mul12 11393	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑2) ∈ ℂ ∧ ((𝑇 + 1)↑1) ∈ ℂ) → (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))))
93	41, 83, 91, 92	mp3an2i 1495	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))))
94	93	oveq2d 7439	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))))
95		mulcl 11202	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (𝑇 + 1) ∈ ℂ) → (2 · (𝑇 + 1)) ∈ ℂ)
96	41, 10, 95	sylancr 599	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) ∈ ℂ)
97	83, 83, 96	subdid 11688	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
98	90, 94, 97	3eqtr4d 2811	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))))
99	98	oveq1d 7438	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 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 11587	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) ∈ ℂ)
101		ax-1cn 11176	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
102		adddi 11207	. . . . . . . . . . . . 13 ⊢ ((((𝑇 + 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 1479	. . . . . . . . . . . 12 ⊢ ((((𝑇 + 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 596	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = ((((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) + (((𝑇 + 1)↑2) · 1)))
105	99, 104	eqtr4d 2804	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)))
106		adddi 11207	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
107	41, 101, 106	mp3an13 1481	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
108		2t1e2 12421	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) = 2
109	108	oveq2i 7434	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) + (2 · 1)) = ((2 · 𝑇) + 2)
110	107, 109	eqtrdi 2817	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + 2))
111	110	oveq1d 7438	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = (((2 · 𝑇) + 2) − 1))
112		mulcl 11202	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (2 · 𝑇) ∈ ℂ)
113	41, 112	mpan 703	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · 𝑇) ∈ ℂ)
114		addsubass 11485	. . . . . . . . . . . . . . . . 17 ⊢ (((2 · 𝑇) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
115	41, 101, 114	mp3an23 1482	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
116	113, 115	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
117		2m1e1 12383	. . . . . . . . . . . . . . . 16 ⊢ (2 − 1) = 1
118	117	oveq2i 7434	. . . . . . . . . . . . . . 15 ⊢ ((2 · 𝑇) + (2 − 1)) = ((2 · 𝑇) + 1)
119	116, 118	eqtrdi 2817	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + 1))
120	111, 119	eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = ((2 · 𝑇) + 1))
121	120	oveq2d 7439	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)))
122		subsub 11506	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 + 1)↑2) ∈ ℂ ∧ (2 · (𝑇 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
123	101, 122	mp3an3 1479	. . . . . . . . . . . . 13 ⊢ ((((𝑇 + 1)↑2) ∈ ℂ ∧ (2 · (𝑇 + 1)) ∈ ℂ) → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
124	83, 96, 123	syl2anc 596	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
125		sqcl 14174	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (𝑇↑2) ∈ ℂ)
126		peano2cn 11400	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑇) ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
127	113, 126	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
128		binom21 14275	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇↑2) + (2 · 𝑇)) + 1))
129		addass 11205	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇↑2) ∈ ℂ ∧ (2 · 𝑇) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
130	101, 129	mp3an3 1479	. . . . . . . . . . . . . . 15 ⊢ (((𝑇↑2) ∈ ℂ ∧ (2 · 𝑇) ∈ ℂ) → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
131	125, 113, 130	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
132	128, 131	eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
133	125, 127, 132	mvrraddd 11644	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)) = (𝑇↑2))
134	121, 124, 133	3eqtr3d 2809	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1) = (𝑇↑2))
135	134	oveq2d 7439	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = (((𝑇 + 1)↑2) · (𝑇↑2)))
136	83, 125	mulcomd 11248	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (𝑇↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
137	105, 135, 136	3eqtrd 2805	. . . . . . . . 9 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
138	86, 137	eqtrd 2801	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
139	9, 138	syl 18	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
140	73, 139	eqtrid 2813	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
141	65, 140	eqtrd 2801	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
142	37, 62, 141	3eqtrd 2805	. . . 4 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
143	142	oveq1d 7438	. . 3 ⊢ (𝑇 ∈ ℕ₀ → (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
144	8, 143	eqtr3id 2815	. 2 ⊢ (𝑇 ∈ ℕ₀ → ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
145	3, 144	eqtrd 2801	1 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2146 (class class class)co 7423 ℂcc 11116 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 − cmin 11459 -cneg 11460 / cdiv 11889 ℕcn 12251 2c2 12313 3c3 12314 4c4 12315 ℕ₀cn0 12522 cdc 12729 ...cfz 13553 ↑cexp 14117 Σcsu 15763 BernPoly cbp 16125

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-sup 9412 df-oi 9482 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12523 df-z 12610 df-dec 12730 df-uz 12881 df-rp 13035 df-fz 13554 df-fzo 13702 df-seq 14058 df-exp 14118 df-fac 14330 df-bc 14359 df-hash 14387 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-clim 15565 df-sum 15764 df-bpoly 16126

This theorem is used by: (None)

W3C validator