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 15985

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 12420	. . 3 ⊢ 3 ∈ ℕ₀
2		fsumkthpow 15981	. . 3 ⊢ ((3 ∈ ℕ₀ ∧ 𝑇 ∈ ℕ₀) → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)))
3	1, 2	mpan 690	. 2 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)))
4		df-4 12211	. . . . . 6 ⊢ 4 = (3 + 1)
5	4	oveq1i 7363	. . . . 5 ⊢ (4 BernPoly (𝑇 + 1)) = ((3 + 1) BernPoly (𝑇 + 1))
6	4	oveq1i 7363	. . . . 5 ⊢ (4 BernPoly 0) = ((3 + 1) BernPoly 0)
7	5, 6	oveq12i 7365	. . . 4 ⊢ ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = (((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0))
8	7, 4	oveq12i 7365	. . 3 ⊢ (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1))
9		nn0cn 12412	. . . . . . . 8 ⊢ (𝑇 ∈ ℕ₀ → 𝑇 ∈ ℂ)
10		peano2cn 11306	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 + 1) ∈ ℂ)
11	9, 10	syl 17	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → (𝑇 + 1) ∈ ℂ)
12		bpoly4 15984	. . . . . . 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 12229	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℕ
15		0exp 14022	. . . . . . . . . . . . . 14 ⊢ (4 ∈ ℕ → (0↑4) = 0)
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0↑4) = 0
17		3nn 12225	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ
18		0exp 14022	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℕ → (0↑3) = 0)
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (0↑3) = 0
20	19	oveq2i 7364	. . . . . . . . . . . . . 14 ⊢ (2 · (0↑3)) = (2 · 0)
21		2t0e0 12310	. . . . . . . . . . . . . 14 ⊢ (2 · 0) = 0
22	20, 21	eqtri 2752	. . . . . . . . . . . . 13 ⊢ (2 · (0↑3)) = 0
23	16, 22	oveq12i 7365	. . . . . . . . . . . 12 ⊢ ((0↑4) − (2 · (0↑3))) = (0 − 0)
24		0m0e0 12261	. . . . . . . . . . . 12 ⊢ (0 − 0) = 0
25	23, 24	eqtri 2752	. . . . . . . . . . 11 ⊢ ((0↑4) − (2 · (0↑3))) = 0
26		sq0 14117	. . . . . . . . . . 11 ⊢ (0↑2) = 0
27	25, 26	oveq12i 7365	. . . . . . . . . 10 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = (0 + 0)
28		00id 11309	. . . . . . . . . 10 ⊢ (0 + 0) = 0
29	27, 28	eqtri 2752	. . . . . . . . 9 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = 0
30	29	oveq1i 7363	. . . . . . . 8 ⊢ ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30)) = (0 − (1 / ;30))
31		0cn 11126	. . . . . . . . 9 ⊢ 0 ∈ ℂ
32		bpoly4 15984	. . . . . . . . 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 11368	. . . . . . . 8 ⊢ -(1 / ;30) = (0 − (1 / ;30))
35	30, 33, 34	3eqtr4i 2762	. . . . . . 7 ⊢ (4 BernPoly 0) = -(1 / ;30)
36	35	a1i 11	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (4 BernPoly 0) = -(1 / ;30))
37	13, 36	oveq12d 7371	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)))
38		4nn0 12421	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
39		expcl 14004	. . . . . . . . . . . 12 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 4 ∈ ℕ₀) → ((𝑇 + 1)↑4) ∈ ℂ)
40	38, 39	mpan2 691	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑4) ∈ ℂ)
41		2cn 12221	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
42		expcl 14004	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑇 + 1)↑3) ∈ ℂ)
43	1, 42	mpan2 691	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑3) ∈ ℂ)
44		mulcl 11112	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑3) ∈ ℂ) → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
45	41, 43, 44	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
46	40, 45	subcld 11493	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) ∈ ℂ)
47		sqcl 14043	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
48	46, 47	addcld 11153	. . . . . . . . 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 12417	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
52	1, 51	deccl 12624	. . . . . . . . 9 ⊢ ;30 ∈ ℕ₀
53	52	nn0cni 12414	. . . . . . . 8 ⊢ ;30 ∈ ℂ
54	52	nn0rei 12413	. . . . . . . . 9 ⊢ ;30 ∈ ℝ
55		10pos 12626	. . . . . . . . . 10 ⊢ 0 < ;10
56	17, 51, 51, 55	declti 12647	. . . . . . . . 9 ⊢ 0 < ;30
57	54, 56	gt0ne0ii 11674	. . . . . . . 8 ⊢ ;30 ≠ 0
58	53, 57	reccli 11872	. . . . . . 7 ⊢ (1 / ;30) ∈ ℂ
59		subcl 11380	. . . . . . 7 ⊢ ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) ∈ ℂ ∧ (1 / ;30) ∈ ℂ) → (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ)
60	50, 58, 59	sylancl 586	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) ∈ ℂ)
61		subneg 11431	. . . . . 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 586	. . . . 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 11390	. . . . . . . 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 586	. . . . . . 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 12276	. . . . . . . . . . 11 ⊢ (2 + 2) = 4
67	66	eqcomi 2738	. . . . . . . . . 10 ⊢ 4 = (2 + 2)
68	67	oveq2i 7364	. . . . . . . . 9 ⊢ ((𝑇 + 1)↑4) = ((𝑇 + 1)↑(2 + 2))
69		df-3 12210	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
70	69	oveq2i 7364	. . . . . . . . . 10 ⊢ ((𝑇 + 1)↑3) = ((𝑇 + 1)↑(2 + 1))
71	70	oveq2i 7364	. . . . . . . . 9 ⊢ (2 · ((𝑇 + 1)↑3)) = (2 · ((𝑇 + 1)↑(2 + 1)))
72	68, 71	oveq12i 7365	. . . . . . . 8 ⊢ (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) = (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1))))
73	72	oveq1i 7363	. . . . . . 7 ⊢ ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2))
74		2nn0 12419	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
75		expadd 14029	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 2 ∈ ℕ₀) → ((𝑇 + 1)↑(2 + 2)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)))
76	74, 74, 75	mp3an23 1455	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑(2 + 2)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)))
77		1nn0 12418	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
78		expadd 14029	. . . . . . . . . . . . . 14 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 2 ∈ ℕ₀ ∧ 1 ∈ ℕ₀) → ((𝑇 + 1)↑(2 + 1)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))
79	74, 77, 78	mp3an23 1455	. . . . . . . . . . . . 13 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑(2 + 1)) = (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))
80	79	oveq2d 7369	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑(2 + 1))) = (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))))
81	76, 80	oveq12d 7371	. . . . . . . . . . 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 14069	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
84	83	mulridd 11151	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · 1) = ((𝑇 + 1)↑2))
85	84	eqcomd 2735	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇 + 1)↑2) · 1))
86	82, 85	oveq12d 7371	. . . . . . . . 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 14066	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) = (𝑇 + 1))
88	87	oveq2d 7369	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · ((𝑇 + 1)↑1)) = (2 · (𝑇 + 1)))
89	88	oveq2d 7369	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · (𝑇 + 1))))
90	89	oveq2d 7369	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
91	87, 10	eqeltrd 2828	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) ∈ ℂ)
92		mul12 11299	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑2) ∈ ℂ ∧ ((𝑇 + 1)↑1) ∈ ℂ) → (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))))
93	41, 83, 91, 92	mp3an2i 1468	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))))
94	93	oveq2d 7369	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))))
95		mulcl 11112	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (𝑇 + 1) ∈ ℂ) → (2 · (𝑇 + 1)) ∈ ℂ)
96	41, 10, 95	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) ∈ ℂ)
97	83, 83, 96	subdid 11594	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
98	90, 94, 97	3eqtr4d 2774	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))))
99	98	oveq1d 7368	. . . . . . . . . . 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 11493	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) ∈ ℂ)
101		ax-1cn 11086	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
102		adddi 11117	. . . . . . . . . . . . 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 1452	. . . . . . . . . . . 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 584	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = ((((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) + (((𝑇 + 1)↑2) · 1)))
105	99, 104	eqtr4d 2767	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)))
106		adddi 11117	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
107	41, 101, 106	mp3an13 1454	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
108		2t1e2 12304	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) = 2
109	108	oveq2i 7364	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) + (2 · 1)) = ((2 · 𝑇) + 2)
110	107, 109	eqtrdi 2780	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + 2))
111	110	oveq1d 7368	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = (((2 · 𝑇) + 2) − 1))
112		mulcl 11112	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (2 · 𝑇) ∈ ℂ)
113	41, 112	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · 𝑇) ∈ ℂ)
114		addsubass 11391	. . . . . . . . . . . . . . . . 17 ⊢ (((2 · 𝑇) ∈ ℂ ∧ 2 ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
115	41, 101, 114	mp3an23 1455	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
116	113, 115	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + (2 − 1)))
117		2m1e1 12267	. . . . . . . . . . . . . . . 16 ⊢ (2 − 1) = 1
118	117	oveq2i 7364	. . . . . . . . . . . . . . 15 ⊢ ((2 · 𝑇) + (2 − 1)) = ((2 · 𝑇) + 1)
119	116, 118	eqtrdi 2780	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + 1))
120	111, 119	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = ((2 · 𝑇) + 1))
121	120	oveq2d 7369	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)))
122		subsub 11412	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 + 1)↑2) ∈ ℂ ∧ (2 · (𝑇 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
123	101, 122	mp3an3 1452	. . . . . . . . . . . . 13 ⊢ ((((𝑇 + 1)↑2) ∈ ℂ ∧ (2 · (𝑇 + 1)) ∈ ℂ) → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
124	83, 96, 123	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1))
125		sqcl 14043	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (𝑇↑2) ∈ ℂ)
126		peano2cn 11306	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑇) ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
127	113, 126	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
128		binom21 14144	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇↑2) + (2 · 𝑇)) + 1))
129		addass 11115	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇↑2) ∈ ℂ ∧ (2 · 𝑇) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
130	101, 129	mp3an3 1452	. . . . . . . . . . . . . . 15 ⊢ (((𝑇↑2) ∈ ℂ ∧ (2 · 𝑇) ∈ ℂ) → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
131	125, 113, 130	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇↑2) + (2 · 𝑇)) + 1) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
132	128, 131	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
133	125, 127, 132	mvrraddd 11550	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)) = (𝑇↑2))
134	121, 124, 133	3eqtr3d 2772	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1) = (𝑇↑2))
135	134	oveq2d 7369	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = (((𝑇 + 1)↑2) · (𝑇↑2)))
136	83, 125	mulcomd 11155	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (𝑇↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
137	105, 135, 136	3eqtrd 2768	. . . . . . . . 9 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
138	86, 137	eqtrd 2764	. . . . . . . 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 2776	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
141	65, 140	eqtrd 2764	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
142	37, 62, 141	3eqtrd 2768	. . . 4 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
143	142	oveq1d 7368	. . 3 ⊢ (𝑇 ∈ ℕ₀ → (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
144	8, 143	eqtr3id 2778	. 2 ⊢ (𝑇 ∈ ℕ₀ → ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
145	3, 144	eqtrd 2764	1 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2109 (class class class)co 7353 ℂcc 11026 0cc0 11028 1c1 11029 + caddc 11031 · cmul 11033 − cmin 11365 -cneg 11366 / cdiv 11795 ℕcn 12146 2c2 12201 3c3 12202 4c4 12203 ℕ₀cn0 12402 cdc 12609 ...cfz 13428 ↑cexp 13986 Σcsu 15611 BernPoly cbp 15971

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-inf2 9556 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8632 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9351 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-div 11796 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-rp 12912 df-fz 13429 df-fzo 13576 df-seq 13927 df-exp 13987 df-fac 14199 df-bc 14228 df-hash 14256 df-cj 15024 df-re 15025 df-im 15026 df-sqrt 15160 df-abs 15161 df-clim 15413 df-sum 15612 df-bpoly 15972

This theorem is referenced by: (None)

W3C validator