binom4 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > binom4		Unicode version

Theorem binom4 13267

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11374, 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 8888	. . . 4
2	1	oveq2i 5832	. . 3
3		addcl 7851	. . . 4 $/\$
4		3nn0 9102	. . . 4
5		expp1 10419	. . . 4 $/\$
6	3, 4, 5	sylancl 410	. . 3 $/\$
7	2, 6	syl5eq 2202	. 2 $/\$
8		binom3 10528	. . 3 $/\$
9	8	oveq1d 5836	. 2 $/\$
10		simpl 108	. . . . . . 7 $/\$
11		expcl 10430	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 410	. . . . . 6 $/\$
13		3cn 8902	. . . . . . 7
14	10	sqcld 10542	. . . . . . . 8 $/\$
15		simpr 109	. . . . . . . 8 $/\$
16	14, 15	mulcld 7892	. . . . . . 7 $/\$
17		mulcl 7853	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 411	. . . . . 6 $/\$
19	12, 18	addcld 7891	. . . . 5 $/\$
20	15	sqcld 10542	. . . . . . . 8 $/\$
21	10, 20	mulcld 7892	. . . . . . 7 $/\$
22		mulcl 7853	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 411	. . . . . 6 $/\$
24		expcl 10430	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 410	. . . . . 6 $/\$
26	23, 25	addcld 7891	. . . . 5 $/\$
27	19, 26	addcld 7891	. . . 4 $/\$
28	27, 10, 15	adddid 7896	. . 3 $/\$
29	1	oveq2i 5832	. . . . . . . . 9
30		expp1 10419	. . . . . . . . . 10 $/\$
31	10, 4, 30	sylancl 410	. . . . . . . . 9 $/\$
32	29, 31	syl5req 2203	. . . . . . . 8 $/\$
33	13	a1i 9	. . . . . . . . . 10 $/\$
34	33, 16, 10	mulassd 7895	. . . . . . . . 9 $/\$
35	14, 15, 10	mul32d 8022	. . . . . . . . . . 11 $/\$
36		df-3 8887	. . . . . . . . . . . . . 14
37	36	oveq2i 5832	. . . . . . . . . . . . 13
38		2nn0 9101	. . . . . . . . . . . . . 14
39		expp1 10419	. . . . . . . . . . . . . 14 $/\$
40	10, 38, 39	sylancl 410	. . . . . . . . . . . . 13 $/\$
41	37, 40	syl5req 2203	. . . . . . . . . . . 12 $/\$
42	41	oveq1d 5836	. . . . . . . . . . 11 $/\$
43	35, 42	eqtrd 2190	. . . . . . . . . 10 $/\$
44	43	oveq2d 5837	. . . . . . . . 9 $/\$
45	34, 44	eqtrd 2190	. . . . . . . 8 $/\$
46	32, 45	oveq12d 5839	. . . . . . 7 $/\$
47	12, 10, 18, 46	joinlmuladdmuld 7899	. . . . . 6 $/\$
48	33, 21, 10	mulassd 7895	. . . . . . . . 9 $/\$
49	10, 20, 10	mul32d 8022	. . . . . . . . . . 11 $/\$
50	10	sqvald 10541	. . . . . . . . . . . 12 $/\$
51	50	oveq1d 5836	. . . . . . . . . . 11 $/\$
52	49, 51	eqtr4d 2193	. . . . . . . . . 10 $/\$
53	52	oveq2d 5837	. . . . . . . . 9 $/\$
54	48, 53	eqtrd 2190	. . . . . . . 8 $/\$
55	25, 10	mulcomd 7893	. . . . . . . 8 $/\$
56	54, 55	oveq12d 5839	. . . . . . 7 $/\$
57	23, 10, 25, 56	joinlmuladdmuld 7899	. . . . . 6 $/\$
58	47, 57	oveq12d 5839	. . . . 5 $/\$
59	19, 10, 26, 58	joinlmuladdmuld 7899	. . . 4 $/\$
60	19, 26, 15	adddird 7897	. . . . 5 $/\$
61	33, 16, 15	mulassd 7895	. . . . . . . . 9 $/\$
62	14, 15, 15	mulassd 7895	. . . . . . . . . . 11 $/\$
63	15	sqvald 10541	. . . . . . . . . . . 12 $/\$
64	63	oveq2d 5837	. . . . . . . . . . 11 $/\$
65	62, 64	eqtr4d 2193	. . . . . . . . . 10 $/\$
66	65	oveq2d 5837	. . . . . . . . 9 $/\$
67	61, 66	eqtrd 2190	. . . . . . . 8 $/\$
68	67	oveq2d 5837	. . . . . . 7 $/\$
69	12, 15, 18, 68	joinlmuladdmuld 7899	. . . . . 6 $/\$
70	33, 21, 15	mulassd 7895	. . . . . . . . 9 $/\$
71	10, 20, 15	mulassd 7895	. . . . . . . . . . 11 $/\$
72	36	oveq2i 5832	. . . . . . . . . . . . 13
73		expp1 10419	. . . . . . . . . . . . . 14 $/\$
74	15, 38, 73	sylancl 410	. . . . . . . . . . . . 13 $/\$
75	72, 74	syl5req 2203	. . . . . . . . . . . 12 $/\$
76	75	oveq2d 5837	. . . . . . . . . . 11 $/\$
77	71, 76	eqtrd 2190	. . . . . . . . . 10 $/\$
78	77	oveq2d 5837	. . . . . . . . 9 $/\$
79	70, 78	eqtrd 2190	. . . . . . . 8 $/\$
80	1	oveq2i 5832	. . . . . . . . 9
81		expp1 10419	. . . . . . . . . 10 $/\$
82	15, 4, 81	sylancl 410	. . . . . . . . 9 $/\$
83	80, 82	syl5req 2203	. . . . . . . 8 $/\$
84	79, 83	oveq12d 5839	. . . . . . 7 $/\$
85	23, 15, 25, 84	joinlmuladdmuld 7899	. . . . . 6 $/\$
86	69, 85	oveq12d 5839	. . . . 5 $/\$
87	12, 15	mulcld 7892	. . . . . 6 $/\$
88	14, 20	mulcld 7892	. . . . . . 7 $/\$
89		mulcl 7853	. . . . . . 7 $/\$
90	13, 88, 89	sylancr 411	. . . . . 6 $/\$
91	10, 25	mulcld 7892	. . . . . . . 8 $/\$
92		mulcl 7853	. . . . . . . 8 $/\$
93	13, 91, 92	sylancr 411	. . . . . . 7 $/\$
94		4nn0 9103	. . . . . . . 8
95		expcl 10430	. . . . . . . 8 $/\$
96	15, 94, 95	sylancl 410	. . . . . . 7 $/\$
97	93, 96	addcld 7891	. . . . . 6 $/\$
98	87, 90, 97	addassd 7894	. . . . 5 $/\$
99	60, 86, 98	3eqtrd 2194	. . . 4 $/\$
100	59, 99	oveq12d 5839	. . 3 $/\$
101		expcl 10430	. . . . . . 7 $/\$
102	10, 94, 101	sylancl 410	. . . . . 6 $/\$
103		mulcl 7853	. . . . . . 7 $/\$
104	13, 87, 103	sylancr 411	. . . . . 6 $/\$
105	102, 104	addcld 7891	. . . . 5 $/\$
106	90, 91	addcld 7891	. . . . 5 $/\$
107	90, 97	addcld 7891	. . . . 5 $/\$
108	105, 106, 87, 107	add4d 8038	. . . 4 $/\$
109	102, 104, 87	addassd 7894	. . . . . 6 $/\$
110	1	oveq1i 5831	. . . . . . . . 9
111		ax-1cn 7819	. . . . . . . . . . 11
112	111	a1i 9	. . . . . . . . . 10 $/\$
113	33, 112, 87	adddird 7897	. . . . . . . . 9 $/\$
114	110, 113	syl5eq 2202	. . . . . . . 8 $/\$
115	87	mulid2d 7890	. . . . . . . . 9 $/\$
116	115	oveq2d 5837	. . . . . . . 8 $/\$
117	114, 116	eqtrd 2190	. . . . . . 7 $/\$
118	117	oveq2d 5837	. . . . . 6 $/\$
119	109, 118	eqtr4d 2193	. . . . 5 $/\$
120	90, 91, 90, 97	add4d 8038	. . . . . 6 $/\$
121		3p3e6 8969	. . . . . . . . 9
122	121	oveq1i 5831	. . . . . . . 8
123	33, 33, 88	adddird 7897	. . . . . . . 8 $/\$
124	122, 123	eqtr3id 2204	. . . . . . 7 $/\$
125		3p1e4 8962	. . . . . . . . . . . . 13
126	13, 111, 125	addcomli 8014	. . . . . . . . . . . 12
127	126	oveq1i 5831	. . . . . . . . . . 11
128	112, 33, 91	adddird 7897	. . . . . . . . . . 11 $/\$
129	127, 128	eqtr3id 2204	. . . . . . . . . 10 $/\$
130	91	mulid2d 7890	. . . . . . . . . . 11 $/\$
131	130	oveq1d 5836	. . . . . . . . . 10 $/\$
132	129, 131	eqtrd 2190	. . . . . . . . 9 $/\$
133	132	oveq1d 5836	. . . . . . . 8 $/\$
134	91, 93, 96	addassd 7894	. . . . . . . 8 $/\$
135	133, 134	eqtrd 2190	. . . . . . 7 $/\$
136	124, 135	oveq12d 5839	. . . . . 6 $/\$
137	120, 136	eqtr4d 2193	. . . . 5 $/\$
138	119, 137	oveq12d 5839	. . . 4 $/\$
139	108, 138	eqtrd 2190	. . 3 $/\$
140	28, 100, 139	3eqtrd 2194	. 2 $/\$
141	7, 9, 140	3eqtrd 2194	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wceq 1335

