binom4 - Intuitionistic Logic Explorer

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

Theorem binom4 15111

Description: Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11627, 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 9043	. . . 4
2	1	oveq2i 5929	. . 3
3		addcl 7997	. . . 4 $/\$
4		3nn0 9258	. . . 4
5		expp1 10617	. . . 4 $/\$
6	3, 4, 5	sylancl 413	. . 3 $/\$
7	2, 6	eqtrid 2238	. 2 $/\$
8		binom3 10728	. . 3 $/\$
9	8	oveq1d 5933	. 2 $/\$
10		simpl 109	. . . . . . 7 $/\$
11		expcl 10628	. . . . . . 7 $/\$
12	10, 4, 11	sylancl 413	. . . . . 6 $/\$
13		3cn 9057	. . . . . . 7
14	10	sqcld 10742	. . . . . . . 8 $/\$
15		simpr 110	. . . . . . . 8 $/\$
16	14, 15	mulcld 8040	. . . . . . 7 $/\$
17		mulcl 7999	. . . . . . 7 $/\$
18	13, 16, 17	sylancr 414	. . . . . 6 $/\$
19	12, 18	addcld 8039	. . . . 5 $/\$
20	15	sqcld 10742	. . . . . . . 8 $/\$
21	10, 20	mulcld 8040	. . . . . . 7 $/\$
22		mulcl 7999	. . . . . . 7 $/\$
23	13, 21, 22	sylancr 414	. . . . . 6 $/\$
24		expcl 10628	. . . . . . 7 $/\$
25	15, 4, 24	sylancl 413	. . . . . 6 $/\$
26	23, 25	addcld 8039	. . . . 5 $/\$
27	19, 26	addcld 8039	. . . 4 $/\$
28	27, 10, 15	adddid 8044	. . 3 $/\$
29	1	oveq2i 5929	. . . . . . . . 9
30		expp1 10617	. . . . . . . . . 10 $/\$
31	10, 4, 30	sylancl 413	. . . . . . . . 9 $/\$
32	29, 31	eqtr2id 2239	. . . . . . . 8 $/\$
33	13	a1i 9	. . . . . . . . . 10 $/\$
34	33, 16, 10	mulassd 8043	. . . . . . . . 9 $/\$
35	14, 15, 10	mul32d 8172	. . . . . . . . . . 11 $/\$
36		df-3 9042	. . . . . . . . . . . . . 14
37	36	oveq2i 5929	. . . . . . . . . . . . 13
38		2nn0 9257	. . . . . . . . . . . . . 14
39		expp1 10617	. . . . . . . . . . . . . 14 $/\$
40	10, 38, 39	sylancl 413	. . . . . . . . . . . . 13 $/\$
41	37, 40	eqtr2id 2239	. . . . . . . . . . . 12 $/\$
42	41	oveq1d 5933	. . . . . . . . . . 11 $/\$
43	35, 42	eqtrd 2226	. . . . . . . . . 10 $/\$
44	43	oveq2d 5934	. . . . . . . . 9 $/\$
45	34, 44	eqtrd 2226	. . . . . . . 8 $/\$
46	32, 45	oveq12d 5936	. . . . . . 7 $/\$
47	12, 10, 18, 46	joinlmuladdmuld 8047	. . . . . 6 $/\$
48	33, 21, 10	mulassd 8043	. . . . . . . . 9 $/\$
49	10, 20, 10	mul32d 8172	. . . . . . . . . . 11 $/\$
50	10	sqvald 10741	. . . . . . . . . . . 12 $/\$
51	50	oveq1d 5933	. . . . . . . . . . 11 $/\$
52	49, 51	eqtr4d 2229	. . . . . . . . . 10 $/\$
53	52	oveq2d 5934	. . . . . . . . 9 $/\$
54	48, 53	eqtrd 2226	. . . . . . . 8 $/\$
55	25, 10	mulcomd 8041	. . . . . . . 8 $/\$
56	54, 55	oveq12d 5936	. . . . . . 7 $/\$
57	23, 10, 25, 56	joinlmuladdmuld 8047	. . . . . 6 $/\$
58	47, 57	oveq12d 5936	. . . . 5 $/\$
59	19, 10, 26, 58	joinlmuladdmuld 8047	. . . 4 $/\$
60	19, 26, 15	adddird 8045	. . . . 5 $/\$
61	33, 16, 15	mulassd 8043	. . . . . . . . 9 $/\$
62	14, 15, 15	mulassd 8043	. . . . . . . . . . 11 $/\$
63	15	sqvald 10741	. . . . . . . . . . . 12 $/\$
64	63	oveq2d 5934	. . . . . . . . . . 11 $/\$
65	62, 64	eqtr4d 2229	. . . . . . . . . 10 $/\$
66	65	oveq2d 5934	. . . . . . . . 9 $/\$
67	61, 66	eqtrd 2226	. . . . . . . 8 $/\$
68	67	oveq2d 5934	. . . . . . 7 $/\$
69	12, 15, 18, 68	joinlmuladdmuld 8047	. . . . . 6 $/\$
70	33, 21, 15	mulassd 8043	. . . . . . . . 9 $/\$
71	10, 20, 15	mulassd 8043	. . . . . . . . . . 11 $/\$
72	36	oveq2i 5929	. . . . . . . . . . . . 13
73		expp1 10617	. . . . . . . . . . . . . 14 $/\$
74	15, 38, 73	sylancl 413	. . . . . . . . . . . . 13 $/\$
75	72, 74	eqtr2id 2239	. . . . . . . . . . . 12 $/\$
76	75	oveq2d 5934	. . . . . . . . . . 11 $/\$
77	71, 76	eqtrd 2226	. . . . . . . . . 10 $/\$
78	77	oveq2d 5934	. . . . . . . . 9 $/\$
79	70, 78	eqtrd 2226	. . . . . . . 8 $/\$
80	1	oveq2i 5929	. . . . . . . . 9
81		expp1 10617	. . . . . . . . . 10 $/\$
82	15, 4, 81	sylancl 413	. . . . . . . . 9 $/\$
83	80, 82	eqtr2id 2239	. . . . . . . 8 $/\$
84	79, 83	oveq12d 5936	. . . . . . 7 $/\$
85	23, 15, 25, 84	joinlmuladdmuld 8047	. . . . . 6 $/\$
86	69, 85	oveq12d 5936	. . . . 5 $/\$
87	12, 15	mulcld 8040	. . . . . 6 $/\$
88	14, 20	mulcld 8040	. . . . . . 7 $/\$
89		mulcl 7999	. . . . . . 7 $/\$
90	13, 88, 89	sylancr 414	. . . . . 6 $/\$
91	10, 25	mulcld 8040	. . . . . . . 8 $/\$
92		mulcl 7999	. . . . . . . 8 $/\$
93	13, 91, 92	sylancr 414	. . . . . . 7 $/\$
94		4nn0 9259	. . . . . . . 8
95		expcl 10628	. . . . . . . 8 $/\$
96	15, 94, 95	sylancl 413	. . . . . . 7 $/\$
97	93, 96	addcld 8039	. . . . . 6 $/\$
98	87, 90, 97	addassd 8042	. . . . 5 $/\$
99	60, 86, 98	3eqtrd 2230	. . . 4 $/\$
100	59, 99	oveq12d 5936	. . 3 $/\$
101		expcl 10628	. . . . . . 7 $/\$
102	10, 94, 101	sylancl 413	. . . . . 6 $/\$
103		mulcl 7999	. . . . . . 7 $/\$
104	13, 87, 103	sylancr 414	. . . . . 6 $/\$
105	102, 104	addcld 8039	. . . . 5 $/\$
106	90, 91	addcld 8039	. . . . 5 $/\$
107	90, 97	addcld 8039	. . . . 5 $/\$
108	105, 106, 87, 107	add4d 8188	. . . 4 $/\$
109	102, 104, 87	addassd 8042	. . . . . 6 $/\$
110	1	oveq1i 5928	. . . . . . . . 9
111		ax-1cn 7965	. . . . . . . . . . 11
112	111	a1i 9	. . . . . . . . . 10 $/\$
113	33, 112, 87	adddird 8045	. . . . . . . . 9 $/\$
114	110, 113	eqtrid 2238	. . . . . . . 8 $/\$
115	87	mulid2d 8038	. . . . . . . . 9 $/\$
116	115	oveq2d 5934	. . . . . . . 8 $/\$
117	114, 116	eqtrd 2226	. . . . . . 7 $/\$
118	117	oveq2d 5934	. . . . . 6 $/\$
119	109, 118	eqtr4d 2229	. . . . 5 $/\$
120	90, 91, 90, 97	add4d 8188	. . . . . 6 $/\$
121		3p3e6 9124	. . . . . . . . 9
122	121	oveq1i 5928	. . . . . . . 8
123	33, 33, 88	adddird 8045	. . . . . . . 8 $/\$
124	122, 123	eqtr3id 2240	. . . . . . 7 $/\$
125		3p1e4 9117	. . . . . . . . . . . . 13
126	13, 111, 125	addcomli 8164	. . . . . . . . . . . 12
127	126	oveq1i 5928	. . . . . . . . . . 11
128	112, 33, 91	adddird 8045	. . . . . . . . . . 11 $/\$
129	127, 128	eqtr3id 2240	. . . . . . . . . 10 $/\$
130	91	mulid2d 8038	. . . . . . . . . . 11 $/\$
131	130	oveq1d 5933	. . . . . . . . . 10 $/\$
132	129, 131	eqtrd 2226	. . . . . . . . 9 $/\$
133	132	oveq1d 5933	. . . . . . . 8 $/\$
134	91, 93, 96	addassd 8042	. . . . . . . 8 $/\$
135	133, 134	eqtrd 2226	. . . . . . 7 $/\$
136	124, 135	oveq12d 5936	. . . . . 6 $/\$
137	120, 136	eqtr4d 2229	. . . . 5 $/\$
138	119, 137	oveq12d 5936	. . . 4 $/\$
139	108, 138	eqtrd 2226	. . 3 $/\$
140	28, 100, 139	3eqtrd 2230	. 2 $/\$
141	7, 9, 140	3eqtrd 2230	1 $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wceq 1364

