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 23769

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 13881, 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 10667	. . . 4
2	1	oveq2i 6299	. . 3
3		addcl 9618	. . . 4 $/\$
4		3nn0 10884	. . . 4
5		expp1 12276	. . . 4 $/\$
6	3, 4, 5	sylancl 667	. . 3 $/\$
7	2, 6	syl5eq 2496	. 2 $/\$
8		binom3 12390	. . 3 $/\$
9	8	oveq1d 6303	. 2 $/\$
10		simpl 459	. . . . . . 7 $/\$
11		expcl 12287	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 667	. . . . . 6 $/\$
13		3cn 10681	. . . . . . 7
14	10	sqcld 12411	. . . . . . . 8 $/\$
15		simpr 463	. . . . . . . 8 $/\$
16	14, 15	mulcld 9660	. . . . . . 7 $/\$
17		mulcl 9620	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 668	. . . . . 6 $/\$
19	12, 18	addcld 9659	. . . . 5 $/\$
20	15	sqcld 12411	. . . . . . . 8 $/\$
21	10, 20	mulcld 9660	. . . . . . 7 $/\$
22		mulcl 9620	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 668	. . . . . 6 $/\$
24		expcl 12287	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 667	. . . . . 6 $/\$
26	23, 25	addcld 9659	. . . . 5 $/\$
27	19, 26	addcld 9659	. . . 4 $/\$
28	27, 10, 15	adddid 9664	. . 3 $/\$
29	19, 26, 10	adddird 9665	. . . . 5 $/\$
30	12, 18, 10	adddird 9665	. . . . . . 7 $/\$
31	1	oveq2i 6299	. . . . . . . . 9
32		expp1 12276	. . . . . . . . . 10 $/\$
33	10, 4, 32	sylancl 667	. . . . . . . . 9 $/\$
34	31, 33	syl5req 2497	. . . . . . . 8 $/\$
35	13	a1i 11	. . . . . . . . . 10 $/\$
36	35, 16, 10	mulassd 9663	. . . . . . . . 9 $/\$
37	14, 15, 10	mul32d 9840	. . . . . . . . . . 11 $/\$
38		df-3 10666	. . . . . . . . . . . . . 14
39	38	oveq2i 6299	. . . . . . . . . . . . 13
40		2nn0 10883	. . . . . . . . . . . . . 14
41		expp1 12276	. . . . . . . . . . . . . 14 $/\$
42	10, 40, 41	sylancl 667	. . . . . . . . . . . . 13 $/\$
43	39, 42	syl5req 2497	. . . . . . . . . . . 12 $/\$
44	43	oveq1d 6303	. . . . . . . . . . 11 $/\$
45	37, 44	eqtrd 2484	. . . . . . . . . 10 $/\$
46	45	oveq2d 6304	. . . . . . . . 9 $/\$
47	36, 46	eqtrd 2484	. . . . . . . 8 $/\$
48	34, 47	oveq12d 6306	. . . . . . 7 $/\$
49	30, 48	eqtrd 2484	. . . . . 6 $/\$
50	23, 25, 10	adddird 9665	. . . . . . 7 $/\$
51	35, 21, 10	mulassd 9663	. . . . . . . . 9 $/\$
52	10, 20, 10	mul32d 9840	. . . . . . . . . . 11 $/\$
53	10	sqvald 12410	. . . . . . . . . . . 12 $/\$
54	53	oveq1d 6303	. . . . . . . . . . 11 $/\$
55	52, 54	eqtr4d 2487	. . . . . . . . . 10 $/\$
56	55	oveq2d 6304	. . . . . . . . 9 $/\$
57	51, 56	eqtrd 2484	. . . . . . . 8 $/\$
58	25, 10	mulcomd 9661	. . . . . . . 8 $/\$
59	57, 58	oveq12d 6306	. . . . . . 7 $/\$
60	50, 59	eqtrd 2484	. . . . . 6 $/\$
61	49, 60	oveq12d 6306	. . . . 5 $/\$
62	29, 61	eqtrd 2484	. . . 4 $/\$
63	19, 26, 15	adddird 9665	. . . . 5 $/\$
64	12, 18, 15	adddird 9665	. . . . . . 7 $/\$
65	35, 16, 15	mulassd 9663	. . . . . . . . 9 $/\$
66	14, 15, 15	mulassd 9663	. . . . . . . . . . 11 $/\$
67	15	sqvald 12410	. . . . . . . . . . . 12 $/\$
68	67	oveq2d 6304	. . . . . . . . . . 11 $/\$
69	66, 68	eqtr4d 2487	. . . . . . . . . 10 $/\$
70	69	oveq2d 6304	. . . . . . . . 9 $/\$
71	65, 70	eqtrd 2484	. . . . . . . 8 $/\$
72	71	oveq2d 6304	. . . . . . 7 $/\$
73	64, 72	eqtrd 2484	. . . . . 6 $/\$
74	23, 25, 15	adddird 9665	. . . . . . 7 $/\$
75	35, 21, 15	mulassd 9663	. . . . . . . . 9 $/\$
76	10, 20, 15	mulassd 9663	. . . . . . . . . . 11 $/\$
77	38	oveq2i 6299	. . . . . . . . . . . . 13
78		expp1 12276	. . . . . . . . . . . . . 14 $/\$
79	15, 40, 78	sylancl 667	. . . . . . . . . . . . 13 $/\$
80	77, 79	syl5req 2497	. . . . . . . . . . . 12 $/\$
81	80	oveq2d 6304	. . . . . . . . . . 11 $/\$
82	76, 81	eqtrd 2484	. . . . . . . . . 10 $/\$
83	82	oveq2d 6304	. . . . . . . . 9 $/\$
84	75, 83	eqtrd 2484	. . . . . . . 8 $/\$
85	1	oveq2i 6299	. . . . . . . . 9
86		expp1 12276	. . . . . . . . . 10 $/\$
87	15, 4, 86	sylancl 667	. . . . . . . . 9 $/\$
88	85, 87	syl5req 2497	. . . . . . . 8 $/\$
89	84, 88	oveq12d 6306	. . . . . . 7 $/\$
90	74, 89	eqtrd 2484	. . . . . 6 $/\$
91	73, 90	oveq12d 6306	. . . . 5 $/\$
92	12, 15	mulcld 9660	. . . . . 6 $/\$
93	14, 20	mulcld 9660	. . . . . . 7 $/\$
94		mulcl 9620	. . . . . . 7 $/\$
95	13, 93, 94	sylancr 668	. . . . . 6 $/\$
96	10, 25	mulcld 9660	. . . . . . . 8 $/\$
97		mulcl 9620	. . . . . . . 8 $/\$
98	13, 96, 97	sylancr 668	. . . . . . 7 $/\$
99		4nn0 10885	. . . . . . . 8
100		expcl 12287	. . . . . . . 8 $/\$
101	15, 99, 100	sylancl 667	. . . . . . 7 $/\$
102	98, 101	addcld 9659	. . . . . 6 $/\$
103	92, 95, 102	addassd 9662	. . . . 5 $/\$
104	63, 91, 103	3eqtrd 2488	. . . 4 $/\$
105	62, 104	oveq12d 6306	. . 3 $/\$
106		expcl 12287	. . . . . . 7 $/\$
107	10, 99, 106	sylancl 667	. . . . . 6 $/\$
108		mulcl 9620	. . . . . . 7 $/\$
109	13, 92, 108	sylancr 668	. . . . . 6 $/\$
110	107, 109	addcld 9659	. . . . 5 $/\$
111	95, 96	addcld 9659	. . . . 5 $/\$
112	95, 102	addcld 9659	. . . . 5 $/\$
113	110, 111, 92, 112	add4d 9855	. . . 4 $/\$
114	107, 109, 92	addassd 9662	. . . . . 6 $/\$
115	1	oveq1i 6298	. . . . . . . . 9
116		ax-1cn 9594	. . . . . . . . . . 11
117	116	a1i 11	. . . . . . . . . 10 $/\$
118	35, 117, 92	adddird 9665	. . . . . . . . 9 $/\$
119	115, 118	syl5eq 2496	. . . . . . . 8 $/\$
120	92	mulid2d 9658	. . . . . . . . 9 $/\$
121	120	oveq2d 6304	. . . . . . . 8 $/\$
122	119, 121	eqtrd 2484	. . . . . . 7 $/\$
123	122	oveq2d 6304	. . . . . 6 $/\$
124	114, 123	eqtr4d 2487	. . . . 5 $/\$
125	95, 96, 95, 102	add4d 9855	. . . . . 6 $/\$
126		3p3e6 10740	. . . . . . . . 9
127	126	oveq1i 6298	. . . . . . . 8
128	35, 35, 93	adddird 9665	. . . . . . . 8 $/\$
129	127, 128	syl5eqr 2498	. . . . . . 7 $/\$
130		3p1e4 10732	. . . . . . . . . . . . 13
131	13, 116, 130	addcomli 9822	. . . . . . . . . . . 12
132	131	oveq1i 6298	. . . . . . . . . . 11
133	117, 35, 96	adddird 9665	. . . . . . . . . . 11 $/\$
134	132, 133	syl5eqr 2498	. . . . . . . . . 10 $/\$
135	96	mulid2d 9658	. . . . . . . . . . 11 $/\$
136	135	oveq1d 6303	. . . . . . . . . 10 $/\$
137	134, 136	eqtrd 2484	. . . . . . . . 9 $/\$
138	137	oveq1d 6303	. . . . . . . 8 $/\$
139	96, 98, 101	addassd 9662	. . . . . . . 8 $/\$
140	138, 139	eqtrd 2484	. . . . . . 7 $/\$
141	129, 140	oveq12d 6306	. . . . . 6 $/\$
142	125, 141	eqtr4d 2487	. . . . 5 $/\$
143	124, 142	oveq12d 6306	. . . 4 $/\$
144	113, 143	eqtrd 2484	. . 3 $/\$
145	28, 105, 144	3eqtrd 2488	. 2 $/\$
146	7, 9, 145	3eqtrd 2488	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371

wceq 1443

wcel 1886 (class class class)co 6288

cc 9534

c1 9537

caddc 9539

cmul 9541

c2 10656

c3 10657

c4 10658

c6 10660

cn0 10866

cexp 12269

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-2 10665 df-3 10666 df-4 10667 df-5 10668 df-6 10669 df-n0 10867 df-z 10935 df-uz 11157 df-seq 12211 df-exp 12270

This theorem is referenced by: quart1 23775

W3C validator