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 29387

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 10804	. . 3
2		fsumkthpow 29383	. . 3 $/\$ BernPoly BernPoly
3	1, 2	mpan 670	. 2 BernPoly BernPoly
4		df-4 10587	. . . . . 6
5	4	oveq1i 6287	. . . . 5 BernPoly BernPoly
6	4	oveq1i 6287	. . . . 5 BernPoly BernPoly
7	5, 6	oveq12i 6289	. . . 4 BernPoly BernPoly BernPoly BernPoly
8	7, 4	oveq12i 6289	. . 3 BernPoly BernPoly BernPoly BernPoly
9		nn0cn 10796	. . . . . . . 8
10		peano2cn 9742	. . . . . . . 8
11	9, 10	syl 16	. . . . . . 7
12		bpoly4 29386	. . . . . . 7 BernPoly ;
13	11, 12	syl 16	. . . . . 6 BernPoly ;
14		4nn 10686	. . . . . . . . . . . . . 14
15		0exp 12158	. . . . . . . . . . . . . 14
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13
17		3nn 10685	. . . . . . . . . . . . . . . 16
18		0exp 12158	. . . . . . . . . . . . . . . 16
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15
20	19	oveq2i 6288	. . . . . . . . . . . . . 14
21		2t0e0 10682	. . . . . . . . . . . . . 14
22	20, 21	eqtri 2491	. . . . . . . . . . . . 13
23	16, 22	oveq12i 6289	. . . . . . . . . . . 12
24		0m0e0 10636	. . . . . . . . . . . 12
25	23, 24	eqtri 2491	. . . . . . . . . . 11
26		sq0 12216	. . . . . . . . . . 11
27	25, 26	oveq12i 6289	. . . . . . . . . 10
28		00id 9745	. . . . . . . . . 10
29	27, 28	eqtri 2491	. . . . . . . . 9
30	29	oveq1i 6287	. . . . . . . 8 ; ;
31		0cn 9579	. . . . . . . . 9
32		bpoly4 29386	. . . . . . . . 9 BernPoly ;
33	31, 32	ax-mp 5	. . . . . . . 8 BernPoly ;
34		df-neg 9799	. . . . . . . 8 ; ;
35	30, 33, 34	3eqtr4i 2501	. . . . . . 7 BernPoly ;
36	35	a1i 11	. . . . . 6 BernPoly ;
37	13, 36	oveq12d 6295	. . . . 5 BernPoly BernPoly ; ;
38		4nn0 10805	. . . . . . . . . . . 12
39		expcl 12142	. . . . . . . . . . . 12 $/\$
40	38, 39	mpan2 671	. . . . . . . . . . 11
41		2cn 10597	. . . . . . . . . . . 12
42		expcl 12142	. . . . . . . . . . . . 13 $/\$
43	1, 42	mpan2 671	. . . . . . . . . . . 12
44		mulcl 9567	. . . . . . . . . . . 12 $/\$
45	41, 43, 44	sylancr 663	. . . . . . . . . . 11
46	40, 45	subcld 9921	. . . . . . . . . 10
47		sqcl 12187	. . . . . . . . . 10
48	46, 47	addcld 9606	. . . . . . . . 9
49	10, 48	syl 16	. . . . . . . 8
50	9, 49	syl 16	. . . . . . 7
51		0nn0 10801	. . . . . . . . . 10
52	1, 51	deccl 10981	. . . . . . . . 9 ;
53	52	nn0cni 10798	. . . . . . . 8 ;
54	52	nn0rei 10797	. . . . . . . . 9 ;
55		10pos 10629	. . . . . . . . . 10
56	17, 51, 51, 55	declti 10992	. . . . . . . . 9 ;
57	54, 56	gt0ne0ii 10080	. . . . . . . 8 ;
58	53, 57	reccli 10265	. . . . . . 7 ;
59		subcl 9810	. . . . . . 7 $/\$ ; ;
60	50, 58, 59	sylancl 662	. . . . . 6 ;
61		subneg 9859	. . . . . 6 ; $/\$ ; ; ; ; ;
62	60, 58, 61	sylancl 662	. . . . 5 ; ; ; ;
63		npcan 9820	. . . . . . . 8 $/\$ ; ; ;
64	49, 58, 63	sylancl 662	. . . . . . 7 ; ;
65	9, 64	syl 16	. . . . . 6 ; ;
66		2p2e4 10644	. . . . . . . . . . 11
67	66	eqcomi 2475	. . . . . . . . . 10
68	67	oveq2i 6288	. . . . . . . . 9
69		df-3 10586	. . . . . . . . . . 11
70	69	oveq2i 6288	. . . . . . . . . 10
71	70	oveq2i 6288	. . . . . . . . 9
72	68, 71	oveq12i 6289	. . . . . . . 8
73	72	oveq1i 6287	. . . . . . 7
74		2nn0 10803	. . . . . . . . . . . . 13
75		expadd 12165	. . . . . . . . . . . . 13 $/\$ $/\$
76	74, 74, 75	mp3an23 1311	. . . . . . . . . . . 12
77		1nn0 10802	. . . . . . . . . . . . . 14
78		expadd 12165	. . . . . . . . . . . . . 14 $/\$ $/\$
79	74, 77, 78	mp3an23 1311	. . . . . . . . . . . . 13
80	79	oveq2d 6293	. . . . . . . . . . . 12
81	76, 80	oveq12d 6295	. . . . . . . . . . 11
82	10, 81	syl 16	. . . . . . . . . 10
83	10	sqcld 12265	. . . . . . . . . . . 12
84	83	mulid1d 9604	. . . . . . . . . . 11
85	84	eqcomd 2470	. . . . . . . . . 10
86	82, 85	oveq12d 6295	. . . . . . . . 9
87	10	exp1d 12262	. . . . . . . . . . . . . . . 16
88	87	oveq2d 6293	. . . . . . . . . . . . . . 15
89	88	oveq2d 6293	. . . . . . . . . . . . . 14
90	89	oveq2d 6293	. . . . . . . . . . . . 13
91	87, 10	eqeltrd 2550	. . . . . . . . . . . . . . 15
92		mul12 9736	. . . . . . . . . . . . . . . 16 $/\$ $/\$
93	41, 92	mp3an1 1306	. . . . . . . . . . . . . . 15 $/\$
94	83, 91, 93	syl2anc 661	. . . . . . . . . . . . . 14
95	94	oveq2d 6293	. . . . . . . . . . . . 13
96		mulcl 9567	. . . . . . . . . . . . . . 15 $/\$
97	41, 10, 96	sylancr 663	. . . . . . . . . . . . . 14
98	83, 83, 97	subdid 10003	. . . . . . . . . . . . 13
99	90, 95, 98	3eqtr4d 2513	. . . . . . . . . . . 12
100	99	oveq1d 6292	. . . . . . . . . . 11
101	83, 97	subcld 9921	. . . . . . . . . . . 12
102		ax-1cn 9541	. . . . . . . . . . . . 13
103		adddi 9572	. . . . . . . . . . . . 13 $/\$ $/\$
104	102, 103	mp3an3 1308	. . . . . . . . . . . 12 $/\$
105	83, 101, 104	syl2anc 661	. . . . . . . . . . 11
106	100, 105	eqtr4d 2506	. . . . . . . . . 10
107		adddi 9572	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	41, 102, 107	mp3an13 1310	. . . . . . . . . . . . . . . 16
109	41	mulid1i 9589	. . . . . . . . . . . . . . . . 17
110	109	oveq2i 6288	. . . . . . . . . . . . . . . 16
111	108, 110	syl6eq 2519	. . . . . . . . . . . . . . 15
112	111	oveq1d 6292	. . . . . . . . . . . . . 14
113		mulcl 9567	. . . . . . . . . . . . . . . . 17 $/\$
114	41, 113	mpan 670	. . . . . . . . . . . . . . . 16
115		addsubass 9821	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	41, 102, 115	mp3an23 1311	. . . . . . . . . . . . . . . 16
117	114, 116	syl 16	. . . . . . . . . . . . . . 15
118		2m1e1 10641	. . . . . . . . . . . . . . . 16
119	118	oveq2i 6288	. . . . . . . . . . . . . . 15
120	117, 119	syl6eq 2519	. . . . . . . . . . . . . 14
121	112, 120	eqtrd 2503	. . . . . . . . . . . . 13
122	121	oveq2d 6293	. . . . . . . . . . . 12
123		subsub 9840	. . . . . . . . . . . . . 14 $/\$ $/\$
124	102, 123	mp3an3 1308	. . . . . . . . . . . . 13 $/\$
125	83, 97, 124	syl2anc 661	. . . . . . . . . . . 12
126		binom21 12241	. . . . . . . . . . . . . . 15
127		sqcl 12187	. . . . . . . . . . . . . . . 16
128		addass 9570	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	102, 128	mp3an3 1308	. . . . . . . . . . . . . . . 16 $/\$
130	127, 114, 129	syl2anc 661	. . . . . . . . . . . . . . 15
131	126, 130	eqtrd 2503	. . . . . . . . . . . . . 14
132	131	oveq1d 6292	. . . . . . . . . . . . 13
133		peano2cn 9742	. . . . . . . . . . . . . . 15
134	114, 133	syl 16	. . . . . . . . . . . . . 14
135	127, 134	pncand 9922	. . . . . . . . . . . . 13
136	132, 135	eqtrd 2503	. . . . . . . . . . . 12
137	122, 125, 136	3eqtr3d 2511	. . . . . . . . . . 11
138	137	oveq2d 6293	. . . . . . . . . 10
139	83, 127	mulcomd 9608	. . . . . . . . . 10
140	106, 138, 139	3eqtrd 2507	. . . . . . . . 9
141	86, 140	eqtrd 2503	. . . . . . . 8
142	9, 141	syl 16	. . . . . . 7
143	73, 142	syl5eq 2515	. . . . . 6
144	65, 143	eqtrd 2503	. . . . 5 ; ;
145	37, 62, 144	3eqtrd 2507	. . . 4 BernPoly BernPoly
146	145	oveq1d 6292	. . 3 BernPoly BernPoly
147	8, 146	syl5eqr 2517	. 2 BernPoly BernPoly
148	3, 147	eqtrd 2503	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1374