wcel 2128 (class class class)co 5821

cc 7724

c1 7727

caddc 7729

cmul 7731

c2 8878

c3 8879

c4 8880

c6 8882

cn0 9084

cexp 10411

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4079 ax-sep 4082 ax-nul 4090 ax-pow 4135 ax-pr 4169 ax-un 4393 ax-setind 4495 ax-iinf 4546 ax-cnex 7817 ax-resscn 7818 ax-1cn 7819 ax-1re 7820 ax-icn 7821 ax-addcl 7822 ax-addrcl 7823 ax-mulcl 7824 ax-mulrcl 7825 ax-addcom 7826 ax-mulcom 7827 ax-addass 7828 ax-mulass 7829 ax-distr 7830 ax-i2m1 7831 ax-0lt1 7832 ax-1rid 7833 ax-0id 7834 ax-rnegex 7835 ax-precex 7836 ax-cnre 7837 ax-pre-ltirr 7838 ax-pre-ltwlin 7839 ax-pre-lttrn 7840 ax-pre-apti 7841 ax-pre-ltadd 7842 ax-pre-mulgt0 7843 ax-pre-mulext 7844

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3773 df-int 3808 df-iun 3851 df-br 3966 df-opab 4026 df-mpt 4027 df-tr 4063 df-id 4253 df-po 4256 df-iso 4257 df-iord 4326 df-on 4328 df-ilim 4329 df-suc 4331 df-iom 4549 df-xp 4591 df-rel 4592 df-cnv 4593 df-co 4594 df-dm 4595 df-rn 4596 df-res 4597 df-ima 4598 df-iota 5134 df-fun 5171 df-fn 5172 df-f 5173 df-f1 5174 df-fo 5175 df-f1o 5176 df-fv 5177 df-riota 5777 df-ov 5824 df-oprab 5825 df-mpo 5826 df-1st 6085 df-2nd 6086 df-recs 6249 df-frec 6335 df-pnf 7908 df-mnf 7909 df-xr 7910 df-ltxr 7911 df-le 7912 df-sub 8042 df-neg 8043 df-reap 8444 df-ap 8451 df-div 8540 df-inn 8828 df-2 8886 df-3 8887 df-4 8888 df-5 8889 df-6 8890 df-n0 9085 df-z 9162 df-uz 9434 df-seqfrec 10338 df-exp 10412

This theorem is referenced by: (None)

W3C validator