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 28049

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 10584	. . 3
2		fsumkthpow 28045	. . 3 $/\$ BernPoly BernPoly
3	1, 2	mpan 663	. 2 BernPoly BernPoly
4		df-4 10369	. . . . . 6
5	4	oveq1i 6090	. . . . 5 BernPoly BernPoly
6	4	oveq1i 6090	. . . . 5 BernPoly BernPoly
7	5, 6	oveq12i 6092	. . . 4 BernPoly BernPoly BernPoly BernPoly
8	7, 4	oveq12i 6092	. . 3 BernPoly BernPoly BernPoly BernPoly
9		nn0cn 10576	. . . . . . . 8
10		peano2cn 9528	. . . . . . . 8
11	9, 10	syl 16	. . . . . . 7
12		bpoly4 28048	. . . . . . 7 BernPoly ;
13	11, 12	syl 16	. . . . . 6 BernPoly ;
14		4nn 10468	. . . . . . . . . . . . . 14
15		0exp 11882	. . . . . . . . . . . . . 14
16	14, 15	ax-mp 5	. . . . . . . . . . . . 13
17		3nn 10467	. . . . . . . . . . . . . . . 16
18		0exp 11882	. . . . . . . . . . . . . . . 16
19	17, 18	ax-mp 5	. . . . . . . . . . . . . . 15
20	19	oveq2i 6091	. . . . . . . . . . . . . 14
21		2t0e0 10464	. . . . . . . . . . . . . 14
22	20, 21	eqtri 2453	. . . . . . . . . . . . 13
23	16, 22	oveq12i 6092	. . . . . . . . . . . 12
24		0m0e0 10418	. . . . . . . . . . . 12
25	23, 24	eqtri 2453	. . . . . . . . . . 11
26		sq0 11940	. . . . . . . . . . 11
27	25, 26	oveq12i 6092	. . . . . . . . . 10
28		00id 9531	. . . . . . . . . 10
29	27, 28	eqtri 2453	. . . . . . . . 9
30	29	oveq1i 6090	. . . . . . . 8 ; ;
31		0cn 9365	. . . . . . . . 9
32		bpoly4 28048	. . . . . . . . 9 BernPoly ;
33	31, 32	ax-mp 5	. . . . . . . 8 BernPoly ;
34		df-neg 9585	. . . . . . . 8 ; ;
35	30, 33, 34	3eqtr4i 2463	. . . . . . 7 BernPoly ;
36	35	a1i 11	. . . . . 6 BernPoly ;
37	13, 36	oveq12d 6098	. . . . 5 BernPoly BernPoly ; ;
38		4nn0 10585	. . . . . . . . . . . 12
39		expcl 11866	. . . . . . . . . . . 12 $/\$
40	38, 39	mpan2 664	. . . . . . . . . . 11
41		2cn 10379	. . . . . . . . . . . 12
42		expcl 11866	. . . . . . . . . . . . 13 $/\$
43	1, 42	mpan2 664	. . . . . . . . . . . 12
44		mulcl 9353	. . . . . . . . . . . 12 $/\$
45	41, 43, 44	sylancr 656	. . . . . . . . . . 11
46	40, 45	subcld 9706	. . . . . . . . . 10
47		sqcl 11911	. . . . . . . . . 10
48	46, 47	addcld 9392	. . . . . . . . 9
49	10, 48	syl 16	. . . . . . . 8
50	9, 49	syl 16	. . . . . . 7
51		0nn0 10581	. . . . . . . . . 10
52	1, 51	deccl 10756	. . . . . . . . 9 ;
53	52	nn0cni 10578	. . . . . . . 8 ;
54	52	nn0rei 10577	. . . . . . . . 9 ;
55		10pos 10411	. . . . . . . . . 10
56	17, 51, 51, 55	declti 10767	. . . . . . . . 9 ;
57	54, 56	gt0ne0ii 9863	. . . . . . . 8 ;
58	53, 57	reccli 10048	. . . . . . 7 ;
59		subcl 9596	. . . . . . 7 $/\$ ; ;
60	50, 58, 59	sylancl 655	. . . . . 6 ;
61		subneg 9645	. . . . . 6 ; $/\$ ; ; ; ; ;
62	60, 58, 61	sylancl 655	. . . . 5 ; ; ; ;
63		npcan 9606	. . . . . . . 8 $/\$ ; ; ;
64	49, 58, 63	sylancl 655	. . . . . . 7 ; ;
65	9, 64	syl 16	. . . . . 6 ; ;
66		2p2e4 10426	. . . . . . . . . . 11
67	66	eqcomi 2437	. . . . . . . . . 10
68	67	oveq2i 6091	. . . . . . . . 9
69		df-3 10368	. . . . . . . . . . 11
70	69	oveq2i 6091	. . . . . . . . . 10
71	70	oveq2i 6091	. . . . . . . . 9
72	68, 71	oveq12i 6092	. . . . . . . 8
73	72	oveq1i 6090	. . . . . . 7
74		2nn0 10583	. . . . . . . . . . . . 13
75		expadd 11889	. . . . . . . . . . . . 13 $/\$ $/\$
76	74, 74, 75	mp3an23 1299	. . . . . . . . . . . 12
77		1nn0 10582	. . . . . . . . . . . . . 14
78		expadd 11889	. . . . . . . . . . . . . 14 $/\$ $/\$
79	74, 77, 78	mp3an23 1299	. . . . . . . . . . . . 13
80	79	oveq2d 6096	. . . . . . . . . . . 12
81	76, 80	oveq12d 6098	. . . . . . . . . . 11
82	10, 81	syl 16	. . . . . . . . . 10
83	10	sqcld 11989	. . . . . . . . . . . 12
84	83	mulid1d 9390	. . . . . . . . . . 11
85	84	eqcomd 2438	. . . . . . . . . 10
86	82, 85	oveq12d 6098	. . . . . . . . 9
87	10	exp1d 11986	. . . . . . . . . . . . . . . 16
88	87	oveq2d 6096	. . . . . . . . . . . . . . 15
89	88	oveq2d 6096	. . . . . . . . . . . . . 14
90	89	oveq2d 6096	. . . . . . . . . . . . 13
91	87, 10	eqeltrd 2507	. . . . . . . . . . . . . . 15
92		mul12 9522	. . . . . . . . . . . . . . . 16 $/\$ $/\$
93	41, 92	mp3an1 1294	. . . . . . . . . . . . . . 15 $/\$
94	83, 91, 93	syl2anc 654	. . . . . . . . . . . . . 14
95	94	oveq2d 6096	. . . . . . . . . . . . 13
96		mulcl 9353	. . . . . . . . . . . . . . 15 $/\$
97	41, 10, 96	sylancr 656	. . . . . . . . . . . . . 14
98	83, 83, 97	subdid 9787	. . . . . . . . . . . . 13
99	90, 95, 98	3eqtr4d 2475	. . . . . . . . . . . 12
100	99	oveq1d 6095	. . . . . . . . . . 11
101	83, 97	subcld 9706	. . . . . . . . . . . 12
102		ax-1cn 9327	. . . . . . . . . . . . 13
103		adddi 9358	. . . . . . . . . . . . 13 $/\$ $/\$
104	102, 103	mp3an3 1296	. . . . . . . . . . . 12 $/\$
105	83, 101, 104	syl2anc 654	. . . . . . . . . . 11
106	100, 105	eqtr4d 2468	. . . . . . . . . 10
107		adddi 9358	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
108	41, 102, 107	mp3an13 1298	. . . . . . . . . . . . . . . 16
109	41	mulid1i 9375	. . . . . . . . . . . . . . . . 17
110	109	oveq2i 6091	. . . . . . . . . . . . . . . 16
111	108, 110	syl6eq 2481	. . . . . . . . . . . . . . 15
112	111	oveq1d 6095	. . . . . . . . . . . . . 14
113		mulcl 9353	. . . . . . . . . . . . . . . . 17 $/\$
114	41, 113	mpan 663	. . . . . . . . . . . . . . . 16
115		addsubass 9607	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
116	41, 102, 115	mp3an23 1299	. . . . . . . . . . . . . . . 16
117	114, 116	syl 16	. . . . . . . . . . . . . . 15
118		2m1e1 10423	. . . . . . . . . . . . . . . 16
119	118	oveq2i 6091	. . . . . . . . . . . . . . 15
120	117, 119	syl6eq 2481	. . . . . . . . . . . . . 14
121	112, 120	eqtrd 2465	. . . . . . . . . . . . 13
122	121	oveq2d 6096	. . . . . . . . . . . 12
123		subsub 9626	. . . . . . . . . . . . . 14 $/\$ $/\$
124	102, 123	mp3an3 1296	. . . . . . . . . . . . 13 $/\$
125	83, 97, 124	syl2anc 654	. . . . . . . . . . . 12
126		binom21 11965	. . . . . . . . . . . . . . 15
127		sqcl 11911	. . . . . . . . . . . . . . . 16
128		addass 9356	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
129	102, 128	mp3an3 1296	. . . . . . . . . . . . . . . 16 $/\$
130	127, 114, 129	syl2anc 654	. . . . . . . . . . . . . . 15
131	126, 130	eqtrd 2465	. . . . . . . . . . . . . 14
132	131	oveq1d 6095	. . . . . . . . . . . . 13
133		peano2cn 9528	. . . . . . . . . . . . . . 15
134	114, 133	syl 16	. . . . . . . . . . . . . 14
135	127, 134	pncand 9707	. . . . . . . . . . . . 13
136	132, 135	eqtrd 2465	. . . . . . . . . . . 12
137	122, 125, 136	3eqtr3d 2473	. . . . . . . . . . 11
138	137	oveq2d 6096	. . . . . . . . . 10
139	83, 127	mulcomd 9394	. . . . . . . . . 10
140	106, 138, 139	3eqtrd 2469	. . . . . . . . 9
141	86, 140	eqtrd 2465	. . . . . . . 8
142	9, 141	syl 16	. . . . . . 7
143	73, 142	syl5eq 2477	. . . . . 6
144	65, 143	eqtrd 2465	. . . . 5 ; ;
145	37, 62, 144	3eqtrd 2469	. . . 4 BernPoly BernPoly
146	145	oveq1d 6095	. . 3 BernPoly BernPoly
147	8, 146	syl5eqr 2479	. 2 BernPoly BernPoly
148	3, 147	eqtrd 2465	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wceq 1362

