fsumcube - Mathbox for Scott Fenton

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

Theorem fsumcube 26010

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 10195	. . 3
2		fsumkthpow 26006	. . 3 $/\$ BernPoly BernPoly
3	1, 2	mpan 652	. 2 BernPoly BernPoly
4		df-4 10016	. . . . . 6
5	4	oveq1i 6050	. . . . 5 BernPoly BernPoly
6	4	oveq1i 6050	. . . . 5 BernPoly BernPoly
7	5, 6	oveq12i 6052	. . . 4 BernPoly BernPoly BernPoly BernPoly
8	7, 4	oveq12i 6052	. . 3 BernPoly BernPoly BernPoly BernPoly
9		nn0cn 10187	. . . . . . . 8
10		peano2cn 9194	. . . . . . . 8
11	9, 10	syl 16	. . . . . . 7
12		bpoly4 26009	. . . . . . 7 BernPoly ;
13	11, 12	syl 16	. . . . . 6 BernPoly ;
14		4nn 10091	. . . . . . . . . . . . . 14
15		0exp 11370	. . . . . . . . . . . . . 14
16	14, 15	ax-mp 8	. . . . . . . . . . . . 13
17		3nn 10090	. . . . . . . . . . . . . . . 16
18		0exp 11370	. . . . . . . . . . . . . . . 16
19	17, 18	ax-mp 8	. . . . . . . . . . . . . . 15
20	19	oveq2i 6051	. . . . . . . . . . . . . 14
21		2cn 10026	. . . . . . . . . . . . . . 15
22	21	mul01i 9212	. . . . . . . . . . . . . 14
23	20, 22	eqtri 2424	. . . . . . . . . . . . 13
24	16, 23	oveq12i 6052	. . . . . . . . . . . 12
25		0cn 9040	. . . . . . . . . . . . 13
26	25	subid1i 9328	. . . . . . . . . . . 12
27	24, 26	eqtri 2424	. . . . . . . . . . 11
28		sq0 11428	. . . . . . . . . . 11
29	27, 28	oveq12i 6052	. . . . . . . . . 10
30		00id 9197	. . . . . . . . . 10
31	29, 30	eqtri 2424	. . . . . . . . 9
32	31	oveq1i 6050	. . . . . . . 8 ; ;
33		bpoly4 26009	. . . . . . . . 9 BernPoly ;
34	25, 33	ax-mp 8	. . . . . . . 8 BernPoly ;
35		df-neg 9250	. . . . . . . 8 ; ;
36	32, 34, 35	3eqtr4i 2434	. . . . . . 7 BernPoly ;
37	36	a1i 11	. . . . . 6 BernPoly ;
38	13, 37	oveq12d 6058	. . . . 5 BernPoly BernPoly ; ;
39		4nn0 10196	. . . . . . . . . . . 12
40		expcl 11354	. . . . . . . . . . . 12 $/\$
41	39, 40	mpan2 653	. . . . . . . . . . 11
42		expcl 11354	. . . . . . . . . . . . 13 $/\$
43	1, 42	mpan2 653	. . . . . . . . . . . 12
44		mulcl 9030	. . . . . . . . . . . 12 $/\$
45	21, 43, 44	sylancr 645	. . . . . . . . . . 11
46	41, 45	subcld 9367	. . . . . . . . . 10
47		sqcl 11399	. . . . . . . . . 10
48	46, 47	addcld 9063	. . . . . . . . 9
49	10, 48	syl 16	. . . . . . . 8
50	9, 49	syl 16	. . . . . . 7
51		0nn0 10192	. . . . . . . . . 10
52	1, 51	deccl 10352	. . . . . . . . 9 ;
53	52	nn0cni 10189	. . . . . . . 8 ;
54	52	nn0rei 10188	. . . . . . . . 9 ;
55		10pos 10048	. . . . . . . . . 10
56	17, 51, 51, 55	declti 10363	. . . . . . . . 9 ;
57	54, 56	gt0ne0ii 9519	. . . . . . . 8 ;
58	53, 57	reccli 9700	. . . . . . 7 ;
59		subcl 9261	. . . . . . 7 $/\$ ; ;
60	50, 58, 59	sylancl 644	. . . . . 6 ;
61		subneg 9306	. . . . . 6 ; $/\$ ; ; ; ; ;
62	60, 58, 61	sylancl 644	. . . . 5 ; ; ; ;
63		npcan 9270	. . . . . . . 8 $/\$ ; ; ;
64	49, 58, 63	sylancl 644	. . . . . . 7 ; ;
65	9, 64	syl 16	. . . . . 6 ; ;
66		2p2e4 10054	. . . . . . . . . . 11
67	66	eqcomi 2408	. . . . . . . . . 10
68	67	oveq2i 6051	. . . . . . . . 9
69		df-3 10015	. . . . . . . . . . 11
70	69	oveq2i 6051	. . . . . . . . . 10
71	70	oveq2i 6051	. . . . . . . . 9
72	68, 71	oveq12i 6052	. . . . . . . 8
73	72	oveq1i 6050	. . . . . . 7
74		2nn0 10194	. . . . . . . . . . . . 13
75		expadd 11377	. . . . . . . . . . . . 13 $/\$ $/\$
76	74, 74, 75	mp3an23 1271	. . . . . . . . . . . 12
77		1nn0 10193	. . . . . . . . . . . . . 14
78		expadd 11377	. . . . . . . . . . . . . 14 $/\$ $/\$
79	74, 77, 78	mp3an23 1271	. . . . . . . . . . . . 13
80	79	oveq2d 6056	. . . . . . . . . . . 12
81	76, 80	oveq12d 6058	. . . . . . . . . . 11
82	10, 81	syl 16	. . . . . . . . . 10
83	10	sqcld 11476	. . . . . . . . . . . 12
84	83	mulid1d 9061	. . . . . . . . . . 11
85	84	eqcomd 2409	. . . . . . . . . 10
86	82, 85	oveq12d 6058	. . . . . . . . 9
87	10	exp1d 11473	. . . . . . . . . . . . . . . 16
88	87	oveq2d 6056	. . . . . . . . . . . . . . 15
89	88	oveq2d 6056	. . . . . . . . . . . . . 14
90	89	oveq2d 6056	. . . . . . . . . . . . 13
91	87, 10	eqeltrd 2478	. . . . . . . . . . . . . . 15
92		mul12 9188	. . . . . . . . . . . . . . . 16 $/\$ $/\$
93	21, 92	mp3an1 1266	. . . . . . . . . . . . . . 15 $/\$
94	83, 91, 93	syl2anc 643	. . . . . . . . . . . . . 14
95	94	oveq2d 6056	. . . . . . . . . . . . 13
96		mulcl 9030	. . . . . . . . . . . . . . 15 $/\$
97	21, 10, 96	sylancr 645	. . . . . . . . . . . . . 14
98	83, 83, 97	subdid 9445	. . . . . . . . . . . . 13
99	90, 95, 98	3eqtr4d 2446	. . . . . . . . . . . 12
100	99	oveq1d 6055	. . . . . . . . . . 11
101	83, 97	subcld 9367	. . . . . . . . . . . 12
102		ax-1cn 9004	. . . . . . . . . . . . 13
103		adddi 9035	. . . . . . . . . . . . 13 $/\$ $/\$
104	102, 103	mp3an3 1268	. . . . . . . . . . . 12 $/\$
105	83, 101, 104	syl2anc 643	. . . . . . . . . . 11
106	100, 105	eqtr4d 2439	. . . . . . . . . 10
107		adddi 9035	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	21, 102, 107	mp3an13 1270	. . . . . . . . . . . . . . . 16
109	21	mulid1i 9048	. . . . . . . . . . . . . . . . 17
110	109	oveq2i 6051	. . . . . . . . . . . . . . . 16
111	108, 110	syl6eq 2452	. . . . . . . . . . . . . . 15
112	111	oveq1d 6055	. . . . . . . . . . . . . 14
113		mulcl 9030	. . . . . . . . . . . . . . . . 17 $/\$
114	21, 113	mpan 652	. . . . . . . . . . . . . . . 16
115		addsubass 9271	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	21, 102, 115	mp3an23 1271	. . . . . . . . . . . . . . . 16
117	114, 116	syl 16	. . . . . . . . . . . . . . 15
118		2m1e1 10051	. . . . . . . . . . . . . . . 16
119	118	oveq2i 6051	. . . . . . . . . . . . . . 15
120	117, 119	syl6eq 2452	. . . . . . . . . . . . . 14
121	112, 120	eqtrd 2436	. . . . . . . . . . . . 13
122	121	oveq2d 6056	. . . . . . . . . . . 12
123		subsub 9287	. . . . . . . . . . . . . 14 $/\$ $/\$
124	102, 123	mp3an3 1268	. . . . . . . . . . . . 13 $/\$
125	83, 97, 124	syl2anc 643	. . . . . . . . . . . 12
126		binom21 11452	. . . . . . . . . . . . . . 15
127		sqcl 11399	. . . . . . . . . . . . . . . 16
128		addass 9033	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	102, 128	mp3an3 1268	. . . . . . . . . . . . . . . 16 $/\$
130	127, 114, 129	syl2anc 643	. . . . . . . . . . . . . . 15
131	126, 130	eqtrd 2436	. . . . . . . . . . . . . 14
132	131	oveq1d 6055	. . . . . . . . . . . . 13
133		peano2cn 9194	. . . . . . . . . . . . . . 15
134	114, 133	syl 16	. . . . . . . . . . . . . 14
135	127, 134	pncand 9368	. . . . . . . . . . . . 13
136	132, 135	eqtrd 2436	. . . . . . . . . . . 12
137	122, 125, 136	3eqtr3d 2444	. . . . . . . . . . 11
138	137	oveq2d 6056	. . . . . . . . . 10
139	83, 127	mulcomd 9065	. . . . . . . . . 10
140	106, 138, 139	3eqtrd 2440	. . . . . . . . 9
141	86, 140	eqtrd 2436	. . . . . . . 8
142	9, 141	syl 16	. . . . . . 7
143	73, 142	syl5eq 2448	. . . . . 6
144	65, 143	eqtrd 2436	. . . . 5 ; ;
145	38, 62, 144	3eqtrd 2440	. . . 4 BernPoly BernPoly
146	145	oveq1d 6055	. . 3 BernPoly BernPoly
147	8, 146	syl5eqr 2450	. 2 BernPoly BernPoly
148	3, 147	eqtrd 2436	1

Colors of variables: wff set class

Syntax hints:

wi 4

wceq 1649

wcel 1721 (class class class)co 6040

cc 8944

cc0 8946

c1 8947

caddc 8949

cmul 8951

cmin 9247

cneg 9248

cdiv 9633

cn 9956

c2 10005

c3 10006

c4 10007

cn0 10177 ;cdc 10338

cfz 10999

cexp 11337

csu 12434 BernPoly cbp 25996

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-inf2 7552 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023 ax-pre-sup 9024

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-se 4502 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-isom 5422 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-sup 7404 df-oi 7435 df-card 7782 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-2 10014 df-3 10015 df-4 10016 df-5 10017 df-6 10018 df-7 10019 df-8 10020 df-9 10021 df-10 10022 df-n0 10178 df-z 10239 df-dec 10339 df-uz 10445 df-rp 10569 df-fz 11000 df-fzo 11091 df-seq 11279 df-exp 11338 df-fac 11522 df-bc 11549 df-hash 11574 df-cj 11859 df-re 11860 df-im 11861 df-sqr 11995 df-abs 11996 df-clim 12237 df-sum 12435 df-pred 25382 df-bpoly 25997

W3C validator