fsumcube - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fsumcube		Structured version Unicode version

Theorem fsumcube 28225

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

**Assertion**
Ref	Expression
fsumcube

Distinct variable group:

**Proof of Theorem fsumcube**
Step	Hyp	Ref	Expression
1		3nn0 10618	. . 3
2		fsumkthpow 28221	. . 3 $/\$ BernPoly BernPoly
3	1, 2	mpan 670	. 2 BernPoly BernPoly
4		df-4 10403	. . . . . 6
5	4	oveq1i 6122	. . . . 5 BernPoly BernPoly
6	4	oveq1i 6122	. . . . 5 BernPoly BernPoly
7	5, 6	oveq12i 6124	. . . 4 BernPoly BernPoly BernPoly BernPoly
8	7, 4	oveq12i 6124	. . 3 BernPoly BernPoly BernPoly BernPoly
9		nn0cn 10610	. . . . . . . 8
10		peano2cn 9562	. . . . . . . 8
11	9, 10	syl 16	. . . . . . 7
12		bpoly4 28224	. . . . . . 7 BernPoly ;
13	11, 12	syl 16	. . . . . 6 BernPoly ;
14		4nn 10502	. . . . . . . . . . . . . 14
15		0exp 11920	. . . . . . . . . . . . . 14
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13
17		3nn 10501	. . . . . . . . . . . . . . . 16
18		0exp 11920	. . . . . . . . . . . . . . . 16
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15
20	19	oveq2i 6123	. . . . . . . . . . . . . 14
21		2t0e0 10498	. . . . . . . . . . . . . 14
22	20, 21	eqtri 2463	. . . . . . . . . . . . 13
23	16, 22	oveq12i 6124	. . . . . . . . . . . 12
24		0m0e0 10452	. . . . . . . . . . . 12
25	23, 24	eqtri 2463	. . . . . . . . . . 11
26		sq0 11978	. . . . . . . . . . 11
27	25, 26	oveq12i 6124	. . . . . . . . . 10
28		00id 9565	. . . . . . . . . 10
29	27, 28	eqtri 2463	. . . . . . . . 9
30	29	oveq1i 6122	. . . . . . . 8 ; ;
31		0cn 9399	. . . . . . . . 9
32		bpoly4 28224	. . . . . . . . 9 BernPoly ;
33	31, 32	ax-mp 5	. . . . . . . 8 BernPoly ;
34		df-neg 9619	. . . . . . . 8 ; ;
35	30, 33, 34	3eqtr4i 2473	. . . . . . 7 BernPoly ;
36	35	a1i 11	. . . . . 6 BernPoly ;
37	13, 36	oveq12d 6130	. . . . 5 BernPoly BernPoly ; ;
38		4nn0 10619	. . . . . . . . . . . 12
39		expcl 11904	. . . . . . . . . . . 12 $/\$
40	38, 39	mpan2 671	. . . . . . . . . . 11
41		2cn 10413	. . . . . . . . . . . 12
42		expcl 11904	. . . . . . . . . . . . 13 $/\$
43	1, 42	mpan2 671	. . . . . . . . . . . 12
44		mulcl 9387	. . . . . . . . . . . 12 $/\$
45	41, 43, 44	sylancr 663	. . . . . . . . . . 11
46	40, 45	subcld 9740	. . . . . . . . . 10
47		sqcl 11949	. . . . . . . . . 10
48	46, 47	addcld 9426	. . . . . . . . 9
49	10, 48	syl 16	. . . . . . . 8
50	9, 49	syl 16	. . . . . . 7
51		0nn0 10615	. . . . . . . . . 10
52	1, 51	deccl 10790	. . . . . . . . 9 ;
53	52	nn0cni 10612	. . . . . . . 8 ;
54	52	nn0rei 10611	. . . . . . . . 9 ;
55		10pos 10445	. . . . . . . . . 10
56	17, 51, 51, 55	declti 10801	. . . . . . . . 9 ;
57	54, 56	gt0ne0ii 9897	. . . . . . . 8 ;
58	53, 57	reccli 10082	. . . . . . 7 ;
59		subcl 9630	. . . . . . 7 $/\$ ; ;
60	50, 58, 59	sylancl 662	. . . . . 6 ;
61		subneg 9679	. . . . . 6 ; $/\$ ; ; ; ; ;
62	60, 58, 61	sylancl 662	. . . . 5 ; ; ; ;
63		npcan 9640	. . . . . . . 8 $/\$ ; ; ;
64	49, 58, 63	sylancl 662	. . . . . . 7 ; ;
65	9, 64	syl 16	. . . . . 6 ; ;
66		2p2e4 10460	. . . . . . . . . . 11
67	66	eqcomi 2447	. . . . . . . . . 10
68	67	oveq2i 6123	. . . . . . . . 9
69		df-3 10402	. . . . . . . . . . 11
70	69	oveq2i 6123	. . . . . . . . . 10
71	70	oveq2i 6123	. . . . . . . . 9
72	68, 71	oveq12i 6124	. . . . . . . 8
73	72	oveq1i 6122	. . . . . . 7
74		2nn0 10617	. . . . . . . . . . . . 13
75		expadd 11927	. . . . . . . . . . . . 13 $/\$ $/\$
76	74, 74, 75	mp3an23 1306	. . . . . . . . . . . 12
77		1nn0 10616	. . . . . . . . . . . . . 14
78		expadd 11927	. . . . . . . . . . . . . 14 $/\$ $/\$
79	74, 77, 78	mp3an23 1306	. . . . . . . . . . . . 13
80	79	oveq2d 6128	. . . . . . . . . . . 12
81	76, 80	oveq12d 6130	. . . . . . . . . . 11
82	10, 81	syl 16	. . . . . . . . . 10
83	10	sqcld 12027	. . . . . . . . . . . 12
84	83	mulid1d 9424	. . . . . . . . . . 11
85	84	eqcomd 2448	. . . . . . . . . 10
86	82, 85	oveq12d 6130	. . . . . . . . 9
87	10	exp1d 12024	. . . . . . . . . . . . . . . 16
88	87	oveq2d 6128	. . . . . . . . . . . . . . 15
89	88	oveq2d 6128	. . . . . . . . . . . . . 14
90	89	oveq2d 6128	. . . . . . . . . . . . 13
91	87, 10	eqeltrd 2517	. . . . . . . . . . . . . . 15
92		mul12 9556	. . . . . . . . . . . . . . . 16 $/\$ $/\$
93	41, 92	mp3an1 1301	. . . . . . . . . . . . . . 15 $/\$
94	83, 91, 93	syl2anc 661	. . . . . . . . . . . . . 14
95	94	oveq2d 6128	. . . . . . . . . . . . 13
96		mulcl 9387	. . . . . . . . . . . . . . 15 $/\$
97	41, 10, 96	sylancr 663	. . . . . . . . . . . . . 14
98	83, 83, 97	subdid 9821	. . . . . . . . . . . . 13
99	90, 95, 98	3eqtr4d 2485	. . . . . . . . . . . 12
100	99	oveq1d 6127	. . . . . . . . . . 11
101	83, 97	subcld 9740	. . . . . . . . . . . 12
102		ax-1cn 9361	. . . . . . . . . . . . 13
103		adddi 9392	. . . . . . . . . . . . 13 $/\$ $/\$
104	102, 103	mp3an3 1303	. . . . . . . . . . . 12 $/\$
105	83, 101, 104	syl2anc 661	. . . . . . . . . . 11
106	100, 105	eqtr4d 2478	. . . . . . . . . 10
107		adddi 9392	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	41, 102, 107	mp3an13 1305	. . . . . . . . . . . . . . . 16
109	41	mulid1i 9409	. . . . . . . . . . . . . . . . 17
110	109	oveq2i 6123	. . . . . . . . . . . . . . . 16
111	108, 110	syl6eq 2491	. . . . . . . . . . . . . . 15
112	111	oveq1d 6127	. . . . . . . . . . . . . 14
113		mulcl 9387	. . . . . . . . . . . . . . . . 17 $/\$
114	41, 113	mpan 670	. . . . . . . . . . . . . . . 16
115		addsubass 9641	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	41, 102, 115	mp3an23 1306	. . . . . . . . . . . . . . . 16
117	114, 116	syl 16	. . . . . . . . . . . . . . 15
118		2m1e1 10457	. . . . . . . . . . . . . . . 16
119	118	oveq2i 6123	. . . . . . . . . . . . . . 15
120	117, 119	syl6eq 2491	. . . . . . . . . . . . . 14
121	112, 120	eqtrd 2475	. . . . . . . . . . . . 13
122	121	oveq2d 6128	. . . . . . . . . . . 12
123		subsub 9660	. . . . . . . . . . . . . 14 $/\$ $/\$
124	102, 123	mp3an3 1303	. . . . . . . . . . . . 13 $/\$
125	83, 97, 124	syl2anc 661	. . . . . . . . . . . 12
126		binom21 12003	. . . . . . . . . . . . . . 15
127		sqcl 11949	. . . . . . . . . . . . . . . 16
128		addass 9390	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	102, 128	mp3an3 1303	. . . . . . . . . . . . . . . 16 $/\$
130	127, 114, 129	syl2anc 661	. . . . . . . . . . . . . . 15
131	126, 130	eqtrd 2475	. . . . . . . . . . . . . 14
132	131	oveq1d 6127	. . . . . . . . . . . . 13
133		peano2cn 9562	. . . . . . . . . . . . . . 15
134	114, 133	syl 16	. . . . . . . . . . . . . 14
135	127, 134	pncand 9741	. . . . . . . . . . . . 13
136	132, 135	eqtrd 2475	. . . . . . . . . . . 12
137	122, 125, 136	3eqtr3d 2483	. . . . . . . . . . 11
138	137	oveq2d 6128	. . . . . . . . . 10
139	83, 127	mulcomd 9428	. . . . . . . . . 10
140	106, 138, 139	3eqtrd 2479	. . . . . . . . 9
141	86, 140	eqtrd 2475	. . . . . . . 8
142	9, 141	syl 16	. . . . . . 7
143	73, 142	syl5eq 2487	. . . . . 6
144	65, 143	eqtrd 2475	. . . . 5 ; ;
145	37, 62, 144	3eqtrd 2479	. . . 4 BernPoly BernPoly
146	145	oveq1d 6127	. . 3 BernPoly BernPoly
147	8, 146	syl5eqr 2489	. 2 BernPoly BernPoly
148	3, 147	eqtrd 2475	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1369

