bcval5 - Intuitionistic Logic Explorer

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

Theorem bcval5 10743

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 10730	. . . 4
2	1	adantl 277	. . 3 $/\$ $/\$
3		simprl 529	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
4		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
5	3, 4	mulcld 7978	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
6		simpr1 1003	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simpr2 1004	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simpr3 1005	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9	6, 7, 8	mulassd 7981	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpll 527	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	nn0zd 9373	. . . . . . . . . . . 12 $/\$ $/\$
12		simplr 528	. . . . . . . . . . . . 13 $/\$ $/\$
13	12	nnzd 9374	. . . . . . . . . . . 12 $/\$ $/\$
14	11, 13	zsubcld 9380	. . . . . . . . . . 11 $/\$ $/\$
15	14	peano2zd 9378	. . . . . . . . . 10 $/\$ $/\$
16		1red 7972	. . . . . . . . . . . 12 $/\$ $/\$
17	12	nnred 8932	. . . . . . . . . . . 12 $/\$ $/\$
18	10	nn0red 9230	. . . . . . . . . . . 12 $/\$ $/\$
19	12	nnge1d 8962	. . . . . . . . . . . 12 $/\$ $/\$
20	16, 17, 18, 19	lesub2dd 8519	. . . . . . . . . . 11 $/\$ $/\$
21	14	zred 9375	. . . . . . . . . . . 12 $/\$ $/\$
22		leaddsub 8395	. . . . . . . . . . . 12 $/\$ $/\$
23	21, 16, 18, 22	syl3anc 1238	. . . . . . . . . . 11 $/\$ $/\$
24	20, 23	mpbird 167	. . . . . . . . . 10 $/\$ $/\$
25		eluz2 9534	. . . . . . . . . 10 $/\$ $/\$
26	15, 11, 24, 25	syl3anbrc 1181	. . . . . . . . 9 $/\$ $/\$
27	26	adantrr 479	. . . . . . . 8 $/\$ $/\$ $/\$
28		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$
29		nnuz 9563	. . . . . . . . 9
30	28, 29	eleqtrdi 2270	. . . . . . . 8 $/\$ $/\$ $/\$
31		fvi 5574	. . . . . . . . . 10
32	31	elv 2742	. . . . . . . . 9
33		eluzelcn 9539	. . . . . . . . . 10
34	33	adantl 277	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	32, 34	eqeltrid 2264	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
36	5, 9, 27, 30, 35	seq3split 10479	. . . . . . 7 $/\$ $/\$ $/\$
37		elfzuz3 10022	. . . . . . . . . . 11
38	37	adantl 277	. . . . . . . . . 10 $/\$ $/\$
39		eluznn 9600	. . . . . . . . . 10 $/\$
40	12, 38, 39	syl2anc 411	. . . . . . . . 9 $/\$ $/\$
41	40	adantrr 479	. . . . . . . 8 $/\$ $/\$ $/\$
42		facnn 10707	. . . . . . . 8
43	41, 42	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
44		facnn 10707	. . . . . . . . 9
45	28, 44	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
46	45	oveq1d 5890	. . . . . . 7 $/\$ $/\$ $/\$
47	36, 43, 46	3eqtr4d 2220	. . . . . 6 $/\$ $/\$ $/\$
48	47	expr 375	. . . . 5 $/\$ $/\$
49	10	faccld 10716	. . . . . . . . 9 $/\$ $/\$
50	49	nncnd 8933	. . . . . . . 8 $/\$ $/\$
51	50	mulid2d 7976	. . . . . . 7 $/\$ $/\$
52	40, 42	syl 14	. . . . . . . 8 $/\$ $/\$
53	52	oveq2d 5891	. . . . . . 7 $/\$ $/\$
54	51, 53	eqtr3d 2212	. . . . . 6 $/\$ $/\$
55		fveq2 5516	. . . . . . . . 9
56		fac0 10708	. . . . . . . . 9
57	55, 56	eqtrdi 2226	. . . . . . . 8
58		oveq1 5882	. . . . . . . . . . 11
59		0p1e1 9033	. . . . . . . . . . 11
60	58, 59	eqtrdi 2226	. . . . . . . . . 10
61	60	seqeq1d 10451	. . . . . . . . 9
62	61	fveq1d 5518	. . . . . . . 8
63	57, 62	oveq12d 5893	. . . . . . 7
64	63	eqeq2d 2189	. . . . . 6
65	54, 64	syl5ibrcom 157	. . . . 5 $/\$ $/\$
66		fznn0sub 10057	. . . . . . 7
67	66	adantl 277	. . . . . 6 $/\$ $/\$
68		elnn0 9178	. . . . . 6 $\/$
69	67, 68	sylib 122	. . . . 5 $/\$ $/\$ $\/$
70	48, 65, 69	mpjaod 718	. . . 4 $/\$ $/\$
71	70	oveq1d 5890	. . 3 $/\$ $/\$
72		eqid 2177	. . . . . 6
73		fvi 5574	. . . . . . . 8
74	73	elv 2742	. . . . . . 7
75		eluzelcn 9539	. . . . . . . 8
76	75	adantl 277	. . . . . . 7 $/\$ $/\$ $/\$
77	74, 76	eqeltrid 2264	. . . . . 6 $/\$ $/\$ $/\$
78		mulcl 7938	. . . . . . 7 $/\$
79	78	adantl 277	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80	72, 15, 77, 79	seqf 10461	. . . . 5 $/\$ $/\$
81	80, 26	ffvelcdmd 5653	. . . 4 $/\$ $/\$
82	12	nnnn0d 9229	. . . . . 6 $/\$ $/\$
83	82	faccld 10716	. . . . 5 $/\$ $/\$
84	83	nncnd 8933	. . . 4 $/\$ $/\$
85	67	faccld 10716	. . . . 5 $/\$ $/\$
86	85	nncnd 8933	. . . 4 $/\$ $/\$
87	83	nnap0d 8965	. . . 4 $/\$ $/\$ #
88	85	nnap0d 8965	. . . 4 $/\$ $/\$ #
89	81, 84, 86, 87, 88	divcanap5d 8774	. . 3 $/\$ $/\$
90	2, 71, 89	3eqtrd 2214	. 2 $/\$ $/\$
91		simplr 528	. . . . . . 7 $/\$ $/\$
92	91	nnnn0d 9229	. . . . . 6 $/\$ $/\$
93	92	faccld 10716	. . . . 5 $/\$ $/\$
94	93	nncnd 8933	. . . 4 $/\$ $/\$
95	93	nnap0d 8965	. . . 4 $/\$ $/\$ #
96	94, 95	div0apd 8744	. . 3 $/\$ $/\$
97		mulcl 7938	. . . . . 6 $/\$
98	97	adantl 277	. . . . 5 $/\$ $/\$ $/\$ $/\$
99		eluzelcn 9539	. . . . . . 7
100	99	adantl 277	. . . . . 6 $/\$ $/\$ $/\$
101	32, 100	eqeltrid 2264	. . . . 5 $/\$ $/\$ $/\$
102		simpr 110	. . . . . 6 $/\$ $/\$ $/\$
103	102	mul02d 8349	. . . . 5 $/\$ $/\$ $/\$
104	102	mul01d 8350	. . . . 5 $/\$ $/\$ $/\$
105		simpr 110	. . . . . . . . 9 $/\$ $/\$
106		nn0uz 9562	. . . . . . . . . . . 12
107	92, 106	eleqtrdi 2270	. . . . . . . . . . 11 $/\$ $/\$
108		simpll 527	. . . . . . . . . . . 12 $/\$ $/\$
109	108	nn0zd 9373	. . . . . . . . . . 11 $/\$ $/\$
110		elfz5 10017	. . . . . . . . . . 11 $/\$
111	107, 109, 110	syl2anc 411	. . . . . . . . . 10 $/\$ $/\$
112		nn0re 9185	. . . . . . . . . . . 12
113	112	ad2antrr 488	. . . . . . . . . . 11 $/\$ $/\$
114		nnre 8926	. . . . . . . . . . . 12
115	114	ad2antlr 489	. . . . . . . . . . 11 $/\$ $/\$
116	113, 115	subge0d 8492	. . . . . . . . . 10 $/\$ $/\$
117	111, 116	bitr4d 191	. . . . . . . . 9 $/\$ $/\$
118	105, 117	mtbid 672	. . . . . . . 8 $/\$ $/\$
119		simpl 109	. . . . . . . . . . . 12 $/\$
120	119	nn0zd 9373	. . . . . . . . . . 11 $/\$
121		simpr 110	. . . . . . . . . . . 12 $/\$
122	121	nnzd 9374	. . . . . . . . . . 11 $/\$
123	120, 122	zsubcld 9380	. . . . . . . . . 10 $/\$
124	123	adantr 276	. . . . . . . . 9 $/\$ $/\$
125		0z 9264	. . . . . . . . 9
126		zltnle 9299	. . . . . . . . 9 $/\$
127	124, 125, 126	sylancl 413	. . . . . . . 8 $/\$ $/\$
128	118, 127	mpbird 167	. . . . . . 7 $/\$ $/\$
129		zltp1le 9307	. . . . . . . 8 $/\$
130	124, 125, 129	sylancl 413	. . . . . . 7 $/\$ $/\$
131	128, 130	mpbid 147	. . . . . 6 $/\$ $/\$
132		nn0ge0 9201	. . . . . . 7
133	132	ad2antrr 488	. . . . . 6 $/\$ $/\$
134		0zd 9265	. . . . . . 7 $/\$ $/\$
135	124	peano2zd 9378	. . . . . . 7 $/\$ $/\$
136		elfz 10014	. . . . . . 7 $/\$ $/\$ $/\$
137	134, 135, 109, 136	syl3anc 1238	. . . . . 6 $/\$ $/\$ $/\$
138	131, 133, 137	mpbir2and 944	. . . . 5 $/\$ $/\$
139		0cn 7949	. . . . . 6
140		fvi 5574	. . . . . 6
141	139, 140	mp1i 10	. . . . 5 $/\$ $/\$
142	98, 101, 103, 104, 138, 141	seq3z 10511	. . . 4 $/\$ $/\$
143	142	oveq1d 5890	. . 3 $/\$ $/\$
144		nnz 9272	. . . . 5
145		bcval3 10731	. . . . 5 $/\$ $/\$
146	144, 145	syl3an2 1272	. . . 4 $/\$ $/\$
147	146	3expa 1203	. . 3 $/\$ $/\$
148	96, 143, 147	3eqtr4rd 2221	. 2 $/\$ $/\$
149		0zd 9265	. . . 4 $/\$
150		fzdcel 10040	. . . 4 $/\$ $/\$ DECID
151	122, 149, 120, 150	syl3anc 1238	. . 3 $/\$ DECID
152		exmiddc 836	. . 3 DECID $\/$
153	151, 152	syl 14	. 2 $/\$ $\/$
154	90, 148, 153	mpjaodan 798	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 708 DECID wdc 834 $/\$ w3a 978

