bcval5 - Intuitionistic Logic Explorer

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

Theorem bcval5 11088

Description: Write out the top and bottom parts of the binomial coefficient

explicitly. In this form, it is valid even for

, although it is no longer valid for nonpositive

. (Contributed by Mario Carneiro, 22-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.)

**Assertion**
Ref	Expression
bcval5	$/\$

Proof of Theorem bcval5 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bcval2 11075	. . . 4
2	1	adantl 277	. . 3 $/\$ $/\$
3		simprl 531	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
4		simprr 533	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
5	3, 4	mulcld 8259	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
6		simpr1 1030	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simpr2 1031	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simpr3 1032	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9	6, 7, 8	mulassd 8262	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	nn0zd 9661	. . . . . . . . . . . 12 $/\$ $/\$
12		simplr 529	. . . . . . . . . . . . 13 $/\$ $/\$
13	12	nnzd 9662	. . . . . . . . . . . 12 $/\$ $/\$
14	11, 13	zsubcld 9668	. . . . . . . . . . 11 $/\$ $/\$
15	14	peano2zd 9666	. . . . . . . . . 10 $/\$ $/\$
16		1red 8254	. . . . . . . . . . . 12 $/\$ $/\$
17	12	nnred 9215	. . . . . . . . . . . 12 $/\$ $/\$
18	10	nn0red 9517	. . . . . . . . . . . 12 $/\$ $/\$
19	12	nnge1d 9245	. . . . . . . . . . . 12 $/\$ $/\$
20	16, 17, 18, 19	lesub2dd 8801	. . . . . . . . . . 11 $/\$ $/\$
21	14	zred 9663	. . . . . . . . . . . 12 $/\$ $/\$
22		leaddsub 8677	. . . . . . . . . . . 12 $/\$ $/\$
23	21, 16, 18, 22	syl3anc 1274	. . . . . . . . . . 11 $/\$ $/\$
24	20, 23	mpbird 167	. . . . . . . . . 10 $/\$ $/\$
25		eluz2 9822	. . . . . . . . . 10 $/\$ $/\$
26	15, 11, 24, 25	syl3anbrc 1208	. . . . . . . . 9 $/\$ $/\$
27	26	adantrr 479	. . . . . . . 8 $/\$ $/\$ $/\$
28		simprr 533	. . . . . . . . 9 $/\$ $/\$ $/\$
29		nnuz 9853	. . . . . . . . 9
30	28, 29	eleqtrdi 2324	. . . . . . . 8 $/\$ $/\$ $/\$
31		fvi 5712	. . . . . . . . . 10
32	31	elv 2807	. . . . . . . . 9
33		eluzelcn 9828	. . . . . . . . . 10
34	33	adantl 277	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	32, 34	eqeltrid 2318	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
36	5, 9, 27, 30, 35	seq3split 10813	. . . . . . 7 $/\$ $/\$ $/\$
37		elfzuz3 10319	. . . . . . . . . . 11
38	37	adantl 277	. . . . . . . . . 10 $/\$ $/\$
39		eluznn 9895	. . . . . . . . . 10 $/\$
40	12, 38, 39	syl2anc 411	. . . . . . . . 9 $/\$ $/\$
41	40	adantrr 479	. . . . . . . 8 $/\$ $/\$ $/\$
42		facnn 11052	. . . . . . . 8
43	41, 42	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
44		facnn 11052	. . . . . . . . 9
45	28, 44	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
46	45	oveq1d 6043	. . . . . . 7 $/\$ $/\$ $/\$
47	36, 43, 46	3eqtr4d 2274	. . . . . 6 $/\$ $/\$ $/\$
48	47	expr 375	. . . . 5 $/\$ $/\$
49	10	faccld 11061	. . . . . . . . 9 $/\$ $/\$
50	49	nncnd 9216	. . . . . . . 8 $/\$ $/\$
51	50	mullidd 8257	. . . . . . 7 $/\$ $/\$
52	40, 42	syl 14	. . . . . . . 8 $/\$ $/\$
53	52	oveq2d 6044	. . . . . . 7 $/\$ $/\$
54	51, 53	eqtr3d 2266	. . . . . 6 $/\$ $/\$
55		fveq2 5648	. . . . . . . . 9
56		fac0 11053	. . . . . . . . 9
57	55, 56	eqtrdi 2280	. . . . . . . 8
58		oveq1 6035	. . . . . . . . . . 11
59		0p1e1 9316	. . . . . . . . . . 11
60	58, 59	eqtrdi 2280	. . . . . . . . . 10
61	60	seqeq1d 10778	. . . . . . . . 9
62	61	fveq1d 5650	. . . . . . . 8
63	57, 62	oveq12d 6046	. . . . . . 7
64	63	eqeq2d 2243	. . . . . 6
65	54, 64	syl5ibrcom 157	. . . . 5 $/\$ $/\$
66		fznn0sub 10354	. . . . . . 7
67	66	adantl 277	. . . . . 6 $/\$ $/\$
68		elnn0 9463	. . . . . 6 $\/$
69	67, 68	sylib 122	. . . . 5 $/\$ $/\$ $\/$
70	48, 65, 69	mpjaod 726	. . . 4 $/\$ $/\$
71	70	oveq1d 6043	. . 3 $/\$ $/\$
72		eqid 2231	. . . . . 6
73		fvi 5712	. . . . . . . 8
74	73	elv 2807	. . . . . . 7
75		eluzelcn 9828	. . . . . . . 8
76	75	adantl 277	. . . . . . 7 $/\$ $/\$ $/\$
77	74, 76	eqeltrid 2318	. . . . . 6 $/\$ $/\$ $/\$
78		mulcl 8219	. . . . . . 7 $/\$
79	78	adantl 277	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80	72, 15, 77, 79	seqf 10789	. . . . 5 $/\$ $/\$
81	80, 26	ffvelcdmd 5791	. . . 4 $/\$ $/\$
82	12	nnnn0d 9516	. . . . . 6 $/\$ $/\$
83	82	faccld 11061	. . . . 5 $/\$ $/\$
84	83	nncnd 9216	. . . 4 $/\$ $/\$
85	67	faccld 11061	. . . . 5 $/\$ $/\$
86	85	nncnd 9216	. . . 4 $/\$ $/\$
87	83	nnap0d 9248	. . . 4 $/\$ $/\$ #
88	85	nnap0d 9248	. . . 4 $/\$ $/\$ #
89	81, 84, 86, 87, 88	divcanap5d 9056	. . 3 $/\$ $/\$
90	2, 71, 89	3eqtrd 2268	. 2 $/\$ $/\$
91		simplr 529	. . . . . . 7 $/\$ $/\$
92	91	nnnn0d 9516	. . . . . 6 $/\$ $/\$
93	92	faccld 11061	. . . . 5 $/\$ $/\$
94	93	nncnd 9216	. . . 4 $/\$ $/\$
95	93	nnap0d 9248	. . . 4 $/\$ $/\$ #
96	94, 95	div0apd 9026	. . 3 $/\$ $/\$
97		mulcl 8219	. . . . . 6 $/\$
98	97	adantl 277	. . . . 5 $/\$ $/\$ $/\$ $/\$
99		eluzelcn 9828	. . . . . . 7
100	99	adantl 277	. . . . . 6 $/\$ $/\$ $/\$
101	32, 100	eqeltrid 2318	. . . . 5 $/\$ $/\$ $/\$
102		simpr 110	. . . . . 6 $/\$ $/\$ $/\$
103	102	mul02d 8630	. . . . 5 $/\$ $/\$ $/\$
104	102	mul01d 8631	. . . . 5 $/\$ $/\$ $/\$
105		simpr 110	. . . . . . . . 9 $/\$ $/\$
106		nn0uz 9852	. . . . . . . . . . . 12
107	92, 106	eleqtrdi 2324	. . . . . . . . . . 11 $/\$ $/\$
108		simpll 527	. . . . . . . . . . . 12 $/\$ $/\$
109	108	nn0zd 9661	. . . . . . . . . . 11 $/\$ $/\$
110		elfz5 10314	. . . . . . . . . . 11 $/\$
111	107, 109, 110	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$
112		nn0re 9470	. . . . . . . . . . . 12
113	112	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$
114		nnre 9209	. . . . . . . . . . . 12
115	114	ad2antlr 489	. . . . . . . . . . 11 $/\$ $/\$
116	113, 115	subge0d 8774	. . . . . . . . . 10 $/\$ $/\$
117	111, 116	bitr4d 191	. . . . . . . . 9 $/\$ $/\$
118	105, 117	mtbid 679	. . . . . . . 8 $/\$ $/\$
119		simpl 109	. . . . . . . . . . . 12 $/\$
120	119	nn0zd 9661	. . . . . . . . . . 11 $/\$
121		simpr 110	. . . . . . . . . . . 12 $/\$
122	121	nnzd 9662	. . . . . . . . . . 11 $/\$
123	120, 122	zsubcld 9668	. . . . . . . . . 10 $/\$
124	123	adantr 276	. . . . . . . . 9 $/\$ $/\$
125		0z 9551	. . . . . . . . 9
126		zltnle 9586	. . . . . . . . 9 $/\$
127	124, 125, 126	sylancl 413	. . . . . . . 8 $/\$ $/\$
128	118, 127	mpbird 167	. . . . . . 7 $/\$ $/\$
129		zltp1le 9595	. . . . . . . 8 $/\$
130	124, 125, 129	sylancl 413	. . . . . . 7 $/\$ $/\$
131	128, 130	mpbid 147	. . . . . 6 $/\$ $/\$
132		nn0ge0 9486	. . . . . . 7
133	132	ad2antrr 488	. . . . . 6 $/\$ $/\$
134		0zd 9552	. . . . . . 7 $/\$ $/\$
135	124	peano2zd 9666	. . . . . . 7 $/\$ $/\$
136		elfz 10311	. . . . . . 7 $/\$ $/\$ $/\$
137	134, 135, 109, 136	syl3anc 1274	. . . . . 6 $/\$ $/\$ $/\$
138	131, 133, 137	mpbir2and 953	. . . . 5 $/\$ $/\$
139		0cn 8231	. . . . . 6
140		fvi 5712	. . . . . 6
141	139, 140	mp1i 10	. . . . 5 $/\$ $/\$
142	98, 101, 103, 104, 138, 141	seq3z 10853	. . . 4 $/\$ $/\$
143	142	oveq1d 6043	. . 3 $/\$ $/\$
144		nnz 9559	. . . . 5
145		bcval3 11076	. . . . 5 $/\$ $/\$
146	144, 145	syl3an2 1308	. . . 4 $/\$ $/\$
147	146	3expa 1230	. . 3 $/\$ $/\$
148	96, 143, 147	3eqtr4rd 2275	. 2 $/\$ $/\$
149		0zd 9552	. . . 4 $/\$
150		fzdcel 10337	. . . 4 $/\$ $/\$ DECID
151	122, 149, 120, 150	syl3anc 1274	. . 3 $/\$ DECID
152		exmiddc 844	. . 3 DECID $\/$
153	151, 152	syl 14	. 2 $/\$ $\/$
154	90, 148, 153	mpjaodan 806	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 716 DECID wdc 842 $/\$ w3a 1005

