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 30027

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 10834	. . 3
2		fsumkthpow 30023	. . 3 $/\$ BernPoly BernPoly
3	1, 2	mpan 670	. 2 BernPoly BernPoly
4		df-4 10617	. . . . . 6
5	4	oveq1i 6306	. . . . 5 BernPoly BernPoly
6	4	oveq1i 6306	. . . . 5 BernPoly BernPoly
7	5, 6	oveq12i 6308	. . . 4 BernPoly BernPoly BernPoly BernPoly
8	7, 4	oveq12i 6308	. . 3 BernPoly BernPoly BernPoly BernPoly
9		nn0cn 10826	. . . . . . . 8
10		peano2cn 9769	. . . . . . . 8
11	9, 10	syl 16	. . . . . . 7
12		bpoly4 30026	. . . . . . 7 BernPoly ;
13	11, 12	syl 16	. . . . . 6 BernPoly ;
14		4nn 10716	. . . . . . . . . . . . . 14
15		0exp 12204	. . . . . . . . . . . . . 14
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13
17		3nn 10715	. . . . . . . . . . . . . . . 16
18		0exp 12204	. . . . . . . . . . . . . . . 16
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15
20	19	oveq2i 6307	. . . . . . . . . . . . . 14
21		2t0e0 10712	. . . . . . . . . . . . . 14
22	20, 21	eqtri 2486	. . . . . . . . . . . . 13
23	16, 22	oveq12i 6308	. . . . . . . . . . . 12
24		0m0e0 10666	. . . . . . . . . . . 12
25	23, 24	eqtri 2486	. . . . . . . . . . 11
26		sq0 12262	. . . . . . . . . . 11
27	25, 26	oveq12i 6308	. . . . . . . . . 10
28		00id 9772	. . . . . . . . . 10
29	27, 28	eqtri 2486	. . . . . . . . 9
30	29	oveq1i 6306	. . . . . . . 8 ; ;
31		0cn 9605	. . . . . . . . 9
32		bpoly4 30026	. . . . . . . . 9 BernPoly ;
33	31, 32	ax-mp 5	. . . . . . . 8 BernPoly ;
34		df-neg 9827	. . . . . . . 8 ; ;
35	30, 33, 34	3eqtr4i 2496	. . . . . . 7 BernPoly ;
36	35	a1i 11	. . . . . 6 BernPoly ;
37	13, 36	oveq12d 6314	. . . . 5 BernPoly BernPoly ; ;
38		4nn0 10835	. . . . . . . . . . . 12
39		expcl 12187	. . . . . . . . . . . 12 $/\$
40	38, 39	mpan2 671	. . . . . . . . . . 11
41		2cn 10627	. . . . . . . . . . . 12
42		expcl 12187	. . . . . . . . . . . . 13 $/\$
43	1, 42	mpan2 671	. . . . . . . . . . . 12
44		mulcl 9593	. . . . . . . . . . . 12 $/\$
45	41, 43, 44	sylancr 663	. . . . . . . . . . 11
46	40, 45	subcld 9950	. . . . . . . . . 10
47		sqcl 12233	. . . . . . . . . 10
48	46, 47	addcld 9632	. . . . . . . . 9
49	10, 48	syl 16	. . . . . . . 8
50	9, 49	syl 16	. . . . . . 7
51		0nn0 10831	. . . . . . . . . 10
52	1, 51	deccl 11014	. . . . . . . . 9 ;
53	52	nn0cni 10828	. . . . . . . 8 ;
54	52	nn0rei 10827	. . . . . . . . 9 ;
55		10pos 10659	. . . . . . . . . 10
56	17, 51, 51, 55	declti 11025	. . . . . . . . 9 ;
57	54, 56	gt0ne0ii 10110	. . . . . . . 8 ;
58	53, 57	reccli 10295	. . . . . . 7 ;
59		subcl 9838	. . . . . . 7 $/\$ ; ;
60	50, 58, 59	sylancl 662	. . . . . 6 ;
61		subneg 9887	. . . . . 6 ; $/\$ ; ; ; ; ;
62	60, 58, 61	sylancl 662	. . . . 5 ; ; ; ;
63		npcan 9848	. . . . . . . 8 $/\$ ; ; ;
64	49, 58, 63	sylancl 662	. . . . . . 7 ; ;
65	9, 64	syl 16	. . . . . 6 ; ;
66		2p2e4 10674	. . . . . . . . . . 11
67	66	eqcomi 2470	. . . . . . . . . 10
68	67	oveq2i 6307	. . . . . . . . 9
69		df-3 10616	. . . . . . . . . . 11
70	69	oveq2i 6307	. . . . . . . . . 10
71	70	oveq2i 6307	. . . . . . . . 9
72	68, 71	oveq12i 6308	. . . . . . . 8
73	72	oveq1i 6306	. . . . . . 7
74		2nn0 10833	. . . . . . . . . . . . 13
75		expadd 12211	. . . . . . . . . . . . 13 $/\$ $/\$
76	74, 74, 75	mp3an23 1316	. . . . . . . . . . . 12
77		1nn0 10832	. . . . . . . . . . . . . 14
78		expadd 12211	. . . . . . . . . . . . . 14 $/\$ $/\$
79	74, 77, 78	mp3an23 1316	. . . . . . . . . . . . 13
80	79	oveq2d 6312	. . . . . . . . . . . 12
81	76, 80	oveq12d 6314	. . . . . . . . . . 11
82	10, 81	syl 16	. . . . . . . . . 10
83	10	sqcld 12311	. . . . . . . . . . . 12
84	83	mulid1d 9630	. . . . . . . . . . 11
85	84	eqcomd 2465	. . . . . . . . . 10
86	82, 85	oveq12d 6314	. . . . . . . . 9
87	10	exp1d 12308	. . . . . . . . . . . . . . . 16
88	87	oveq2d 6312	. . . . . . . . . . . . . . 15
89	88	oveq2d 6312	. . . . . . . . . . . . . 14
90	89	oveq2d 6312	. . . . . . . . . . . . 13
91	87, 10	eqeltrd 2545	. . . . . . . . . . . . . . 15
92		mul12 9763	. . . . . . . . . . . . . . . 16 $/\$ $/\$
93	41, 92	mp3an1 1311	. . . . . . . . . . . . . . 15 $/\$
94	83, 91, 93	syl2anc 661	. . . . . . . . . . . . . 14
95	94	oveq2d 6312	. . . . . . . . . . . . 13
96		mulcl 9593	. . . . . . . . . . . . . . 15 $/\$
97	41, 10, 96	sylancr 663	. . . . . . . . . . . . . 14
98	83, 83, 97	subdid 10033	. . . . . . . . . . . . 13
99	90, 95, 98	3eqtr4d 2508	. . . . . . . . . . . 12
100	99	oveq1d 6311	. . . . . . . . . . 11
101	83, 97	subcld 9950	. . . . . . . . . . . 12
102		ax-1cn 9567	. . . . . . . . . . . . 13
103		adddi 9598	. . . . . . . . . . . . 13 $/\$ $/\$
104	102, 103	mp3an3 1313	. . . . . . . . . . . 12 $/\$
105	83, 101, 104	syl2anc 661	. . . . . . . . . . 11
106	100, 105	eqtr4d 2501	. . . . . . . . . 10
107		adddi 9598	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	41, 102, 107	mp3an13 1315	. . . . . . . . . . . . . . . 16
109		2t1e2 10705	. . . . . . . . . . . . . . . . 17
110	109	oveq2i 6307	. . . . . . . . . . . . . . . 16
111	108, 110	syl6eq 2514	. . . . . . . . . . . . . . 15
112	111	oveq1d 6311	. . . . . . . . . . . . . 14
113		mulcl 9593	. . . . . . . . . . . . . . . . 17 $/\$
114	41, 113	mpan 670	. . . . . . . . . . . . . . . 16
115		addsubass 9849	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	41, 102, 115	mp3an23 1316	. . . . . . . . . . . . . . . 16
117	114, 116	syl 16	. . . . . . . . . . . . . . 15
118		2m1e1 10671	. . . . . . . . . . . . . . . 16
119	118	oveq2i 6307	. . . . . . . . . . . . . . 15
120	117, 119	syl6eq 2514	. . . . . . . . . . . . . 14
121	112, 120	eqtrd 2498	. . . . . . . . . . . . 13
122	121	oveq2d 6312	. . . . . . . . . . . 12
123		subsub 9868	. . . . . . . . . . . . . 14 $/\$ $/\$
124	102, 123	mp3an3 1313	. . . . . . . . . . . . 13 $/\$
125	83, 97, 124	syl2anc 661	. . . . . . . . . . . 12
126		binom21 12287	. . . . . . . . . . . . . . 15
127		sqcl 12233	. . . . . . . . . . . . . . . 16
128		addass 9596	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	102, 128	mp3an3 1313	. . . . . . . . . . . . . . . 16 $/\$
130	127, 114, 129	syl2anc 661	. . . . . . . . . . . . . . 15
131	126, 130	eqtrd 2498	. . . . . . . . . . . . . 14
132	131	oveq1d 6311	. . . . . . . . . . . . 13
133		peano2cn 9769	. . . . . . . . . . . . . . 15
134	114, 133	syl 16	. . . . . . . . . . . . . 14
135	127, 134	pncand 9951	. . . . . . . . . . . . 13
136	132, 135	eqtrd 2498	. . . . . . . . . . . 12
137	122, 125, 136	3eqtr3d 2506	. . . . . . . . . . 11
138	137	oveq2d 6312	. . . . . . . . . 10
139	83, 127	mulcomd 9634	. . . . . . . . . 10
140	106, 138, 139	3eqtrd 2502	. . . . . . . . 9
141	86, 140	eqtrd 2498	. . . . . . . 8
142	9, 141	syl 16	. . . . . . 7
143	73, 142	syl5eq 2510	. . . . . 6
144	65, 143	eqtrd 2498	. . . . 5 ; ;
145	37, 62, 144	3eqtrd 2502	. . . 4 BernPoly BernPoly
146	145	oveq1d 6311	. . 3 BernPoly BernPoly
147	8, 146	syl5eqr 2512	. 2 BernPoly BernPoly
148	3, 147	eqtrd 2498	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1395

wcel 1819 (class class class)co 6296

cc 9507

cc0 9509

c1 9510

caddc 9512

cmul 9514

cmin 9824

cneg 9825

cdiv 10227

cn 10556

c2 10606

c3 10607

c4 10608

cn0 10816 ;cdc 11000

cfz 11697

cexp 12169

csu 13520 BernPoly cbp 30013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-oadd 7152 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-sup 7919 df-oi 7953 df-card 8337 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-7 10620 df-8 10621 df-9 10622 df-10 10623 df-n0 10817 df-z 10886 df-dec 11001 df-uz 11107 df-rp 11246 df-fz 11698 df-fzo 11822 df-seq 12111 df-exp 12170 df-fac 12357 df-bc 12384 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-sum 13521 df-pred 29461 df-wrecs 29553 df-bpoly 30014

This theorem is referenced by: (None)

W3C validator