wceq 1353

wcel 2148

cvv 2738 class class class wbr 4004

cid 4289

cfv 5217 (class class class)co 5875

cc 7809

cr 7810

cc0 7811

c1 7812

caddc 7814

cmul 7816

clt 7992

cle 7993

cmin 8128

cdiv 8629

cn 8919

cn0 9176

cz 9253

cuz 9528

cfz 10008

cseq 10445

cfa 10705

cbc 10727

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 614 ax-in2 615 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-13 2150 ax-14 2151 ax-ext 2159 ax-coll 4119 ax-sep 4122 ax-nul 4130 ax-pow 4175 ax-pr 4210 ax-un 4434 ax-setind 4537 ax-iinf 4588 ax-cnex 7902 ax-resscn 7903 ax-1cn 7904 ax-1re 7905 ax-icn 7906 ax-addcl 7907 ax-addrcl 7908 ax-mulcl 7909 ax-mulrcl 7910 ax-addcom 7911 ax-mulcom 7912 ax-addass 7913 ax-mulass 7914 ax-distr 7915 ax-i2m1 7916 ax-0lt1 7917 ax-1rid 7918 ax-0id 7919 ax-rnegex 7920 ax-precex 7921 ax-cnre 7922 ax-pre-ltirr 7923 ax-pre-ltwlin 7924 ax-pre-lttrn 7925 ax-pre-apti 7926 ax-pre-ltadd 7927 ax-pre-mulgt0 7928 ax-pre-mulext 7929

