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 15983

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 12419	. . 3 ⊢ 3 ∈ ℕ₀
2		fsumkthpow 15979	. . 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 12210	. . . . . 6 ⊢ 4 = (3 + 1)
5	4	oveq1i 7368	. . . . 5 ⊢ (4 BernPoly (𝑇 + 1)) = ((3 + 1) BernPoly (𝑇 + 1))
6	4	oveq1i 7368	. . . . 5 ⊢ (4 BernPoly 0) = ((3 + 1) BernPoly 0)
7	5, 6	oveq12i 7370	. . . 4 ⊢ ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = (((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0))
8	7, 4	oveq12i 7370	. . 3 ⊢ (((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) / 4) = ((((3 + 1) BernPoly (𝑇 + 1)) − ((3 + 1) BernPoly 0)) / (3 + 1))
9		nn0cn 12411	. . . . . . . 8 ⊢ (𝑇 ∈ ℕ₀ → 𝑇 ∈ ℂ)
10		peano2cn 11305	. . . . . . . 8 ⊢ (𝑇 ∈ ℂ → (𝑇 + 1) ∈ ℂ)
11	9, 10	syl 17	. . . . . . 7 ⊢ (𝑇 ∈ ℕ₀ → (𝑇 + 1) ∈ ℂ)
12		bpoly4 15982	. . . . . . 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 12228	. . . . . . . . . . . . . 14 ⊢ 4 ∈ ℕ
15		0exp 14020	. . . . . . . . . . . . . 14 ⊢ (4 ∈ ℕ → (0↑4) = 0)
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (0↑4) = 0
17		3nn 12224	. . . . . . . . . . . . . . . 16 ⊢ 3 ∈ ℕ
18		0exp 14020	. . . . . . . . . . . . . . . 16 ⊢ (3 ∈ ℕ → (0↑3) = 0)
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (0↑3) = 0
20	19	oveq2i 7369	. . . . . . . . . . . . . 14 ⊢ (2 · (0↑3)) = (2 · 0)
21		2t0e0 12309	. . . . . . . . . . . . . 14 ⊢ (2 · 0) = 0
22	20, 21	eqtri 2759	. . . . . . . . . . . . 13 ⊢ (2 · (0↑3)) = 0
23	16, 22	oveq12i 7370	. . . . . . . . . . . 12 ⊢ ((0↑4) − (2 · (0↑3))) = (0 − 0)
24		0m0e0 12260	. . . . . . . . . . . 12 ⊢ (0 − 0) = 0
25	23, 24	eqtri 2759	. . . . . . . . . . 11 ⊢ ((0↑4) − (2 · (0↑3))) = 0
26		sq0 14115	. . . . . . . . . . 11 ⊢ (0↑2) = 0
27	25, 26	oveq12i 7370	. . . . . . . . . 10 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = (0 + 0)
28		00id 11308	. . . . . . . . . 10 ⊢ (0 + 0) = 0
29	27, 28	eqtri 2759	. . . . . . . . 9 ⊢ (((0↑4) − (2 · (0↑3))) + (0↑2)) = 0
30	29	oveq1i 7368	. . . . . . . 8 ⊢ ((((0↑4) − (2 · (0↑3))) + (0↑2)) − (1 / ;30)) = (0 − (1 / ;30))
31		0cn 11124	. . . . . . . . 9 ⊢ 0 ∈ ℂ
32		bpoly4 15982	. . . . . . . . 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 11367	. . . . . . . 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 7376	. . . . 5 ⊢ (𝑇 ∈ ℕ₀ → ((4 BernPoly (𝑇 + 1)) − (4 BernPoly 0)) = ((((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) − (1 / ;30)) − -(1 / ;30)))
38		4nn0 12420	. . . . . . . . . . . 12 ⊢ 4 ∈ ℕ₀
39		expcl 14002	. . . . . . . . . . . 12 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 4 ∈ ℕ₀) → ((𝑇 + 1)↑4) ∈ ℂ)
40	38, 39	mpan2 691	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑4) ∈ ℂ)
41		2cn 12220	. . . . . . . . . . . 12 ⊢ 2 ∈ ℂ
42		expcl 14002	. . . . . . . . . . . . 13 ⊢ (((𝑇 + 1) ∈ ℂ ∧ 3 ∈ ℕ₀) → ((𝑇 + 1)↑3) ∈ ℂ)
43	1, 42	mpan2 691	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑3) ∈ ℂ)
44		mulcl 11110	. . . . . . . . . . . 12 ⊢ ((2 ∈ ℂ ∧ ((𝑇 + 1)↑3) ∈ ℂ) → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
45	41, 43, 44	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑3)) ∈ ℂ)
46	40, 45	subcld 11492	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) ∈ ℂ)
47		sqcl 14041	. . . . . . . . . 10 ⊢ ((𝑇 + 1) ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
48	46, 47	addcld 11151	. . . . . . . . 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 12416	. . . . . . . . . 10 ⊢ 0 ∈ ℕ₀
52	1, 51	deccl 12622	. . . . . . . . 9 ⊢ ;30 ∈ ℕ₀
53	52	nn0cni 12413	. . . . . . . 8 ⊢ ;30 ∈ ℂ
54	52	nn0rei 12412	. . . . . . . . 9 ⊢ ;30 ∈ ℝ
55		10pos 12624	. . . . . . . . . 10 ⊢ 0 < ;10
56	17, 51, 51, 55	declti 12645	. . . . . . . . 9 ⊢ 0 < ;30
57	54, 56	gt0ne0ii 11673	. . . . . . . 8 ⊢ ;30 ≠ 0
58	53, 57	reccli 11871	. . . . . . 7 ⊢ (1 / ;30) ∈ ℂ
59		subcl 11379	. . . . . . 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 11430	. . . . . 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 11389	. . . . . . . 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 12275	. . . . . . . . . . 11 ⊢ (2 + 2) = 4
67	66	eqcomi 2745	. . . . . . . . . 10 ⊢ 4 = (2 + 2)
68	67	oveq2i 7369	. . . . . . . . 9 ⊢ ((𝑇 + 1)↑4) = ((𝑇 + 1)↑(2 + 2))
69		df-3 12209	. . . . . . . . . . 11 ⊢ 3 = (2 + 1)
70	69	oveq2i 7369	. . . . . . . . . 10 ⊢ ((𝑇 + 1)↑3) = ((𝑇 + 1)↑(2 + 1))
71	70	oveq2i 7369	. . . . . . . . 9 ⊢ (2 · ((𝑇 + 1)↑3)) = (2 · ((𝑇 + 1)↑(2 + 1)))
72	68, 71	oveq12i 7370	. . . . . . . 8 ⊢ (((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) = (((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1))))
73	72	oveq1i 7368	. . . . . . 7 ⊢ ((((𝑇 + 1)↑4) − (2 · ((𝑇 + 1)↑3))) + ((𝑇 + 1)↑2)) = ((((𝑇 + 1)↑(2 + 2)) − (2 · ((𝑇 + 1)↑(2 + 1)))) + ((𝑇 + 1)↑2))
74		2nn0 12418	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℕ₀
75		expadd 14027	. . . . . . . . . . . . 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 12417	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℕ₀
78		expadd 14027	. . . . . . . . . . . . . 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 7374	. . . . . . . . . . . 12 ⊢ ((𝑇 + 1) ∈ ℂ → (2 · ((𝑇 + 1)↑(2 + 1))) = (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1))))
81	76, 80	oveq12d 7376	. . . . . . . . . . 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 14067	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) ∈ ℂ)
84	83	mulridd 11149	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · 1) = ((𝑇 + 1)↑2))
85	84	eqcomd 2742	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇 + 1)↑2) · 1))
86	82, 85	oveq12d 7376	. . . . . . . . 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 14064	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑1) = (𝑇 + 1))
88	87	oveq2d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · ((𝑇 + 1)↑1)) = (2 · (𝑇 + 1)))
89	88	oveq2d 7374	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1))) = (((𝑇 + 1)↑2) · (2 · (𝑇 + 1))))
90	89	oveq2d 7374	. . . . . . . . . . . . 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 11298	. . . . . . . . . . . . . . 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 7374	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) = ((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (((𝑇 + 1)↑2) · (2 · ((𝑇 + 1)↑1)))))
95		mulcl 11110	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ (𝑇 + 1) ∈ ℂ) → (2 · (𝑇 + 1)) ∈ ℂ)
96	41, 10, 95	sylancr 587	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) ∈ ℂ)
97	83, 83, 96	subdid 11593	. . . . . . . . . . . . 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 7373	. . . . . . . . . . 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 11492	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) ∈ ℂ)
101		ax-1cn 11084	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
102		adddi 11115	. . . . . . . . . . . . 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 2774	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((((𝑇 + 1)↑2) · ((𝑇 + 1)↑2)) − (2 · (((𝑇 + 1)↑2) · ((𝑇 + 1)↑1)))) + (((𝑇 + 1)↑2) · 1)) = (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)))
106		adddi 11115	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
107	41, 101, 106	mp3an13 1454	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + (2 · 1)))
108		2t1e2 12303	. . . . . . . . . . . . . . . . 17 ⊢ (2 · 1) = 2
109	108	oveq2i 7369	. . . . . . . . . . . . . . . 16 ⊢ ((2 · 𝑇) + (2 · 1)) = ((2 · 𝑇) + 2)
110	107, 109	eqtrdi 2787	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∈ ℂ → (2 · (𝑇 + 1)) = ((2 · 𝑇) + 2))
111	110	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((2 · (𝑇 + 1)) − 1) = (((2 · 𝑇) + 2) − 1))
112		mulcl 11110	. . . . . . . . . . . . . . . . 17 ⊢ ((2 ∈ ℂ ∧ 𝑇 ∈ ℂ) → (2 · 𝑇) ∈ ℂ)
113	41, 112	mpan 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 ∈ ℂ → (2 · 𝑇) ∈ ℂ)
114		addsubass 11390	. . . . . . . . . . . . . . . . 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 12266	. . . . . . . . . . . . . . . 16 ⊢ (2 − 1) = 1
118	117	oveq2i 7369	. . . . . . . . . . . . . . 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 7374	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · (𝑇 + 1)) − 1)) = (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)))
122		subsub 11411	. . . . . . . . . . . . . 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 14041	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → (𝑇↑2) ∈ ℂ)
126		peano2cn 11305	. . . . . . . . . . . . . 14 ⊢ ((2 · 𝑇) ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
127	113, 126	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((2 · 𝑇) + 1) ∈ ℂ)
128		binom21 14142	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = (((𝑇↑2) + (2 · 𝑇)) + 1))
129		addass 11113	. . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ ℂ → ((𝑇 + 1)↑2) = ((𝑇↑2) + ((2 · 𝑇) + 1)))
133	125, 127, 132	mvrraddd 11549	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) − ((2 · 𝑇) + 1)) = (𝑇↑2))
134	121, 124, 133	3eqtr3d 2779	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℂ → ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1) = (𝑇↑2))
135	134	oveq2d 7374	. . . . . . . . . 10 ⊢ (𝑇 ∈ ℂ → (((𝑇 + 1)↑2) · ((((𝑇 + 1)↑2) − (2 · (𝑇 + 1))) + 1)) = (((𝑇 + 1)↑2) · (𝑇↑2)))
136	83, 125	mulcomd 11153	. . . . . . . . . 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 7373	. . 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 1541 ∈ wcel 2113 (class class class)co 7358 ℂcc 11024 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 − cmin 11364 -cneg 11365 / cdiv 11794 ℕcn 12145 2c2 12200 3c3 12201 4c4 12202 ℕ₀cn0 12401 cdc 12607 ...cfz 13423 ↑cexp 13984 Σcsu 15609 BernPoly cbp 15969

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 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 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-oi 9415 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-rp 12906 df-fz 13424 df-fzo 13571 df-seq 13925 df-exp 13985 df-fac 14197 df-bc 14226 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-clim 15411 df-sum 15610 df-bpoly 15970

This theorem is referenced by: (None)

W3C validator