wceq 1398

wcel 2202

cvv 2803 class class class wbr 4093

cid 4391

cfv 5333 (class class class)co 6028

cc 8090

cr 8091

cc0 8092

c1 8093

caddc 8095

cmul 8097

clt 8273

cle 8274

cmin 8409

cdiv 8911

cn 9202

cn0 9461

cz 9540

cuz 9816

cfz 10305

cseq 10772

cfa 11050

cbc 11072

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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-coll 4209 ax-sep 4212 ax-nul 4220 ax-pow 4270 ax-pr 4305 ax-un 4536 ax-setind 4641 ax-iinf 4692 ax-cnex 8183 ax-resscn 8184 ax-1cn 8185 ax-1re 8186 ax-icn 8187 ax-addcl 8188 ax-addrcl 8189 ax-mulcl 8190 ax-mulrcl 8191 ax-addcom 8192 ax-mulcom 8193 ax-addass 8194 ax-mulass 8195 ax-distr 8196 ax-i2m1 8197 ax-0lt1 8198 ax-1rid 8199 ax-0id 8200 ax-rnegex 8201 ax-precex 8202 ax-cnre 8203 ax-pre-ltirr 8204 ax-pre-ltwlin 8205 ax-pre-lttrn 8206 ax-pre-apti 8207 ax-pre-ltadd 8208 ax-pre-mulgt0 8209 ax-pre-mulext 8210