wcel 1756 (class class class)co 6112

cc 9301

cc0 9303

c1 9304

caddc 9306

cmul 9308

cmin 9616

cneg 9617

cdiv 10014

cn 10343

c2 10392

c3 10393

c4 10394

cn0 10600 ;cdc 10776

cfz 11458

cexp 11886

csu 13184 BernPoly cbp 28211

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4424 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-inf2 7868 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380 ax-pre-sup 9381

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-int 4150 df-iun 4194 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-se 4701 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-isom 5448 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-1o 6941 df-oadd 6945 df-er 7122 df-en 7332 df-dom 7333 df-sdom 7334 df-fin 7335 df-sup 7712 df-oi 7745 df-card 8130 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-div 10015 df-nn 10344 df-2 10401 df-3 10402 df-4 10403 df-5 10404 df-6 10405 df-7 10406 df-8 10407 df-9 10408 df-10 10409 df-n0 10601 df-z 10668 df-dec 10777 df-uz 10883 df-rp 11013 df-fz 11459 df-fzo 11570 df-seq 11828 df-exp 11887 df-fac 12073 df-bc 12100 df-hash 12125 df-cj 12609 df-re 12610 df-im 12611 df-sqr 12745 df-abs 12746 df-clim 12987 df-sum 13185 df-pred 27647 df-wrecs 27739 df-bpoly 28212

This theorem is referenced by: (None)

W3C validator