wcel 2164 (class class class)co 5918

cc 7870

c1 7873

caddc 7875

cmul 7877

c2 9033

c3 9034

c4 9035

c6 9037

cn0 9240

cexp 10609

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-coll 4144 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-iinf 4620 ax-cnex 7963 ax-resscn 7964 ax-1cn 7965 ax-1re 7966 ax-icn 7967 ax-addcl 7968 ax-addrcl 7969 ax-mulcl 7970 ax-mulrcl 7971 ax-addcom 7972 ax-mulcom 7973 ax-addass 7974 ax-mulass 7975 ax-distr 7976 ax-i2m1 7977 ax-0lt1 7978 ax-1rid 7979 ax-0id 7980 ax-rnegex 7981 ax-precex 7982 ax-cnre 7983 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986 ax-pre-apti 7987 ax-pre-ltadd 7988 ax-pre-mulgt0 7989 ax-pre-mulext 7990

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rmo 2480 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-po 4327 df-iso 4328 df-iord 4397 df-on 4399 df-ilim 4400 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-rn 4670 df-res 4671 df-ima 4672 df-iota 5215 df-fun 5256 df-fn 5257 df-f 5258 df-f1 5259 df-fo 5260 df-f1o 5261 df-fv 5262 df-riota 5873 df-ov 5921 df-oprab 5922 df-mpo 5923 df-1st 6193 df-2nd 6194 df-recs 6358 df-frec 6444 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059 df-le 8060 df-sub 8192 df-neg 8193 df-reap 8594 df-ap 8601 df-div 8692 df-inn 8983 df-2 9041 df-3 9042 df-4 9043 df-5 9044 df-6 9045 df-n0 9241 df-z 9318 df-uz 9593 df-seqfrec 10519 df-exp 10610

This theorem is referenced by: (None)

W3C validator