binom4 - Metamath Proof Explorer

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

Theorem binom4 23047

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 13622, 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 10608	. . . 4
2	1	oveq2i 6306	. . 3
3		addcl 9586	. . . 4 $/\$
4		3nn0 10825	. . . 4
5		expp1 12153	. . . 4 $/\$
6	3, 4, 5	sylancl 662	. . 3 $/\$
7	2, 6	syl5eq 2520	. 2 $/\$
8		binom3 12267	. . 3 $/\$
9	8	oveq1d 6310	. 2 $/\$
10		simpl 457	. . . . . . 7 $/\$
11		expcl 12164	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 662	. . . . . 6 $/\$
13		3cn 10622	. . . . . . 7
14	10	sqcld 12288	. . . . . . . 8 $/\$
15		simpr 461	. . . . . . . 8 $/\$
16	14, 15	mulcld 9628	. . . . . . 7 $/\$
17		mulcl 9588	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 663	. . . . . 6 $/\$
19	12, 18	addcld 9627	. . . . 5 $/\$
20	15	sqcld 12288	. . . . . . . 8 $/\$
21	10, 20	mulcld 9628	. . . . . . 7 $/\$
22		mulcl 9588	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 663	. . . . . 6 $/\$
24		expcl 12164	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 662	. . . . . 6 $/\$
26	23, 25	addcld 9627	. . . . 5 $/\$
27	19, 26	addcld 9627	. . . 4 $/\$
28	27, 10, 15	adddid 9632	. . 3 $/\$
29	19, 26, 10	adddird 9633	. . . . 5 $/\$
30	12, 18, 10	adddird 9633	. . . . . . 7 $/\$
31	1	oveq2i 6306	. . . . . . . . 9
32		expp1 12153	. . . . . . . . . 10 $/\$
33	10, 4, 32	sylancl 662	. . . . . . . . 9 $/\$
34	31, 33	syl5req 2521	. . . . . . . 8 $/\$
35	13	a1i 11	. . . . . . . . . 10 $/\$
36	35, 16, 10	mulassd 9631	. . . . . . . . 9 $/\$
37	14, 15, 10	mul32d 9801	. . . . . . . . . . 11 $/\$
38		df-3 10607	. . . . . . . . . . . . . 14
39	38	oveq2i 6306	. . . . . . . . . . . . 13
40		2nn0 10824	. . . . . . . . . . . . . 14
41		expp1 12153	. . . . . . . . . . . . . 14 $/\$
42	10, 40, 41	sylancl 662	. . . . . . . . . . . . 13 $/\$
43	39, 42	syl5req 2521	. . . . . . . . . . . 12 $/\$
44	43	oveq1d 6310	. . . . . . . . . . 11 $/\$
45	37, 44	eqtrd 2508	. . . . . . . . . 10 $/\$
46	45	oveq2d 6311	. . . . . . . . 9 $/\$
47	36, 46	eqtrd 2508	. . . . . . . 8 $/\$
48	34, 47	oveq12d 6313	. . . . . . 7 $/\$
49	30, 48	eqtrd 2508	. . . . . 6 $/\$
50	23, 25, 10	adddird 9633	. . . . . . 7 $/\$
51	35, 21, 10	mulassd 9631	. . . . . . . . 9 $/\$
52	10, 20, 10	mul32d 9801	. . . . . . . . . . 11 $/\$
53	10	sqvald 12287	. . . . . . . . . . . 12 $/\$
54	53	oveq1d 6310	. . . . . . . . . . 11 $/\$
55	52, 54	eqtr4d 2511	. . . . . . . . . 10 $/\$
56	55	oveq2d 6311	. . . . . . . . 9 $/\$
57	51, 56	eqtrd 2508	. . . . . . . 8 $/\$
58	25, 10	mulcomd 9629	. . . . . . . 8 $/\$
59	57, 58	oveq12d 6313	. . . . . . 7 $/\$
60	50, 59	eqtrd 2508	. . . . . 6 $/\$
61	49, 60	oveq12d 6313	. . . . 5 $/\$
62	29, 61	eqtrd 2508	. . . 4 $/\$
63	19, 26, 15	adddird 9633	. . . . 5 $/\$
64	12, 18, 15	adddird 9633	. . . . . . 7 $/\$
65	35, 16, 15	mulassd 9631	. . . . . . . . 9 $/\$
66	14, 15, 15	mulassd 9631	. . . . . . . . . . 11 $/\$
67	15	sqvald 12287	. . . . . . . . . . . 12 $/\$
68	67	oveq2d 6311	. . . . . . . . . . 11 $/\$
69	66, 68	eqtr4d 2511	. . . . . . . . . 10 $/\$
70	69	oveq2d 6311	. . . . . . . . 9 $/\$
71	65, 70	eqtrd 2508	. . . . . . . 8 $/\$
72	71	oveq2d 6311	. . . . . . 7 $/\$
73	64, 72	eqtrd 2508	. . . . . 6 $/\$
74	23, 25, 15	adddird 9633	. . . . . . 7 $/\$
75	35, 21, 15	mulassd 9631	. . . . . . . . 9 $/\$
76	10, 20, 15	mulassd 9631	. . . . . . . . . . 11 $/\$
77	38	oveq2i 6306	. . . . . . . . . . . . 13
78		expp1 12153	. . . . . . . . . . . . . 14 $/\$
79	15, 40, 78	sylancl 662	. . . . . . . . . . . . 13 $/\$
80	77, 79	syl5req 2521	. . . . . . . . . . . 12 $/\$
81	80	oveq2d 6311	. . . . . . . . . . 11 $/\$
82	76, 81	eqtrd 2508	. . . . . . . . . 10 $/\$
83	82	oveq2d 6311	. . . . . . . . 9 $/\$
84	75, 83	eqtrd 2508	. . . . . . . 8 $/\$
85	1	oveq2i 6306	. . . . . . . . 9
86		expp1 12153	. . . . . . . . . 10 $/\$
87	15, 4, 86	sylancl 662	. . . . . . . . 9 $/\$
88	85, 87	syl5req 2521	. . . . . . . 8 $/\$
89	84, 88	oveq12d 6313	. . . . . . 7 $/\$
90	74, 89	eqtrd 2508	. . . . . 6 $/\$
91	73, 90	oveq12d 6313	. . . . 5 $/\$
92	12, 15	mulcld 9628	. . . . . 6 $/\$
93	14, 20	mulcld 9628	. . . . . . 7 $/\$
94		mulcl 9588	. . . . . . 7 $/\$
95	13, 93, 94	sylancr 663	. . . . . 6 $/\$
96	10, 25	mulcld 9628	. . . . . . . 8 $/\$
97		mulcl 9588	. . . . . . . 8 $/\$
98	13, 96, 97	sylancr 663	. . . . . . 7 $/\$
99		4nn0 10826	. . . . . . . 8
100		expcl 12164	. . . . . . . 8 $/\$
101	15, 99, 100	sylancl 662	. . . . . . 7 $/\$
102	98, 101	addcld 9627	. . . . . 6 $/\$
103	92, 95, 102	addassd 9630	. . . . 5 $/\$
104	63, 91, 103	3eqtrd 2512	. . . 4 $/\$
105	62, 104	oveq12d 6313	. . 3 $/\$
106		expcl 12164	. . . . . . 7 $/\$
107	10, 99, 106	sylancl 662	. . . . . 6 $/\$
108		mulcl 9588	. . . . . . 7 $/\$
109	13, 92, 108	sylancr 663	. . . . . 6 $/\$
110	107, 109	addcld 9627	. . . . 5 $/\$
111	95, 96	addcld 9627	. . . . 5 $/\$
112	95, 102	addcld 9627	. . . . 5 $/\$
113	110, 111, 92, 112	add4d 9815	. . . 4 $/\$
114	107, 109, 92	addassd 9630	. . . . . 6 $/\$
115	1	oveq1i 6305	. . . . . . . . 9
116		ax-1cn 9562	. . . . . . . . . . 11
117	116	a1i 11	. . . . . . . . . 10 $/\$
118	35, 117, 92	adddird 9633	. . . . . . . . 9 $/\$
119	115, 118	syl5eq 2520	. . . . . . . 8 $/\$
120	92	mulid2d 9626	. . . . . . . . 9 $/\$
121	120	oveq2d 6311	. . . . . . . 8 $/\$
122	119, 121	eqtrd 2508	. . . . . . 7 $/\$
123	122	oveq2d 6311	. . . . . 6 $/\$
124	114, 123	eqtr4d 2511	. . . . 5 $/\$
125	95, 96, 95, 102	add4d 9815	. . . . . 6 $/\$
126		3p3e6 10681	. . . . . . . . 9
127	126	oveq1i 6305	. . . . . . . 8
128	35, 35, 93	adddird 9633	. . . . . . . 8 $/\$
129	127, 128	syl5eqr 2522	. . . . . . 7 $/\$
130		3p1e4 10673	. . . . . . . . . . . . 13
131	13, 116, 130	addcomli 9783	. . . . . . . . . . . 12
132	131	oveq1i 6305	. . . . . . . . . . 11
133	117, 35, 96	adddird 9633	. . . . . . . . . . 11 $/\$
134	132, 133	syl5eqr 2522	. . . . . . . . . 10 $/\$
135	96	mulid2d 9626	. . . . . . . . . . 11 $/\$
136	135	oveq1d 6310	. . . . . . . . . 10 $/\$
137	134, 136	eqtrd 2508	. . . . . . . . 9 $/\$
138	137	oveq1d 6310	. . . . . . . 8 $/\$
139	96, 98, 101	addassd 9630	. . . . . . . 8 $/\$
140	138, 139	eqtrd 2508	. . . . . . 7 $/\$
141	129, 140	oveq12d 6313	. . . . . 6 $/\$
142	125, 141	eqtr4d 2511	. . . . 5 $/\$
143	124, 142	oveq12d 6313	. . . 4 $/\$
144	113, 143	eqtrd 2508	. . 3 $/\$
145	28, 105, 144	3eqtrd 2512	. 2 $/\$
146	7, 9, 145	3eqtrd 2512	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1379

wcel 1767 (class class class)co 6295

cc 9502

c1 9505

caddc 9507

cmul 9509

c2 10597

c3 10598

c4 10599

c6 10601

cn0 10807

cexp 12146

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 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 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6696 df-2nd 6796 df-recs 7054 df-rdg 7088 df-er 7323 df-en 7529 df-dom 7530 df-sdom 7531 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-nn 10549 df-2 10606 df-3 10607 df-4 10608 df-5 10609 df-6 10610 df-n0 10808 df-z 10877 df-uz 11095 df-seq 12088 df-exp 12147

This theorem is referenced by: quart1 23053

W3C validator