binom4 - Metamath Proof Explorer

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

Theorem binom4 22371

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 13404, 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 10486	. . . 4
2	1	oveq2i 6204	. . 3
3		addcl 9468	. . . 4 $/\$
4		3nn0 10701	. . . 4
5		expp1 11982	. . . 4 $/\$
6	3, 4, 5	sylancl 662	. . 3 $/\$
7	2, 6	syl5eq 2504	. 2 $/\$
8		binom3 12095	. . 3 $/\$
9	8	oveq1d 6208	. 2 $/\$
10		simpl 457	. . . . . . 7 $/\$
11		expcl 11993	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 662	. . . . . 6 $/\$
13		3cn 10500	. . . . . . 7
14	10	sqcld 12116	. . . . . . . 8 $/\$
15		simpr 461	. . . . . . . 8 $/\$
16	14, 15	mulcld 9510	. . . . . . 7 $/\$
17		mulcl 9470	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 663	. . . . . 6 $/\$
19	12, 18	addcld 9509	. . . . 5 $/\$
20	15	sqcld 12116	. . . . . . . 8 $/\$
21	10, 20	mulcld 9510	. . . . . . 7 $/\$
22		mulcl 9470	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 663	. . . . . 6 $/\$
24		expcl 11993	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 662	. . . . . 6 $/\$
26	23, 25	addcld 9509	. . . . 5 $/\$
27	19, 26	addcld 9509	. . . 4 $/\$
28	27, 10, 15	adddid 9514	. . 3 $/\$
29	19, 26, 10	adddird 9515	. . . . 5 $/\$
30	12, 18, 10	adddird 9515	. . . . . . 7 $/\$
31	1	oveq2i 6204	. . . . . . . . 9
32		expp1 11982	. . . . . . . . . 10 $/\$
33	10, 4, 32	sylancl 662	. . . . . . . . 9 $/\$
34	31, 33	syl5req 2505	. . . . . . . 8 $/\$
35	13	a1i 11	. . . . . . . . . 10 $/\$
36	35, 16, 10	mulassd 9513	. . . . . . . . 9 $/\$
37	14, 15, 10	mul32d 9683	. . . . . . . . . . 11 $/\$
38		df-3 10485	. . . . . . . . . . . . . 14
39	38	oveq2i 6204	. . . . . . . . . . . . 13
40		2nn0 10700	. . . . . . . . . . . . . 14
41		expp1 11982	. . . . . . . . . . . . . 14 $/\$
42	10, 40, 41	sylancl 662	. . . . . . . . . . . . 13 $/\$
43	39, 42	syl5req 2505	. . . . . . . . . . . 12 $/\$
44	43	oveq1d 6208	. . . . . . . . . . 11 $/\$
45	37, 44	eqtrd 2492	. . . . . . . . . 10 $/\$
46	45	oveq2d 6209	. . . . . . . . 9 $/\$
47	36, 46	eqtrd 2492	. . . . . . . 8 $/\$
48	34, 47	oveq12d 6211	. . . . . . 7 $/\$
49	30, 48	eqtrd 2492	. . . . . 6 $/\$
50	23, 25, 10	adddird 9515	. . . . . . 7 $/\$
51	35, 21, 10	mulassd 9513	. . . . . . . . 9 $/\$
52	10, 20, 10	mul32d 9683	. . . . . . . . . . 11 $/\$
53	10	sqvald 12115	. . . . . . . . . . . 12 $/\$
54	53	oveq1d 6208	. . . . . . . . . . 11 $/\$
55	52, 54	eqtr4d 2495	. . . . . . . . . 10 $/\$
56	55	oveq2d 6209	. . . . . . . . 9 $/\$
57	51, 56	eqtrd 2492	. . . . . . . 8 $/\$
58	25, 10	mulcomd 9511	. . . . . . . 8 $/\$
59	57, 58	oveq12d 6211	. . . . . . 7 $/\$
60	50, 59	eqtrd 2492	. . . . . 6 $/\$
61	49, 60	oveq12d 6211	. . . . 5 $/\$
62	29, 61	eqtrd 2492	. . . 4 $/\$
63	19, 26, 15	adddird 9515	. . . . 5 $/\$
64	12, 18, 15	adddird 9515	. . . . . . 7 $/\$
65	35, 16, 15	mulassd 9513	. . . . . . . . 9 $/\$
66	14, 15, 15	mulassd 9513	. . . . . . . . . . 11 $/\$
67	15	sqvald 12115	. . . . . . . . . . . 12 $/\$
68	67	oveq2d 6209	. . . . . . . . . . 11 $/\$
69	66, 68	eqtr4d 2495	. . . . . . . . . 10 $/\$
70	69	oveq2d 6209	. . . . . . . . 9 $/\$
71	65, 70	eqtrd 2492	. . . . . . . 8 $/\$
72	71	oveq2d 6209	. . . . . . 7 $/\$
73	64, 72	eqtrd 2492	. . . . . 6 $/\$
74	23, 25, 15	adddird 9515	. . . . . . 7 $/\$
75	35, 21, 15	mulassd 9513	. . . . . . . . 9 $/\$
76	10, 20, 15	mulassd 9513	. . . . . . . . . . 11 $/\$
77	38	oveq2i 6204	. . . . . . . . . . . . 13
78		expp1 11982	. . . . . . . . . . . . . 14 $/\$
79	15, 40, 78	sylancl 662	. . . . . . . . . . . . 13 $/\$
80	77, 79	syl5req 2505	. . . . . . . . . . . 12 $/\$
81	80	oveq2d 6209	. . . . . . . . . . 11 $/\$
82	76, 81	eqtrd 2492	. . . . . . . . . 10 $/\$
83	82	oveq2d 6209	. . . . . . . . 9 $/\$
84	75, 83	eqtrd 2492	. . . . . . . 8 $/\$
85	1	oveq2i 6204	. . . . . . . . 9
86		expp1 11982	. . . . . . . . . 10 $/\$
87	15, 4, 86	sylancl 662	. . . . . . . . 9 $/\$
88	85, 87	syl5req 2505	. . . . . . . 8 $/\$
89	84, 88	oveq12d 6211	. . . . . . 7 $/\$
90	74, 89	eqtrd 2492	. . . . . 6 $/\$
91	73, 90	oveq12d 6211	. . . . 5 $/\$
92	12, 15	mulcld 9510	. . . . . 6 $/\$
93	14, 20	mulcld 9510	. . . . . . 7 $/\$
94		mulcl 9470	. . . . . . 7 $/\$
95	13, 93, 94	sylancr 663	. . . . . 6 $/\$
96	10, 25	mulcld 9510	. . . . . . . 8 $/\$
97		mulcl 9470	. . . . . . . 8 $/\$
98	13, 96, 97	sylancr 663	. . . . . . 7 $/\$
99		4nn0 10702	. . . . . . . 8
100		expcl 11993	. . . . . . . 8 $/\$
101	15, 99, 100	sylancl 662	. . . . . . 7 $/\$
102	98, 101	addcld 9509	. . . . . 6 $/\$
103	92, 95, 102	addassd 9512	. . . . 5 $/\$
104	63, 91, 103	3eqtrd 2496	. . . 4 $/\$
105	62, 104	oveq12d 6211	. . 3 $/\$
106		expcl 11993	. . . . . . 7 $/\$
107	10, 99, 106	sylancl 662	. . . . . 6 $/\$
108		mulcl 9470	. . . . . . 7 $/\$
109	13, 92, 108	sylancr 663	. . . . . 6 $/\$
110	107, 109	addcld 9509	. . . . 5 $/\$
111	95, 96	addcld 9509	. . . . 5 $/\$
112	95, 102	addcld 9509	. . . . 5 $/\$
113	110, 111, 92, 112	add4d 9697	. . . 4 $/\$
114	107, 109, 92	addassd 9512	. . . . . 6 $/\$
115	1	oveq1i 6203	. . . . . . . . 9
116		ax-1cn 9444	. . . . . . . . . . 11
117	116	a1i 11	. . . . . . . . . 10 $/\$
118	35, 117, 92	adddird 9515	. . . . . . . . 9 $/\$
119	115, 118	syl5eq 2504	. . . . . . . 8 $/\$
120	92	mulid2d 9508	. . . . . . . . 9 $/\$
121	120	oveq2d 6209	. . . . . . . 8 $/\$
122	119, 121	eqtrd 2492	. . . . . . 7 $/\$
123	122	oveq2d 6209	. . . . . 6 $/\$
124	114, 123	eqtr4d 2495	. . . . 5 $/\$
125	95, 96, 95, 102	add4d 9697	. . . . . 6 $/\$
126		3p3e6 10559	. . . . . . . . 9
127	126	oveq1i 6203	. . . . . . . 8
128	35, 35, 93	adddird 9515	. . . . . . . 8 $/\$
129	127, 128	syl5eqr 2506	. . . . . . 7 $/\$
130		3p1e4 10551	. . . . . . . . . . . . 13
131	13, 116, 130	addcomli 9665	. . . . . . . . . . . 12
132	131	oveq1i 6203	. . . . . . . . . . 11
133	117, 35, 96	adddird 9515	. . . . . . . . . . 11 $/\$
134	132, 133	syl5eqr 2506	. . . . . . . . . 10 $/\$
135	96	mulid2d 9508	. . . . . . . . . . 11 $/\$
136	135	oveq1d 6208	. . . . . . . . . 10 $/\$
137	134, 136	eqtrd 2492	. . . . . . . . 9 $/\$
138	137	oveq1d 6208	. . . . . . . 8 $/\$
139	96, 98, 101	addassd 9512	. . . . . . . 8 $/\$
140	138, 139	eqtrd 2492	. . . . . . 7 $/\$
141	129, 140	oveq12d 6211	. . . . . 6 $/\$
142	125, 141	eqtr4d 2495	. . . . 5 $/\$
143	124, 142	oveq12d 6211	. . . 4 $/\$
144	113, 143	eqtrd 2492	. . 3 $/\$
145	28, 105, 144	3eqtrd 2496	. 2 $/\$
146	7, 9, 145	3eqtrd 2496	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1370

