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 16096

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 12544	. . 3 ⊢ 3 ∈ ℕ₀
2		fsumkthpow 16092	. . 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 12331	. . . . . 6 ⊢ 4 = (3 + 1)
5	4	oveq1i 7441	. . . . 5 ⊢ (4 BernPoly (𝑇 + 1)) = ((3 + 1) BernPoly (𝑇 + 1))
6	4	oveq1i 7441	. . . . 5 ⊢ (4 BernPoly 0) = ((3 + 1) BernPoly 0)
7	5, 6	oveq12i 7443	. . . 4 ⊢ ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = (((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0))
8	7, 4	oveq12i 7443	. . 3 ⊢ (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1))
9		nn0cn 12536	. . . . . . . 8 ⊢ (𝑇 ∈ ℕ₀ → 𝑇 ∈ ℂ)
10		peano2cn 11433	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 + 1) ∈ ℂ)
11	9, 10	syl 17	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → (𝑇 + 1) ∈ ℂ)
12		bpoly4 16095	. . . . . . 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 12349	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℕ
15		0exp 14138	. . . . . . . . . . . . . 14 ⊢ (4 ∈ ℕ → (0↑4) = 0)
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0↑4) = 0
17		3nn 12345	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ
18		0exp 14138	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℕ → (0↑3) = 0)
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (0↑3) = 0
20	19	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ (2 · (0↑3)) = (2 · 0)
21		2t0e0 12435	. . . . . . . . . . . . . 14 ⊢ (2 · 0) = 0
22	20, 21	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (2 · (0↑3)) = 0
23	16, 22	oveq12i 7443	. . . . . . . . . . . 12 ⊢ ((0↑4) − (2 · (0↑3))) = (0 − 0)
24		0m0e0 12386	. . . . . . . . . . . 12 ⊢ (0 − 0) = 0
25	23, 24	eqtri 2765	. . . . . . . . . . 11 ⊢ ((0↑4) − (2 · (0↑3))) = 0
26		sq0 14231	. . . . . . . . . . 11 ⊢ (0↑2) = 0
27	25, 26	oveq12i 7443	. . . . . . . . . 10 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = (0 + 0)
28		00id 11436	. . . . . . . . . 10 ⊢ (0 + 0) = 0
29	27, 28	eqtri 2765	. . . . . . . . 9 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = 0
30	29	oveq1i 7441	. . . . . . . 8 ⊢ ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30)) = (0 − (1 / ;30))
31		0cn 11253	. . . . . . . . 9 ⊢ 0 ∈ ℂ
32		bpoly4 16095	. . . . . . . . 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 11495	. . . . . . . 8 ⊢ -(1 / ;30) = (0 − (1 / ;30))
35	30, 33, 34	3eqtr4i 2775	. . . . . . 7 ⊢ (4 BernPoly 0) = -(1 / ;30)
36	35	a1i 11	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → (4 BernPoly 0) = -(1 / ;30))
37	13, 36	oveq12d 7449	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)))
38		4nn0 12545	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
39		expcl 14120	. . . . . . . . . . . 12 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 4 ∈ ℕ₀) → ((𝑇 + 1)↑4) ∈ ℂ)
40	38, 39	mpan2 691	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑4) ∈ ℂ)
41		2cn 12341	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
42		expcl 14120	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑇 + 1)↑3) ∈ ℂ)
43	1, 42	mpan2 691	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑3) ∈ ℂ)
44		mulcl 11239	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑3) ∈ ℂ) → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
45	41, 43, 44	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
46	40, 45	subcld 11620	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) ∈ ℂ)
47		sqcl 14158	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
48	46, 47	addcld 11280	. . . . . . . . 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 12541	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
52	1, 51	deccl 12748	. . . . . . . . 9 ⊢ ;30 ∈ ℕ₀
53	52	nn0cni 12538	. . . . . . . 8 ⊢ ;30 ∈ ℂ
54	52	nn0rei 12537	. . . . . . . . 9 ⊢ ;30 ∈ ℝ
55		10pos 12750	. . . . . . . . . 10 ⊢ 0 < ;10
56	17, 51, 51, 55	declti 12771	. . . . . . . . 9 ⊢ 0 < ;30
57	54, 56	gt0ne0ii 11799	. . . . . . . 8 ⊢ ;30 ≠ 0
58	53, 57	reccli 11997	. . . . . . 7 ⊢ (1 / ;30) ∈ ℂ
59		subcl 11507	. . . . . . 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 11558	. . . . . 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 11517	. . . . . . . 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 12401	. . . . . . . . . . 11 ⊢ (2 + 2) = 4
67	66	eqcomi 2746	. . . . . . . . . 10 ⊢ 4 = (2 + 2)
68	67	oveq2i 7442	. . . . . . . . 9 ⊢ ((𝑇 + 1)↑4) = ((𝑇 + 1)↑(2 + 2))
69		df-3 12330	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
70	69	oveq2i 7442	. . . . . . . . . 10 ⊢ ((𝑇 + 1)↑3) = ((𝑇 + 1)↑(2 + 1))
71	70	oveq2i 7442	. . . . . . . . 9 ⊢ (2 · ((𝑇 + 1)↑3)) = (2 · ((𝑇 + 1)↑(2 + 1)))
72	68, 71	oveq12i 7443	. . . . . . . 8 ⊢ (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) = (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1))))
73	72	oveq1i 7441	. . . . . . 7 ⊢ ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2))
74		2nn0 12543	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
75		expadd 14145	. . . . . . . . . . . . 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 12542	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
78		expadd 14145	. . . . . . . . . . . . . 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 7447	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑(2 + 1))) = (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))))
81	76, 80	oveq12d 7449	. . . . . . . . . . 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 14184	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
84	83	mulridd 11278	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · 1) = ((𝑇 + 1)↑2))
85	84	eqcomd 2743	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇 + 1)↑2) · 1))
86	82, 85	oveq12d 7449	. . . . . . . . 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 14181	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) = (𝑇 + 1))
88	87	oveq2d 7447	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · ((𝑇 + 1)↑1)) = (2 · (𝑇 + 1)))
89	88	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · (𝑇 + 1))))
90	89	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
91	87, 10	eqeltrd 2841	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) ∈ ℂ)
92		mul12 11426	. . . . . . . . . . . . . . 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 7447	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))))
95		mulcl 11239	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (𝑇 + 1) ∈ ℂ) → (2 · (𝑇 + 1)) ∈ ℂ)
96	41, 10, 95	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) ∈ ℂ)
97	83, 83, 96	subdid 11719	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · (𝑇 + 1)))))
98	90, 94, 97	3eqtr4d 2787	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = (((𝑇 + 1)↑2) · (((𝑇 + 1)↑2) − (2 · (𝑇 + 1)))))
99	98	oveq1d 7446	. . . . . . . . . . 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 11620	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) ∈ ℂ)
101		ax-1cn 11213	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
102		adddi 11244	. . . . . . . . . . . . 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 2780	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)))
106		adddi 11244	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
107	41, 101, 106	mp3an13 1454	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
108		2t1e2 12429	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) = 2
109	108	oveq2i 7442	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) + (2 · 1)) = ((2 · 𝑇) + 2)
110	107, 109	eqtrdi 2793	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + 2))
111	110	oveq1d 7446	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = (((2 · 𝑇) + 2) − 1))
112		mulcl 11239	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (2 · 𝑇) ∈ ℂ)
113	41, 112	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · 𝑇) ∈ ℂ)
114		addsubass 11518	. . . . . . . . . . . . . . . . 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 12392	. . . . . . . . . . . . . . . 16 ⊢ (2 − 1) = 1
118	117	oveq2i 7442	. . . . . . . . . . . . . . 15 ⊢ ((2 · 𝑇) + (2 − 1)) = ((2 · 𝑇) + 1)
119	116, 118	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((2 · 𝑇) + 2) − 1) = ((2 · 𝑇) + 1))
120	111, 119	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = ((2 · 𝑇) + 1))
121	120	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)))
122		subsub 11539	. . . . . . . . . . . . . 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 14158	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (𝑇↑2) ∈ ℂ)
126		peano2cn 11433	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑇) ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
127	113, 126	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
128		binom21 14258	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇↑2) + (2 · 𝑇)) + 1))
129		addass 11242	. . . . . . . . . . . . . . . 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 2777	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
133	125, 127, 132	mvrraddd 11675	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)) = (𝑇↑2))
134	121, 124, 133	3eqtr3d 2785	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1) = (𝑇↑2))
135	134	oveq2d 7447	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = (((𝑇 + 1)↑2) · (𝑇↑2)))
136	83, 125	mulcomd 11282	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (𝑇↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
137	105, 135, 136	3eqtrd 2781	. . . . . . . . 9 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
138	86, 137	eqtrd 2777	. . . . . . . 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 2789	. . . . . 6 ⊢ (𝑇 ∈ ℕ₀ → ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
141	65, 140	eqtrd 2777	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) + (1 / ;30)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
142	37, 62, 141	3eqtrd 2781	. . . 4 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((𝑇↑2) · ((𝑇 + 1)↑2)))
143	142	oveq1d 7446	. . 3 ⊢ (𝑇 ∈ ℕ₀ → (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
144	8, 143	eqtr3id 2791	. 2 ⊢ (𝑇 ∈ ℕ₀ → ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1)) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))
145	3, 144	eqtrd 2777	1 ⊢ (𝑇 ∈ ℕ₀ → Σ𝑘 ∈ (0...𝑇)(𝑘↑3) = (((𝑇↑2) · ((𝑇 + 1)↑2)) / 4))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 − cmin 11492 -cneg 11493 / cdiv 11920 ℕcn 12266 2c2 12321 3c3 12322 4c4 12323 ℕ₀cn0 12526 cdc 12733 ...cfz 13547 ↑cexp 14102 Σcsu 15722 BernPoly cbp 16082

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-rp 13035 df-fz 13548 df-fzo 13695 df-seq 14043 df-exp 14103 df-fac 14313 df-bc 14342 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-clim 15524 df-sum 15723 df-bpoly 16083

This theorem is referenced by: (None)

W3C validator