binom4 - Metamath Proof Explorer

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

Theorem binom4 23855

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 13965, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)

**Assertion**
Ref	Expression
binom4	$/\$

**Proof of Theorem binom4**
Step	Hyp	Ref	Expression
1		df-4 10692	. . . 4
2	1	oveq2i 6319	. . 3
3		addcl 9639	. . . 4 $/\$
4		3nn0 10911	. . . 4
5		expp1 12317	. . . 4 $/\$
6	3, 4, 5	sylancl 675	. . 3 $/\$
7	2, 6	syl5eq 2517	. 2 $/\$
8		binom3 12431	. . 3 $/\$
9	8	oveq1d 6323	. 2 $/\$
10		simpl 464	. . . . . . 7 $/\$
11		expcl 12328	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 675	. . . . . 6 $/\$
13		3cn 10706	. . . . . . 7
14	10	sqcld 12452	. . . . . . . 8 $/\$
15		simpr 468	. . . . . . . 8 $/\$
16	14, 15	mulcld 9681	. . . . . . 7 $/\$
17		mulcl 9641	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 676	. . . . . 6 $/\$
19	12, 18	addcld 9680	. . . . 5 $/\$
20	15	sqcld 12452	. . . . . . . 8 $/\$
21	10, 20	mulcld 9681	. . . . . . 7 $/\$
22		mulcl 9641	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 676	. . . . . 6 $/\$
24		expcl 12328	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 675	. . . . . 6 $/\$
26	23, 25	addcld 9680	. . . . 5 $/\$
27	19, 26	addcld 9680	. . . 4 $/\$
28	27, 10, 15	adddid 9685	. . 3 $/\$
29	19, 26, 10	adddird 9686	. . . . 5 $/\$
30	12, 18, 10	adddird 9686	. . . . . . 7 $/\$
31	1	oveq2i 6319	. . . . . . . . 9
32		expp1 12317	. . . . . . . . . 10 $/\$
33	10, 4, 32	sylancl 675	. . . . . . . . 9 $/\$
34	31, 33	syl5req 2518	. . . . . . . 8 $/\$
35	13	a1i 11	. . . . . . . . . 10 $/\$
36	35, 16, 10	mulassd 9684	. . . . . . . . 9 $/\$
37	14, 15, 10	mul32d 9861	. . . . . . . . . . 11 $/\$
38		df-3 10691	. . . . . . . . . . . . . 14
39	38	oveq2i 6319	. . . . . . . . . . . . 13
40		2nn0 10910	. . . . . . . . . . . . . 14
41		expp1 12317	. . . . . . . . . . . . . 14 $/\$
42	10, 40, 41	sylancl 675	. . . . . . . . . . . . 13 $/\$
43	39, 42	syl5req 2518	. . . . . . . . . . . 12 $/\$
44	43	oveq1d 6323	. . . . . . . . . . 11 $/\$
45	37, 44	eqtrd 2505	. . . . . . . . . 10 $/\$
46	45	oveq2d 6324	. . . . . . . . 9 $/\$
47	36, 46	eqtrd 2505	. . . . . . . 8 $/\$
48	34, 47	oveq12d 6326	. . . . . . 7 $/\$
49	30, 48	eqtrd 2505	. . . . . 6 $/\$
50	23, 25, 10	adddird 9686	. . . . . . 7 $/\$
51	35, 21, 10	mulassd 9684	. . . . . . . . 9 $/\$
52	10, 20, 10	mul32d 9861	. . . . . . . . . . 11 $/\$
53	10	sqvald 12451	. . . . . . . . . . . 12 $/\$
54	53	oveq1d 6323	. . . . . . . . . . 11 $/\$
55	52, 54	eqtr4d 2508	. . . . . . . . . 10 $/\$
56	55	oveq2d 6324	. . . . . . . . 9 $/\$
57	51, 56	eqtrd 2505	. . . . . . . 8 $/\$
58	25, 10	mulcomd 9682	. . . . . . . 8 $/\$
59	57, 58	oveq12d 6326	. . . . . . 7 $/\$
60	50, 59	eqtrd 2505	. . . . . 6 $/\$
61	49, 60	oveq12d 6326	. . . . 5 $/\$
62	29, 61	eqtrd 2505	. . . 4 $/\$
63	19, 26, 15	adddird 9686	. . . . 5 $/\$
64	12, 18, 15	adddird 9686	. . . . . . 7 $/\$
65	35, 16, 15	mulassd 9684	. . . . . . . . 9 $/\$
66	14, 15, 15	mulassd 9684	. . . . . . . . . . 11 $/\$
67	15	sqvald 12451	. . . . . . . . . . . 12 $/\$
68	67	oveq2d 6324	. . . . . . . . . . 11 $/\$
69	66, 68	eqtr4d 2508	. . . . . . . . . 10 $/\$
70	69	oveq2d 6324	. . . . . . . . 9 $/\$
71	65, 70	eqtrd 2505	. . . . . . . 8 $/\$
72	71	oveq2d 6324	. . . . . . 7 $/\$
73	64, 72	eqtrd 2505	. . . . . 6 $/\$
74	23, 25, 15	adddird 9686	. . . . . . 7 $/\$
75	35, 21, 15	mulassd 9684	. . . . . . . . 9 $/\$
76	10, 20, 15	mulassd 9684	. . . . . . . . . . 11 $/\$
77	38	oveq2i 6319	. . . . . . . . . . . . 13
78		expp1 12317	. . . . . . . . . . . . . 14 $/\$
79	15, 40, 78	sylancl 675	. . . . . . . . . . . . 13 $/\$
80	77, 79	syl5req 2518	. . . . . . . . . . . 12 $/\$
81	80	oveq2d 6324	. . . . . . . . . . 11 $/\$
82	76, 81	eqtrd 2505	. . . . . . . . . 10 $/\$
83	82	oveq2d 6324	. . . . . . . . 9 $/\$
84	75, 83	eqtrd 2505	. . . . . . . 8 $/\$
85	1	oveq2i 6319	. . . . . . . . 9
86		expp1 12317	. . . . . . . . . 10 $/\$
87	15, 4, 86	sylancl 675	. . . . . . . . 9 $/\$
88	85, 87	syl5req 2518	. . . . . . . 8 $/\$
89	84, 88	oveq12d 6326	. . . . . . 7 $/\$
90	74, 89	eqtrd 2505	. . . . . 6 $/\$
91	73, 90	oveq12d 6326	. . . . 5 $/\$
92	12, 15	mulcld 9681	. . . . . 6 $/\$
93	14, 20	mulcld 9681	. . . . . . 7 $/\$
94		mulcl 9641	. . . . . . 7 $/\$
95	13, 93, 94	sylancr 676	. . . . . 6 $/\$
96	10, 25	mulcld 9681	. . . . . . . 8 $/\$
97		mulcl 9641	. . . . . . . 8 $/\$
98	13, 96, 97	sylancr 676	. . . . . . 7 $/\$
99		4nn0 10912	. . . . . . . 8
100		expcl 12328	. . . . . . . 8 $/\$
101	15, 99, 100	sylancl 675	. . . . . . 7 $/\$
102	98, 101	addcld 9680	. . . . . 6 $/\$
103	92, 95, 102	addassd 9683	. . . . 5 $/\$
104	63, 91, 103	3eqtrd 2509	. . . 4 $/\$
105	62, 104	oveq12d 6326	. . 3 $/\$
106		expcl 12328	. . . . . . 7 $/\$
107	10, 99, 106	sylancl 675	. . . . . 6 $/\$
108		mulcl 9641	. . . . . . 7 $/\$
109	13, 92, 108	sylancr 676	. . . . . 6 $/\$
110	107, 109	addcld 9680	. . . . 5 $/\$
111	95, 96	addcld 9680	. . . . 5 $/\$
112	95, 102	addcld 9680	. . . . 5 $/\$
113	110, 111, 92, 112	add4d 9878	. . . 4 $/\$
114	107, 109, 92	addassd 9683	. . . . . 6 $/\$
115	1	oveq1i 6318	. . . . . . . . 9
116		ax-1cn 9615	. . . . . . . . . . 11
117	116	a1i 11	. . . . . . . . . 10 $/\$
118	35, 117, 92	adddird 9686	. . . . . . . . 9 $/\$
119	115, 118	syl5eq 2517	. . . . . . . 8 $/\$
120	92	mulid2d 9679	. . . . . . . . 9 $/\$
121	120	oveq2d 6324	. . . . . . . 8 $/\$
122	119, 121	eqtrd 2505	. . . . . . 7 $/\$
123	122	oveq2d 6324	. . . . . 6 $/\$
124	114, 123	eqtr4d 2508	. . . . 5 $/\$
125	95, 96, 95, 102	add4d 9878	. . . . . 6 $/\$
126		3p3e6 10766	. . . . . . . . 9
127	126	oveq1i 6318	. . . . . . . 8
128	35, 35, 93	adddird 9686	. . . . . . . 8 $/\$
129	127, 128	syl5eqr 2519	. . . . . . 7 $/\$
130		3p1e4 10758	. . . . . . . . . . . . 13
131	13, 116, 130	addcomli 9843	. . . . . . . . . . . 12
132	131	oveq1i 6318	. . . . . . . . . . 11
133	117, 35, 96	adddird 9686	. . . . . . . . . . 11 $/\$
134	132, 133	syl5eqr 2519	. . . . . . . . . 10 $/\$
135	96	mulid2d 9679	. . . . . . . . . . 11 $/\$
136	135	oveq1d 6323	. . . . . . . . . 10 $/\$
137	134, 136	eqtrd 2505	. . . . . . . . 9 $/\$
138	137	oveq1d 6323	. . . . . . . 8 $/\$
139	96, 98, 101	addassd 9683	. . . . . . . 8 $/\$
140	138, 139	eqtrd 2505	. . . . . . 7 $/\$
141	129, 140	oveq12d 6326	. . . . . 6 $/\$
142	125, 141	eqtr4d 2508	. . . . 5 $/\$
143	124, 142	oveq12d 6326	. . . 4 $/\$
144	113, 143	eqtrd 2505	. . 3 $/\$
145	28, 105, 144	3eqtrd 2509	. 2 $/\$
146	7, 9, 145	3eqtrd 2509	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 376

wceq 1452

wcel 1904 (class class class)co 6308

cc 9555

c1 9558

caddc 9560

cmul 9562

c2 10681

c3 10682

c4 10683

c6 10685

cn0 10893

cexp 12310

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-3 10691 df-4 10692 df-5 10693 df-6 10694 df-n0 10894 df-z 10962 df-uz 11183 df-seq 12252 df-exp 12311

This theorem is referenced by: quart1 23861

W3C validator