binom4 - Metamath Proof Explorer

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

Theorem binom4 23306

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 13653, 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 10617	. . . 4
2	1	oveq2i 6307	. . 3
3		addcl 9591	. . . 4 $/\$
4		3nn0 10834	. . . 4
5		expp1 12175	. . . 4 $/\$
6	3, 4, 5	sylancl 662	. . 3 $/\$
7	2, 6	syl5eq 2510	. 2 $/\$
8		binom3 12289	. . 3 $/\$
9	8	oveq1d 6311	. 2 $/\$
10		simpl 457	. . . . . . 7 $/\$
11		expcl 12186	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 662	. . . . . 6 $/\$
13		3cn 10631	. . . . . . 7
14	10	sqcld 12310	. . . . . . . 8 $/\$
15		simpr 461	. . . . . . . 8 $/\$
16	14, 15	mulcld 9633	. . . . . . 7 $/\$
17		mulcl 9593	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 663	. . . . . 6 $/\$
19	12, 18	addcld 9632	. . . . 5 $/\$
20	15	sqcld 12310	. . . . . . . 8 $/\$
21	10, 20	mulcld 9633	. . . . . . 7 $/\$
22		mulcl 9593	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 663	. . . . . 6 $/\$
24		expcl 12186	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 662	. . . . . 6 $/\$
26	23, 25	addcld 9632	. . . . 5 $/\$
27	19, 26	addcld 9632	. . . 4 $/\$
28	27, 10, 15	adddid 9637	. . 3 $/\$
29	19, 26, 10	adddird 9638	. . . . 5 $/\$
30	12, 18, 10	adddird 9638	. . . . . . 7 $/\$
31	1	oveq2i 6307	. . . . . . . . 9
32		expp1 12175	. . . . . . . . . 10 $/\$
33	10, 4, 32	sylancl 662	. . . . . . . . 9 $/\$
34	31, 33	syl5req 2511	. . . . . . . 8 $/\$
35	13	a1i 11	. . . . . . . . . 10 $/\$
36	35, 16, 10	mulassd 9636	. . . . . . . . 9 $/\$
37	14, 15, 10	mul32d 9807	. . . . . . . . . . 11 $/\$
38		df-3 10616	. . . . . . . . . . . . . 14
39	38	oveq2i 6307	. . . . . . . . . . . . 13
40		2nn0 10833	. . . . . . . . . . . . . 14
41		expp1 12175	. . . . . . . . . . . . . 14 $/\$
42	10, 40, 41	sylancl 662	. . . . . . . . . . . . 13 $/\$
43	39, 42	syl5req 2511	. . . . . . . . . . . 12 $/\$
44	43	oveq1d 6311	. . . . . . . . . . 11 $/\$
45	37, 44	eqtrd 2498	. . . . . . . . . 10 $/\$
46	45	oveq2d 6312	. . . . . . . . 9 $/\$
47	36, 46	eqtrd 2498	. . . . . . . 8 $/\$
48	34, 47	oveq12d 6314	. . . . . . 7 $/\$
49	30, 48	eqtrd 2498	. . . . . 6 $/\$
50	23, 25, 10	adddird 9638	. . . . . . 7 $/\$
51	35, 21, 10	mulassd 9636	. . . . . . . . 9 $/\$
52	10, 20, 10	mul32d 9807	. . . . . . . . . . 11 $/\$
53	10	sqvald 12309	. . . . . . . . . . . 12 $/\$
54	53	oveq1d 6311	. . . . . . . . . . 11 $/\$
55	52, 54	eqtr4d 2501	. . . . . . . . . 10 $/\$
56	55	oveq2d 6312	. . . . . . . . 9 $/\$
57	51, 56	eqtrd 2498	. . . . . . . 8 $/\$
58	25, 10	mulcomd 9634	. . . . . . . 8 $/\$
59	57, 58	oveq12d 6314	. . . . . . 7 $/\$
60	50, 59	eqtrd 2498	. . . . . 6 $/\$
61	49, 60	oveq12d 6314	. . . . 5 $/\$
62	29, 61	eqtrd 2498	. . . 4 $/\$
63	19, 26, 15	adddird 9638	. . . . 5 $/\$
64	12, 18, 15	adddird 9638	. . . . . . 7 $/\$
65	35, 16, 15	mulassd 9636	. . . . . . . . 9 $/\$
66	14, 15, 15	mulassd 9636	. . . . . . . . . . 11 $/\$
67	15	sqvald 12309	. . . . . . . . . . . 12 $/\$
68	67	oveq2d 6312	. . . . . . . . . . 11 $/\$
69	66, 68	eqtr4d 2501	. . . . . . . . . 10 $/\$
70	69	oveq2d 6312	. . . . . . . . 9 $/\$
71	65, 70	eqtrd 2498	. . . . . . . 8 $/\$
72	71	oveq2d 6312	. . . . . . 7 $/\$
73	64, 72	eqtrd 2498	. . . . . 6 $/\$
74	23, 25, 15	adddird 9638	. . . . . . 7 $/\$
75	35, 21, 15	mulassd 9636	. . . . . . . . 9 $/\$
76	10, 20, 15	mulassd 9636	. . . . . . . . . . 11 $/\$
77	38	oveq2i 6307	. . . . . . . . . . . . 13
78		expp1 12175	. . . . . . . . . . . . . 14 $/\$
79	15, 40, 78	sylancl 662	. . . . . . . . . . . . 13 $/\$
80	77, 79	syl5req 2511	. . . . . . . . . . . 12 $/\$
81	80	oveq2d 6312	. . . . . . . . . . 11 $/\$
82	76, 81	eqtrd 2498	. . . . . . . . . 10 $/\$
83	82	oveq2d 6312	. . . . . . . . 9 $/\$
84	75, 83	eqtrd 2498	. . . . . . . 8 $/\$
85	1	oveq2i 6307	. . . . . . . . 9
86		expp1 12175	. . . . . . . . . 10 $/\$
87	15, 4, 86	sylancl 662	. . . . . . . . 9 $/\$
88	85, 87	syl5req 2511	. . . . . . . 8 $/\$
89	84, 88	oveq12d 6314	. . . . . . 7 $/\$
90	74, 89	eqtrd 2498	. . . . . 6 $/\$
91	73, 90	oveq12d 6314	. . . . 5 $/\$
92	12, 15	mulcld 9633	. . . . . 6 $/\$
93	14, 20	mulcld 9633	. . . . . . 7 $/\$
94		mulcl 9593	. . . . . . 7 $/\$
95	13, 93, 94	sylancr 663	. . . . . 6 $/\$
96	10, 25	mulcld 9633	. . . . . . . 8 $/\$
97		mulcl 9593	. . . . . . . 8 $/\$
98	13, 96, 97	sylancr 663	. . . . . . 7 $/\$
99		4nn0 10835	. . . . . . . 8
100		expcl 12186	. . . . . . . 8 $/\$
101	15, 99, 100	sylancl 662	. . . . . . 7 $/\$
102	98, 101	addcld 9632	. . . . . 6 $/\$
103	92, 95, 102	addassd 9635	. . . . 5 $/\$
104	63, 91, 103	3eqtrd 2502	. . . 4 $/\$
105	62, 104	oveq12d 6314	. . 3 $/\$
106		expcl 12186	. . . . . . 7 $/\$
107	10, 99, 106	sylancl 662	. . . . . 6 $/\$
108		mulcl 9593	. . . . . . 7 $/\$
109	13, 92, 108	sylancr 663	. . . . . 6 $/\$
110	107, 109	addcld 9632	. . . . 5 $/\$
111	95, 96	addcld 9632	. . . . 5 $/\$
112	95, 102	addcld 9632	. . . . 5 $/\$
113	110, 111, 92, 112	add4d 9822	. . . 4 $/\$
114	107, 109, 92	addassd 9635	. . . . . 6 $/\$
115	1	oveq1i 6306	. . . . . . . . 9
116		ax-1cn 9567	. . . . . . . . . . 11
117	116	a1i 11	. . . . . . . . . 10 $/\$
118	35, 117, 92	adddird 9638	. . . . . . . . 9 $/\$
119	115, 118	syl5eq 2510	. . . . . . . 8 $/\$
120	92	mulid2d 9631	. . . . . . . . 9 $/\$
121	120	oveq2d 6312	. . . . . . . 8 $/\$
122	119, 121	eqtrd 2498	. . . . . . 7 $/\$
123	122	oveq2d 6312	. . . . . 6 $/\$
124	114, 123	eqtr4d 2501	. . . . 5 $/\$
125	95, 96, 95, 102	add4d 9822	. . . . . 6 $/\$
126		3p3e6 10690	. . . . . . . . 9
127	126	oveq1i 6306	. . . . . . . 8
128	35, 35, 93	adddird 9638	. . . . . . . 8 $/\$
129	127, 128	syl5eqr 2512	. . . . . . 7 $/\$
130		3p1e4 10682	. . . . . . . . . . . . 13
131	13, 116, 130	addcomli 9789	. . . . . . . . . . . 12
132	131	oveq1i 6306	. . . . . . . . . . 11
133	117, 35, 96	adddird 9638	. . . . . . . . . . 11 $/\$
134	132, 133	syl5eqr 2512	. . . . . . . . . 10 $/\$
135	96	mulid2d 9631	. . . . . . . . . . 11 $/\$
136	135	oveq1d 6311	. . . . . . . . . 10 $/\$
137	134, 136	eqtrd 2498	. . . . . . . . 9 $/\$
138	137	oveq1d 6311	. . . . . . . 8 $/\$
139	96, 98, 101	addassd 9635	. . . . . . . 8 $/\$
140	138, 139	eqtrd 2498	. . . . . . 7 $/\$
141	129, 140	oveq12d 6314	. . . . . 6 $/\$
142	125, 141	eqtr4d 2501	. . . . 5 $/\$
143	124, 142	oveq12d 6314	. . . 4 $/\$
144	113, 143	eqtrd 2498	. . 3 $/\$
145	28, 105, 144	3eqtrd 2502	. 2 $/\$
146	7, 9, 145	3eqtrd 2502	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1395

wcel 1819 (class class class)co 6296

cc 9507

c1 9510

caddc 9512

cmul 9514

c2 10606

c3 10607

c4 10608

c6 10610

cn0 10816

cexp 12168

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-iun 4334 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6700 df-2nd 6800 df-recs 7060 df-rdg 7094 df-er 7329 df-en 7536 df-dom 7537 df-sdom 7538 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-nn 10557 df-2 10615 df-3 10616 df-4 10617 df-5 10618 df-6 10619 df-n0 10817 df-z 10886 df-uz 11107 df-seq 12110 df-exp 12169

This theorem is referenced by: quart1 23312

W3C validator