wcel 1755 (class class class)co 6080

cc 9267

cc0 9269

c1 9270

caddc 9272

cmul 9274

cmin 9582

cneg 9583

cdiv 9980

cn 10309

c2 10358

c3 10359

c4 10360

cn0 10566 ;cdc 10742

cfz 11423

cexp 11848

csu 13146 BernPoly cbp 28035

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1594 ax-4 1605 ax-5 1669 ax-6 1707 ax-7 1727 ax-8 1757 ax-9 1759 ax-10 1774 ax-11 1779 ax-12 1791 ax-13 1942 ax-ext 2414 ax-rep 4391 ax-sep 4401 ax-nul 4409 ax-pow 4458 ax-pr 4519 ax-un 6361 ax-inf2 7835 ax-cnex 9325 ax-resscn 9326 ax-1cn 9327 ax-icn 9328 ax-addcl 9329 ax-addrcl 9330 ax-mulcl 9331 ax-mulrcl 9332 ax-mulcom 9333 ax-addass 9334 ax-mulass 9335 ax-distr 9336 ax-i2m1 9337 ax-1ne0 9338 ax-1rid 9339 ax-rnegex 9340 ax-rrecex 9341 ax-cnre 9342 ax-pre-lttri 9343 ax-pre-lttrn 9344 ax-pre-ltadd 9345 ax-pre-mulgt0 9346 ax-pre-sup 9347

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 959 df-3an 960 df-tru 1365 df-fal 1368 df-ex 1590 df-nf 1593 df-sb 1700 df-eu 2258 df-mo 2259 df-clab 2420 df-cleq 2426 df-clel 2429 df-nfc 2558 df-ne 2598 df-nel 2599 df-ral 2710 df-rex 2711 df-reu 2712 df-rmo 2713 df-rab 2714 df-v 2964 df-sbc 3176 df-csb 3277 df-dif 3319 df-un 3321 df-in 3323 df-ss 3330 df-pss 3332 df-nul 3626 df-if 3780 df-pw 3850 df-sn 3866 df-pr 3868 df-tp 3870 df-op 3872 df-uni 4080 df-int 4117 df-iun 4161 df-br 4281 df-opab 4339 df-mpt 4340 df-tr 4374 df-eprel 4619 df-id 4623 df-po 4628 df-so 4629 df-fr 4666 df-se 4667 df-we 4668 df-ord 4709 df-on 4710 df-lim 4711 df-suc 4712 df-xp 4833 df-rel 4834 df-cnv 4835 df-co 4836 df-dm 4837 df-rn 4838 df-res 4839 df-ima 4840 df-iota 5369 df-fun 5408 df-fn 5409 df-f 5410 df-f1 5411 df-fo 5412 df-f1o 5413 df-fv 5414 df-isom 5415 df-riota 6039 df-ov 6083 df-oprab 6084 df-mpt2 6085 df-om 6466 df-1st 6566 df-2nd 6567 df-recs 6818 df-rdg 6852 df-1o 6908 df-oadd 6912 df-er 7089 df-en 7299 df-dom 7300 df-sdom 7301 df-fin 7302 df-sup 7679 df-oi 7712 df-card 8097 df-pnf 9407 df-mnf 9408 df-xr 9409 df-ltxr 9410 df-le 9411 df-sub 9584 df-neg 9585 df-div 9981 df-nn 10310 df-2 10367 df-3 10368 df-4 10369 df-5 10370 df-6 10371 df-7 10372 df-8 10373 df-9 10374 df-10 10375 df-n0 10567 df-z 10634 df-dec 10743 df-uz 10849 df-rp 10979 df-fz 11424 df-fzo 11532 df-seq 11790 df-exp 11849 df-fac 12035 df-bc 12062 df-hash 12087 df-cj 12571 df-re 12572 df-im 12573 df-sqr 12707 df-abs 12708 df-clim 12949 df-sum 13147 df-pred 27471 df-wrecs 27563 df-bpoly 28036

This theorem is referenced by: (None)

W3C validator