fsumcube - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fsumcube		Structured version Visualization version Unicode version

Theorem fsumcube 14113

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 10887	. . 3
2		fsumkthpow 14109	. . 3 $/\$ BernPoly BernPoly
3	1, 2	mpan 676	. 2 BernPoly BernPoly
4		df-4 10670	. . . . . 6
5	4	oveq1i 6300	. . . . 5 BernPoly BernPoly
6	4	oveq1i 6300	. . . . 5 BernPoly BernPoly
7	5, 6	oveq12i 6302	. . . 4 BernPoly BernPoly BernPoly BernPoly
8	7, 4	oveq12i 6302	. . 3 BernPoly BernPoly BernPoly BernPoly
9		nn0cn 10879	. . . . . . . 8
10		peano2cn 9805	. . . . . . . 8
11	9, 10	syl 17	. . . . . . 7
12		bpoly4 14112	. . . . . . 7 BernPoly ;
13	11, 12	syl 17	. . . . . 6 BernPoly ;
14		4nn 10769	. . . . . . . . . . . . . 14
15		0exp 12307	. . . . . . . . . . . . . 14
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13
17		3nn 10768	. . . . . . . . . . . . . . . 16
18		0exp 12307	. . . . . . . . . . . . . . . 16
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15
20	19	oveq2i 6301	. . . . . . . . . . . . . 14
21		2t0e0 10765	. . . . . . . . . . . . . 14
22	20, 21	eqtri 2473	. . . . . . . . . . . . 13
23	16, 22	oveq12i 6302	. . . . . . . . . . . 12
24		0m0e0 10719	. . . . . . . . . . . 12
25	23, 24	eqtri 2473	. . . . . . . . . . 11
26		sq0 12366	. . . . . . . . . . 11
27	25, 26	oveq12i 6302	. . . . . . . . . 10
28		00id 9808	. . . . . . . . . 10
29	27, 28	eqtri 2473	. . . . . . . . 9
30	29	oveq1i 6300	. . . . . . . 8 ; ;
31		0cn 9635	. . . . . . . . 9
32		bpoly4 14112	. . . . . . . . 9 BernPoly ;
33	31, 32	ax-mp 5	. . . . . . . 8 BernPoly ;
34		df-neg 9863	. . . . . . . 8 ; ;
35	30, 33, 34	3eqtr4i 2483	. . . . . . 7 BernPoly ;
36	35	a1i 11	. . . . . 6 BernPoly ;
37	13, 36	oveq12d 6308	. . . . 5 BernPoly BernPoly ; ;
38		4nn0 10888	. . . . . . . . . . . 12
39		expcl 12290	. . . . . . . . . . . 12 $/\$
40	38, 39	mpan2 677	. . . . . . . . . . 11
41		2cn 10680	. . . . . . . . . . . 12
42		expcl 12290	. . . . . . . . . . . . 13 $/\$
43	1, 42	mpan2 677	. . . . . . . . . . . 12
44		mulcl 9623	. . . . . . . . . . . 12 $/\$
45	41, 43, 44	sylancr 669	. . . . . . . . . . 11
46	40, 45	subcld 9986	. . . . . . . . . 10
47		sqcl 12337	. . . . . . . . . 10
48	46, 47	addcld 9662	. . . . . . . . 9
49	10, 48	syl 17	. . . . . . . 8
50	9, 49	syl 17	. . . . . . 7
51		0nn0 10884	. . . . . . . . . 10
52	1, 51	deccl 11065	. . . . . . . . 9 ;
53	52	nn0cni 10881	. . . . . . . 8 ;
54	52	nn0rei 10880	. . . . . . . . 9 ;
55		10pos 10712	. . . . . . . . . 10
56	17, 51, 51, 55	declti 11076	. . . . . . . . 9 ;
57	54, 56	gt0ne0ii 10150	. . . . . . . 8 ;
58	53, 57	reccli 10337	. . . . . . 7 ;
59		subcl 9874	. . . . . . 7 $/\$ ; ;
60	50, 58, 59	sylancl 668	. . . . . 6 ;
61		subneg 9923	. . . . . 6 ; $/\$ ; ; ; ; ;
62	60, 58, 61	sylancl 668	. . . . 5 ; ; ; ;
63		npcan 9884	. . . . . . . 8 $/\$ ; ; ;
64	49, 58, 63	sylancl 668	. . . . . . 7 ; ;
65	9, 64	syl 17	. . . . . 6 ; ;
66		2p2e4 10727	. . . . . . . . . . 11
67	66	eqcomi 2460	. . . . . . . . . 10
68	67	oveq2i 6301	. . . . . . . . 9
69		df-3 10669	. . . . . . . . . . 11
70	69	oveq2i 6301	. . . . . . . . . 10
71	70	oveq2i 6301	. . . . . . . . 9
72	68, 71	oveq12i 6302	. . . . . . . 8
73	72	oveq1i 6300	. . . . . . 7
74		2nn0 10886	. . . . . . . . . . . . 13
75		expadd 12314	. . . . . . . . . . . . 13 $/\$ $/\$
76	74, 74, 75	mp3an23 1356	. . . . . . . . . . . 12
77		1nn0 10885	. . . . . . . . . . . . . 14
78		expadd 12314	. . . . . . . . . . . . . 14 $/\$ $/\$
79	74, 77, 78	mp3an23 1356	. . . . . . . . . . . . 13
80	79	oveq2d 6306	. . . . . . . . . . . 12
81	76, 80	oveq12d 6308	. . . . . . . . . . 11
82	10, 81	syl 17	. . . . . . . . . 10
83	10	sqcld 12414	. . . . . . . . . . . 12
84	83	mulid1d 9660	. . . . . . . . . . 11
85	84	eqcomd 2457	. . . . . . . . . 10
86	82, 85	oveq12d 6308	. . . . . . . . 9
87	10	exp1d 12411	. . . . . . . . . . . . . . . 16
88	87	oveq2d 6306	. . . . . . . . . . . . . . 15
89	88	oveq2d 6306	. . . . . . . . . . . . . 14
90	89	oveq2d 6306	. . . . . . . . . . . . 13
91	87, 10	eqeltrd 2529	. . . . . . . . . . . . . . 15
92		mul12 9799	. . . . . . . . . . . . . . . 16 $/\$ $/\$
93	41, 92	mp3an1 1351	. . . . . . . . . . . . . . 15 $/\$
94	83, 91, 93	syl2anc 667	. . . . . . . . . . . . . 14
95	94	oveq2d 6306	. . . . . . . . . . . . 13
96		mulcl 9623	. . . . . . . . . . . . . . 15 $/\$
97	41, 10, 96	sylancr 669	. . . . . . . . . . . . . 14
98	83, 83, 97	subdid 10074	. . . . . . . . . . . . 13
99	90, 95, 98	3eqtr4d 2495	. . . . . . . . . . . 12
100	99	oveq1d 6305	. . . . . . . . . . 11
101	83, 97	subcld 9986	. . . . . . . . . . . 12
102		ax-1cn 9597	. . . . . . . . . . . . 13
103		adddi 9628	. . . . . . . . . . . . 13 $/\$ $/\$
104	102, 103	mp3an3 1353	. . . . . . . . . . . 12 $/\$
105	83, 101, 104	syl2anc 667	. . . . . . . . . . 11
106	100, 105	eqtr4d 2488	. . . . . . . . . 10
107		adddi 9628	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	41, 102, 107	mp3an13 1355	. . . . . . . . . . . . . . . 16
109		2t1e2 10758	. . . . . . . . . . . . . . . . 17
110	109	oveq2i 6301	. . . . . . . . . . . . . . . 16
111	108, 110	syl6eq 2501	. . . . . . . . . . . . . . 15
112	111	oveq1d 6305	. . . . . . . . . . . . . 14
113		mulcl 9623	. . . . . . . . . . . . . . . . 17 $/\$
114	41, 113	mpan 676	. . . . . . . . . . . . . . . 16
115		addsubass 9885	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	41, 102, 115	mp3an23 1356	. . . . . . . . . . . . . . . 16
117	114, 116	syl 17	. . . . . . . . . . . . . . 15
118		2m1e1 10724	. . . . . . . . . . . . . . . 16
119	118	oveq2i 6301	. . . . . . . . . . . . . . 15
120	117, 119	syl6eq 2501	. . . . . . . . . . . . . 14
121	112, 120	eqtrd 2485	. . . . . . . . . . . . 13
122	121	oveq2d 6306	. . . . . . . . . . . 12
123		subsub 9904	. . . . . . . . . . . . . 14 $/\$ $/\$
124	102, 123	mp3an3 1353	. . . . . . . . . . . . 13 $/\$
125	83, 97, 124	syl2anc 667	. . . . . . . . . . . 12
126		binom21 12390	. . . . . . . . . . . . . . 15
127		sqcl 12337	. . . . . . . . . . . . . . . 16
128		addass 9626	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	102, 128	mp3an3 1353	. . . . . . . . . . . . . . . 16 $/\$
130	127, 114, 129	syl2anc 667	. . . . . . . . . . . . . . 15
131	126, 130	eqtrd 2485	. . . . . . . . . . . . . 14
132	131	oveq1d 6305	. . . . . . . . . . . . 13
133		peano2cn 9805	. . . . . . . . . . . . . . 15
134	114, 133	syl 17	. . . . . . . . . . . . . 14
135	127, 134	pncand 9987	. . . . . . . . . . . . 13
136	132, 135	eqtrd 2485	. . . . . . . . . . . 12
137	122, 125, 136	3eqtr3d 2493	. . . . . . . . . . 11
138	137	oveq2d 6306	. . . . . . . . . 10
139	83, 127	mulcomd 9664	. . . . . . . . . 10
140	106, 138, 139	3eqtrd 2489	. . . . . . . . 9
141	86, 140	eqtrd 2485	. . . . . . . 8
142	9, 141	syl 17	. . . . . . 7
143	73, 142	syl5eq 2497	. . . . . 6
144	65, 143	eqtrd 2485	. . . . 5 ; ;
145	37, 62, 144	3eqtrd 2489	. . . 4 BernPoly BernPoly
146	145	oveq1d 6305	. . 3 BernPoly BernPoly
147	8, 146	syl5eqr 2499	. 2 BernPoly BernPoly
148	3, 147	eqtrd 2485	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1444