This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ne 2404 df-nel 2499 df-ral 2516 df-rex 2517 df-reu 2518 df-rmo 2519 df-rab 2520 df-v 2805 df-sbc 3033 df-csb 3129 df-dif 3203 df-un 3205 df-in 3207 df-ss 3214 df-nul 3497 df-if 3608 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-int 3934 df-iun 3977 df-br 4094 df-opab 4156 df-mpt 4157 df-tr 4193 df-id 4396 df-po 4399 df-iso 4400 df-iord 4469 df-on 4471 df-ilim 4472 df-suc 4474 df-iom 4695 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-res 4743 df-ima 4744 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-f1 5338 df-fo 5339 df-f1o 5340 df-fv 5341 df-riota 5981 df-ov 6031 df-oprab 6032 df-mpo 6033 df-1st 6312 df-2nd 6313 df-recs 6514 df-frec 6600 df-pnf 8275 df-mnf 8276 df-xr 8277 df-ltxr 8278 df-le 8279 df-sub 8411 df-neg 8412 df-reap 8814 df-ap 8821 df-div 8912 df-inn 9203 df-n0 9462 df-z 9541 df-uz 9817 df-q 9915 df-fz 10306 df-seqfrec 10773 df-fac 11051 df-bc 11073

This theorem is referenced by: bcn2 11089

W3C validator