wcel 1758 (class class class)co 6193

cc 9384

c1 9387

caddc 9389

cmul 9391

c2 10475

c3 10476

c4 10477

c6 10479

cn0 10683

cexp 11975

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4514 ax-nul 4522 ax-pow 4571 ax-pr 4632 ax-un 6475 ax-cnex 9442 ax-resscn 9443 ax-1cn 9444 ax-icn 9445 ax-addcl 9446 ax-addrcl 9447 ax-mulcl 9448 ax-mulrcl 9449 ax-mulcom 9450 ax-addass 9451 ax-mulass 9452 ax-distr 9453 ax-i2m1 9454 ax-1ne0 9455 ax-1rid 9456 ax-rnegex 9457 ax-rrecex 9458 ax-cnre 9459 ax-pre-lttri 9460 ax-pre-lttrn 9461 ax-pre-ltadd 9462 ax-pre-mulgt0 9463

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3073 df-sbc 3288 df-csb 3390 df-dif 3432 df-un 3434 df-in 3436 df-ss 3443 df-pss 3445 df-nul 3739 df-if 3893 df-pw 3963 df-sn 3979 df-pr 3981 df-tp 3983 df-op 3985 df-uni 4193 df-iun 4274 df-br 4394 df-opab 4452 df-mpt 4453 df-tr 4487 df-eprel 4733 df-id 4737 df-po 4742 df-so 4743 df-fr 4780 df-we 4782 df-ord 4823 df-on 4824 df-lim 4825 df-suc 4826 df-xp 4947 df-rel 4948 df-cnv 4949 df-co 4950 df-dm 4951 df-rn 4952 df-res 4953 df-ima 4954 df-iota 5482 df-fun 5521 df-fn 5522 df-f 5523 df-f1 5524 df-fo 5525 df-f1o 5526 df-fv 5527 df-riota 6154 df-ov 6196 df-oprab 6197 df-mpt2 6198 df-om 6580 df-2nd 6681 df-recs 6935 df-rdg 6969 df-er 7204 df-en 7414 df-dom 7415 df-sdom 7416 df-pnf 9524 df-mnf 9525 df-xr 9526 df-ltxr 9527 df-le 9528 df-sub 9701 df-neg 9702 df-nn 10427 df-2 10484 df-3 10485 df-4 10486 df-5 10487 df-6 10488 df-n0 10684 df-z 10751 df-uz 10966 df-seq 11917 df-exp 11976

This theorem is referenced by: quart1 22377

W3C validator