wcel 1887 (class class class)co 6290

cc 9537

cc0 9539

c1 9540

caddc 9542

cmul 9544

cmin 9860

cneg 9861

cdiv 10269

cn 10609

c2 10659

c3 10660

c4 10661

cn0 10869 ;cdc 11051

cfz 11784

cexp 12272

csu 13752 BernPoly cbp 14099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-rep 4515 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-inf2 8146 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616 ax-pre-sup 9617

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-fal 1450 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rmo 2745 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-int 4235 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-se 4794 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-isom 5591 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-1st 6793 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-1o 7182 df-oadd 7186 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-fin 7573 df-sup 7956 df-oi 8025 df-card 8373 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-div 10270 df-nn 10610 df-2 10668 df-3 10669 df-4 10670 df-5 10671 df-6 10672 df-7 10673 df-8 10674 df-9 10675 df-10 10676 df-n0 10870 df-z 10938 df-dec 11052 df-uz 11160 df-rp 11303 df-fz 11785 df-fzo 11916 df-seq 12214 df-exp 12273 df-fac 12460 df-bc 12488 df-hash 12516 df-cj 13162 df-re 13163 df-im 13164 df-sqrt 13298 df-abs 13299 df-clim 13552 df-sum 13753 df-bpoly 14100

This theorem is referenced by: (None)

W3C validator