wcel 1762 (class class class)co 6277

cc 9481

cc0 9483

c1 9484

caddc 9486

cmul 9488

cmin 9796

cneg 9797

cdiv 10197

cn 10527

c2 10576

c3 10577

c4 10578

cn0 10786 ;cdc 10967

cfz 11663

cexp 12124

csu 13459 BernPoly cbp 29373

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440 ax-rep 4553 ax-sep 4563 ax-nul 4571 ax-pow 4620 ax-pr 4681 ax-un 6569 ax-inf2 8049 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560 ax-pre-sup 9561

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-fal 1380 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2274 df-mo 2275 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-ne 2659 df-nel 2660 df-ral 2814 df-rex 2815 df-reu 2816 df-rmo 2817 df-rab 2818 df-v 3110 df-sbc 3327 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3781 df-if 3935 df-pw 4007 df-sn 4023 df-pr 4025 df-tp 4027 df-op 4029 df-uni 4241 df-int 4278 df-iun 4322 df-br 4443 df-opab 4501 df-mpt 4502 df-tr 4536 df-eprel 4786 df-id 4790 df-po 4795 df-so 4796 df-fr 4833 df-se 4834 df-we 4835 df-ord 4876 df-on 4877 df-lim 4878 df-suc 4879 df-xp 5000 df-rel 5001 df-cnv 5002 df-co 5003 df-dm 5004 df-rn 5005 df-res 5006 df-ima 5007 df-iota 5544 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6674 df-1st 6776 df-2nd 6777 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-en 7509 df-dom 7510 df-sdom 7511 df-fin 7512 df-sup 7892 df-oi 7926 df-card 8311 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9798 df-neg 9799 df-div 10198 df-nn 10528 df-2 10585 df-3 10586 df-4 10587 df-5 10588 df-6 10589 df-7 10590 df-8 10591 df-9 10592 df-10 10593 df-n0 10787 df-z 10856 df-dec 10968 df-uz 11074 df-rp 11212 df-fz 11664 df-fzo 11784 df-seq 12066 df-exp 12125 df-fac 12311 df-bc 12338 df-hash 12363 df-cj 12884 df-re 12885 df-im 12886 df-sqr 13020 df-abs 13021 df-clim 13262 df-sum 13460 df-pred 28809 df-wrecs 28901 df-bpoly 29374

This theorem is referenced by: (None)

W3C validator