This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1461 df-sb 1763 df-eu 2029 df-mo 2030 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ne 2348 df-nel 2443 df-ral 2460 df-rex 2461 df-reu 2462 df-rmo 2463 df-rab 2464 df-v 2740 df-sbc 2964 df-csb 3059 df-dif 3132 df-un 3134 df-in 3136 df-ss 3143 df-nul 3424 df-if 3536 df-pw 3578 df-sn 3599 df-pr 3600 df-op 3602 df-uni 3811 df-int 3846 df-iun 3889 df-br 4005 df-opab 4066 df-mpt 4067 df-tr 4103 df-id 4294 df-po 4297 df-iso 4298 df-iord 4367 df-on 4369 df-ilim 4370 df-suc 4372 df-iom 4591 df-xp 4633 df-rel 4634 df-cnv 4635 df-co 4636 df-dm 4637 df-rn 4638 df-res 4639 df-ima 4640 df-iota 5179 df-fun 5219 df-fn 5220 df-f 5221 df-f1 5222 df-fo 5223 df-f1o 5224 df-fv 5225 df-riota 5831 df-ov 5878 df-oprab 5879 df-mpo 5880 df-1st 6141 df-2nd 6142 df-recs 6306 df-frec 6392 df-pnf 7994 df-mnf 7995 df-xr 7996 df-ltxr 7997 df-le 7998 df-sub 8130 df-neg 8131 df-reap 8532 df-ap 8539 df-div 8630 df-inn 8920 df-n0 9177 df-z 9254 df-uz 9529 df-q 9620 df-fz 10009 df-seqfrec 10446 df-fac 10706 df-bc 10728

This theorem is referenced by: bcn2 10744

W3C validator