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 16025

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 12455	. . 3 ⊢ 3 ∈ ℕ₀
2		fsumkthpow 16021	. . 3 ⊢ ((3 ∈ ℕ₀ ∧ 𝑇 ∈ ℕ₀) → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)))
3	1, 2	mpan 691	. 2 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)))
4		df-4 12246	. . . . . 6 ⊢ 4 = (3 + 1)
5	4	oveq1i 7377	. . . . 5 ⊢ (4 BernPoly (𝑇 + 1)) = ((3 + 1) BernPoly (𝑇 + 1))
6	4	oveq1i 7377	. . . . 5 ⊢ (4 BernPoly 0) = ((3 + 1) BernPoly 0)
7	5, 6	oveq12i 7379	. . . 4 ⊢ ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = (((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0))
8	7, 4	oveq12i 7379	. . 3 ⊢ (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1))
9		nn0cn 12447	. . . . . . . 8 ⊢ (𝑇 ∈ ℕ₀ → 𝑇 ∈ ℂ)
10		peano2cn 11318	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 + 1) ∈ ℂ)
11	9, 10	syl 17	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → (𝑇 + 1) ∈ ℂ)
12		bpoly4 16024	. . . . . . 7 ⊢ ((𝑇 + 1) ∈ ℂ → (4 BernPoly (𝑇 + 1)) = (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)))
13	11, 12	syl 17	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (4 BernPoly (𝑇 + 1)) = (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)))
14		4nn 12264	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℕ
15		0exp 14059	. . . . . . . . . . . . . 14 ⊢ (4 ∈ ℕ → (0↑4) = 0)
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0↑4) = 0
17		3nn 12260	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ
18		0exp 14059	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℕ → (0↑3) = 0)
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (0↑3) = 0
20	19	oveq2i 7378	. . . . . . . . . . . . . 14 ⊢ (2 · (0↑3)) = (2 · 0)
21		2t0e0 12345	. . . . . . . . . . . . . 14 ⊢ (2 · 0) = 0
22	20, 21	eqtri 2759	. . . . . . . . . . . . 13 ⊢ (2 · (0↑3)) = 0
23	16, 22	oveq12i 7379	. . . . . . . . . . . 12 ⊢ ((0↑4) − (2 · (0↑3))) = (0 − 0)
24		0m0e0 12296	. . . . . . . . . . . 12 ⊢ (0 − 0) = 0
25	23, 24	eqtri 2759	. . . . . . . . . . 11 ⊢ ((0↑4) − (2 · (0↑3))) = 0
26		sq0 14154	. . . . . . . . . . 11 ⊢ (0↑2) = 0
27	25, 26	oveq12i 7379	. . . . . . . . . 10 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = (0 + 0)
28		00id 11321	. . . . . . . . . 10 ⊢ (0 + 0) = 0
29	27, 28	eqtri 2759	. . . . . . . . 9 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = 0
30	29	oveq1i 7377	. . . . . . . 8 ⊢ ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30)) = (0 − (1 / ;30))
31		0cn 11136	. . . . . . . . 9 ⊢ 0 ∈ ℂ
32		bpoly4 16024	. . . . . . . . 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 11380	. . . . . . . 8 ⊢ -(1 / ;30) = (0 − (1 / ;30))
35	30, 33, 34	3eqtr4i 2769	. . . . . . 7 ⊢ (4 BernPoly 0) = -(1 / ;30)
36	35	a1i 11	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (4 BernPoly 0) = -(1 / ;30))
37	13, 36	oveq12d 7385	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)))
38		4nn0 12456	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
39		expcl 14041	. . . . . . . . . . . 12 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 4 ∈ ℕ₀) → ((𝑇 + 1)↑4) ∈ ℂ)
40	38, 39	mpan2 692	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑4) ∈ ℂ)
41		2cn 12256	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
42		expcl 14041	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑇 + 1)↑3) ∈ ℂ)
43	1, 42	mpan2 692	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑3) ∈ ℂ)
44		mulcl 11122	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑3) ∈ ℂ) → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
45	41, 43, 44	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
46	40, 45	subcld 11505	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) ∈ ℂ)
47		sqcl 14080	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
48	46, 47	addcld 11164	. . . . . . . . 9 ⊢ ((𝑇 + 1) ∈ ℂ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ)
49	10, 48	syl 17	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ)
50	9, 49	syl 17	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ)
51		0nn0 12452	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
52	1, 51	deccl 12659	. . . . . . . . 9 ⊢ ;30 ∈ ℕ₀
53	52	nn0cni 12449	. . . . . . . 8 ⊢ ;30 ∈ ℂ
54	52	nn0rei 12448	. . . . . . . . 9 ⊢ ;30 ∈ ℝ
55		10pos 12661	. . . . . . . . . 10 ⊢ 0 < ;10
56	17, 51, 51, 55	declti 12682	. . . . . . . . 9 ⊢ 0 < ;30
57	54, 56	gt0ne0ii 11686	. . . . . . . 8 ⊢ ;30 ≠ 0
58	53, 57	reccli 11885	. . . . . . 7 ⊢ (1 / ;30) ∈ ℂ
59		subcl 11392	. . . . . . 7 ⊢ ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ ∧ (1 / ;30) ∈ ℂ) → (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ)
60	50, 58, 59	sylancl 587	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ)
61		subneg 11443	. . . . . 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 587	. . . . 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 11402	. . . . . . . 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 587	. . . . . . 7 ⊢ (𝑇 ∈ ℂ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)))
65	9, 64	syl 17	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)))
66		2p2e4 12311	. . . . . . . . . . 11 ⊢ (2 + 2) = 4
67	66	eqcomi 2745	. . . . . . . . . 10 ⊢ 4 = (2 + 2)
68	67	oveq2i 7378	. . . . . . . . 9 ⊢ ((𝑇 + 1)↑4) = ((𝑇 + 1)↑(2 + 2))
69		df-3 12245	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
70	69	oveq2i 7378	. . . . . . . . . 10 ⊢ ((𝑇 + 1)↑3) = ((𝑇 + 1)↑(2 + 1))
71	70	oveq2i 7378	. . . . . . . . 9 ⊢ (2 · ((𝑇 + 1)↑3)) = (2 · ((𝑇 + 1)↑(2 + 1)))
72	68, 71	oveq12i 7379	. . . . . . . 8 ⊢ (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) = (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1))))
73	72	oveq1i 7377	. . . . . . 7 ⊢ ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2))
74		2nn0 12454	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
75		expadd 14066	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → ((𝑇 + 1)↑(2 + 2)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)))
76	74, 74, 75	mp3an23 1456	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑(2 + 2)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)))
77		1nn0 12453	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
78		expadd 14066	. . . . . . . . . . . . . 14 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → ((𝑇 + 1)↑(2 + 1)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))
79	74, 77, 78	mp3an23 1456	. . . . . . . . . . . . 13 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑(2 + 1)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))
80	79	oveq2d 7383	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑(2 + 1))) = (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))))
81	76, 80	oveq12d 7385	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))))
82	10, 81	syl 17	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))))
83	10	sqcld 14106	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
84	83	mulridd 11162	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · 1) = ((𝑇 + 1)↑2))
85	84	eqcomd 2742	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇 + 1)↑2) · 1))
86	82, 85	oveq12d 7385	. . . . . . . . 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 14103	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) = (𝑇 + 1))
88	87	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · ((𝑇 + 1)↑1)) = (2 · (𝑇 + 1)))
89	88	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · (𝑇 + 1))))
90	89	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
91	87, 10	eqeltrd 2836	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) ∈ ℂ)
92		mul12 11311	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑2) ∈ ℂ ∧ ((𝑇 + 1)↑1) ∈ ℂ) → (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))))
93	41, 83, 91, 92	mp3an2i 1469	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))))
94	93	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))))
95		mulcl 11122	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (𝑇 + 1) ∈ ℂ) → (2 · (𝑇 + 1)) ∈ ℂ)
96	41, 10, 95	sylancr 588	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) ∈ ℂ)
97	83, 83, 96	subdid 11606	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
98	90, 94, 97	3eqtr4d 2781	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))))
99	98	oveq1d 7382	. . . . . . . . . . 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 11505	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) ∈ ℂ)
101		ax-1cn 11096	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
102		adddi 11127	. . . . . . . . . . . . 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 1453	. . . . . . . . . . . 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 585	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = ((((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) + (((𝑇 + 1)↑2) · 1)))
105	99, 104	eqtr4d 2774	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)))
106		adddi 11127	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
107	41, 101, 106	mp3an13 1455	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
108		2t1e2 12339	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) = 2
109	108	oveq2i 7378	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) + (2 · 1)) = ((2 · 𝑇) + 2)
110	107, 109	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + 2))
111	110	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = (((2 · 𝑇) + 2) − 1))
112		mulcl 11122	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (2 · 𝑇) ∈ ℂ)
113	41, 112	mpan 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · 𝑇) ∈ ℂ)
114		addsubass 11403	. . . . . . . . . . . . . . . . 17 ⊢ (((2 · 𝑇) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
115	41, 101, 114	mp3an23 1456	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
116	113, 115	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
117		2m1e1 12302	. . . . . . . . . . . . . . . 16 ⊢ (2 − 1) = 1
118	117	oveq2i 7378	. . . . . . . . . . . . . . 15 ⊢ ((2 · 𝑇) + (2 − 1)) = ((2 · 𝑇) + 1)
119	116, 118	eqtrdi 2787	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + 1))
120	111, 119	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = ((2 · 𝑇) + 1))
121	120	oveq2d 7383	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)))
122		subsub 11424	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 + 1)↑2) ∈ ℂ ∧ (2 · (𝑇 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
123	101, 122	mp3an3 1453	. . . . . . . . . . . . 13 ⊢ ((((𝑇 + 1)↑2) ∈ ℂ ∧ (2 · (𝑇 + 1)) ∈ ℂ) → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
124	83, 96, 123	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
125		sqcl 14080	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (𝑇↑2) ∈ ℂ)
126		peano2cn 11318	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑇) ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
127	113, 126	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
128		binom21 14181	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇↑2) + (2 · 𝑇)) + 1))
129		addass 11125	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇↑2) ∈ ℂ ∧ (2 · 𝑇) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
130	101, 129	mp3an3 1453	. . . . . . . . . . . . . . 15 ⊢ (((𝑇↑2) ∈ ℂ ∧ (2 · 𝑇) ∈ ℂ) → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
131	125, 113, 130	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
132	128, 131	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
133	125, 127, 132	mvrraddd 11562	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)) = (𝑇↑2))
134	121, 124, 133	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1) = (𝑇↑2))
135	134	oveq2d 7383	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = (((𝑇 + 1)↑2) · (𝑇↑2)))
136	83, 125	mulcomd 11166	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (𝑇↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
137	105, 135, 136	3eqtrd 2775	. . . . . . . . 9 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
138	86, 137	eqtrd 2771	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
139	9, 138	syl 17	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
140	73, 139	eqtrid 2783	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
141	65, 140	eqtrd 2771	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
142	37, 62, 141	3eqtrd 2775	. . . 4 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
143	142	oveq1d 7382	. . 3 ⊢ (𝑇 ∈ ℕ₀ → (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
144	8, 143	eqtr3id 2785	. 2 ⊢ (𝑇 ∈ ℕ₀ → ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
145	3, 144	eqtrd 2771	1 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 (class class class)co 7367 ℂcc 11036 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 − cmin 11377 -cneg 11378 / cdiv 11807 ℕcn 12174 2c2 12236 3c3 12237 4c4 12238 ℕ₀cn0 12437 cdc 12644 ...cfz 13461 ↑cexp 14023 Σcsu 15648 BernPoly cbp 16011

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-isom 6507 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-sup 9355 df-oi 9425 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-4 12246 df-5 12247 df-6 12248 df-7 12249 df-8 12250 df-9 12251 df-n0 12438 df-z 12525 df-dec 12645 df-uz 12789 df-rp 12943 df-fz 13462 df-fzo 13609 df-seq 13964 df-exp 14024 df-fac 14236 df-bc 14265 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-sum 15649 df-bpoly 16012

This theorem is referenced by: (None)

W3C validator