bcval5 - Intuitionistic Logic Explorer

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

Theorem bcval5 10502

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 10489	. . . 4
2	1	adantl 275	. . 3 $/\$ $/\$
3		simprl 520	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
4		simprr 521	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
5	3, 4	mulcld 7779	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
6		simpr1 987	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simpr2 988	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
8		simpr3 989	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
9	6, 7, 8	mulassd 7782	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simpll 518	. . . . . . . . . . . . 13 $/\$ $/\$
11	10	nn0zd 9164	. . . . . . . . . . . 12 $/\$ $/\$
12		simplr 519	. . . . . . . . . . . . 13 $/\$ $/\$
13	12	nnzd 9165	. . . . . . . . . . . 12 $/\$ $/\$
14	11, 13	zsubcld 9171	. . . . . . . . . . 11 $/\$ $/\$
15	14	peano2zd 9169	. . . . . . . . . 10 $/\$ $/\$
16		1red 7774	. . . . . . . . . . . 12 $/\$ $/\$
17	12	nnred 8726	. . . . . . . . . . . 12 $/\$ $/\$
18	10	nn0red 9024	. . . . . . . . . . . 12 $/\$ $/\$
19	12	nnge1d 8756	. . . . . . . . . . . 12 $/\$ $/\$
20	16, 17, 18, 19	lesub2dd 8317	. . . . . . . . . . 11 $/\$ $/\$
21	14	zred 9166	. . . . . . . . . . . 12 $/\$ $/\$
22		leaddsub 8193	. . . . . . . . . . . 12 $/\$ $/\$
23	21, 16, 18, 22	syl3anc 1216	. . . . . . . . . . 11 $/\$ $/\$
24	20, 23	mpbird 166	. . . . . . . . . 10 $/\$ $/\$
25		eluz2 9325	. . . . . . . . . 10 $/\$ $/\$
26	15, 11, 24, 25	syl3anbrc 1165	. . . . . . . . 9 $/\$ $/\$
27	26	adantrr 470	. . . . . . . 8 $/\$ $/\$ $/\$
28		simprr 521	. . . . . . . . 9 $/\$ $/\$ $/\$
29		nnuz 9354	. . . . . . . . 9
30	28, 29	eleqtrdi 2230	. . . . . . . 8 $/\$ $/\$ $/\$
31		fvi 5471	. . . . . . . . . 10
32	31	elv 2685	. . . . . . . . 9
33		eluzelcn 9330	. . . . . . . . . 10
34	33	adantl 275	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	32, 34	eqeltrid 2224	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
36	5, 9, 27, 30, 35	seq3split 10245	. . . . . . 7 $/\$ $/\$ $/\$
37		elfzuz3 9796	. . . . . . . . . . 11
38	37	adantl 275	. . . . . . . . . 10 $/\$ $/\$
39		eluznn 9387	. . . . . . . . . 10 $/\$
40	12, 38, 39	syl2anc 408	. . . . . . . . 9 $/\$ $/\$
41	40	adantrr 470	. . . . . . . 8 $/\$ $/\$ $/\$
42		facnn 10466	. . . . . . . 8
43	41, 42	syl 14	. . . . . . 7 $/\$ $/\$ $/\$
44		facnn 10466	. . . . . . . . 9
45	28, 44	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$
46	45	oveq1d 5782	. . . . . . 7 $/\$ $/\$ $/\$
47	36, 43, 46	3eqtr4d 2180	. . . . . 6 $/\$ $/\$ $/\$
48	47	expr 372	. . . . 5 $/\$ $/\$
49	10	faccld 10475	. . . . . . . . 9 $/\$ $/\$
50	49	nncnd 8727	. . . . . . . 8 $/\$ $/\$
51	50	mulid2d 7777	. . . . . . 7 $/\$ $/\$
52	40, 42	syl 14	. . . . . . . 8 $/\$ $/\$
53	52	oveq2d 5783	. . . . . . 7 $/\$ $/\$
54	51, 53	eqtr3d 2172	. . . . . 6 $/\$ $/\$
55		fveq2 5414	. . . . . . . . 9
56		fac0 10467	. . . . . . . . 9
57	55, 56	syl6eq 2186	. . . . . . . 8
58		oveq1 5774	. . . . . . . . . . 11
59		0p1e1 8827	. . . . . . . . . . 11
60	58, 59	syl6eq 2186	. . . . . . . . . 10
61	60	seqeq1d 10217	. . . . . . . . 9
62	61	fveq1d 5416	. . . . . . . 8
63	57, 62	oveq12d 5785	. . . . . . 7
64	63	eqeq2d 2149	. . . . . 6
65	54, 64	syl5ibrcom 156	. . . . 5 $/\$ $/\$
66		fznn0sub 9830	. . . . . . 7
67	66	adantl 275	. . . . . 6 $/\$ $/\$
68		elnn0 8972	. . . . . 6 $\/$
69	67, 68	sylib 121	. . . . 5 $/\$ $/\$ $\/$
70	48, 65, 69	mpjaod 707	. . . 4 $/\$ $/\$
71	70	oveq1d 5782	. . 3 $/\$ $/\$
72		eqid 2137	. . . . . 6
73		fvi 5471	. . . . . . . 8
74	73	elv 2685	. . . . . . 7
75		eluzelcn 9330	. . . . . . . 8
76	75	adantl 275	. . . . . . 7 $/\$ $/\$ $/\$
77	74, 76	eqeltrid 2224	. . . . . 6 $/\$ $/\$ $/\$
78		mulcl 7740	. . . . . . 7 $/\$
79	78	adantl 275	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80	72, 15, 77, 79	seqf 10227	. . . . 5 $/\$ $/\$
81	80, 26	ffvelrnd 5549	. . . 4 $/\$ $/\$
82	12	nnnn0d 9023	. . . . . 6 $/\$ $/\$
83	82	faccld 10475	. . . . 5 $/\$ $/\$
84	83	nncnd 8727	. . . 4 $/\$ $/\$
85	67	faccld 10475	. . . . 5 $/\$ $/\$
86	85	nncnd 8727	. . . 4 $/\$ $/\$
87	83	nnap0d 8759	. . . 4 $/\$ $/\$ #
88	85	nnap0d 8759	. . . 4 $/\$ $/\$ #
89	81, 84, 86, 87, 88	divcanap5d 8570	. . 3 $/\$ $/\$
90	2, 71, 89	3eqtrd 2174	. 2 $/\$ $/\$
91		simplr 519	. . . . . . 7 $/\$ $/\$
92	91	nnnn0d 9023	. . . . . 6 $/\$ $/\$
93	92	faccld 10475	. . . . 5 $/\$ $/\$
94	93	nncnd 8727	. . . 4 $/\$ $/\$
95	93	nnap0d 8759	. . . 4 $/\$ $/\$ #
96	94, 95	div0apd 8540	. . 3 $/\$ $/\$
97		mulcl 7740	. . . . . 6 $/\$
98	97	adantl 275	. . . . 5 $/\$ $/\$ $/\$ $/\$
99		eluzelcn 9330	. . . . . . 7
100	99	adantl 275	. . . . . 6 $/\$ $/\$ $/\$
101	32, 100	eqeltrid 2224	. . . . 5 $/\$ $/\$ $/\$
102		simpr 109	. . . . . 6 $/\$ $/\$ $/\$
103	102	mul02d 8147	. . . . 5 $/\$ $/\$ $/\$
104	102	mul01d 8148	. . . . 5 $/\$ $/\$ $/\$
105		simpr 109	. . . . . . . . 9 $/\$ $/\$
106		nn0uz 9353	. . . . . . . . . . . 12
107	92, 106	eleqtrdi 2230	. . . . . . . . . . 11 $/\$ $/\$
108		simpll 518	. . . . . . . . . . . 12 $/\$ $/\$
109	108	nn0zd 9164	. . . . . . . . . . 11 $/\$ $/\$
110		elfz5 9791	. . . . . . . . . . 11 $/\$
111	107, 109, 110	syl2anc 408	. . . . . . . . . 10 $/\$ $/\$
112		nn0re 8979	. . . . . . . . . . . 12
113	112	ad2antrr 479	. . . . . . . . . . 11 $/\$ $/\$
114		nnre 8720	. . . . . . . . . . . 12
115	114	ad2antlr 480	. . . . . . . . . . 11 $/\$ $/\$
116	113, 115	subge0d 8290	. . . . . . . . . 10 $/\$ $/\$
117	111, 116	bitr4d 190	. . . . . . . . 9 $/\$ $/\$
118	105, 117	mtbid 661	. . . . . . . 8 $/\$ $/\$
119		simpl 108	. . . . . . . . . . . 12 $/\$
120	119	nn0zd 9164	. . . . . . . . . . 11 $/\$
121		simpr 109	. . . . . . . . . . . 12 $/\$
122	121	nnzd 9165	. . . . . . . . . . 11 $/\$
123	120, 122	zsubcld 9171	. . . . . . . . . 10 $/\$
124	123	adantr 274	. . . . . . . . 9 $/\$ $/\$
125		0z 9058	. . . . . . . . 9
126		zltnle 9093	. . . . . . . . 9 $/\$
127	124, 125, 126	sylancl 409	. . . . . . . 8 $/\$ $/\$
128	118, 127	mpbird 166	. . . . . . 7 $/\$ $/\$
129		zltp1le 9101	. . . . . . . 8 $/\$
130	124, 125, 129	sylancl 409	. . . . . . 7 $/\$ $/\$
131	128, 130	mpbid 146	. . . . . 6 $/\$ $/\$
132		nn0ge0 8995	. . . . . . 7
133	132	ad2antrr 479	. . . . . 6 $/\$ $/\$
134		0zd 9059	. . . . . . 7 $/\$ $/\$
135	124	peano2zd 9169	. . . . . . 7 $/\$ $/\$
136		elfz 9789	. . . . . . 7 $/\$ $/\$ $/\$
137	134, 135, 109, 136	syl3anc 1216	. . . . . 6 $/\$ $/\$ $/\$
138	131, 133, 137	mpbir2and 928	. . . . 5 $/\$ $/\$
139		0cn 7751	. . . . . 6
140		fvi 5471	. . . . . 6
141	139, 140	mp1i 10	. . . . 5 $/\$ $/\$
142	98, 101, 103, 104, 138, 141	seq3z 10277	. . . 4 $/\$ $/\$
143	142	oveq1d 5782	. . 3 $/\$ $/\$
144		nnz 9066	. . . . 5
145		bcval3 10490	. . . . 5 $/\$ $/\$
146	144, 145	syl3an2 1250	. . . 4 $/\$ $/\$
147	146	3expa 1181	. . 3 $/\$ $/\$
148	96, 143, 147	3eqtr4rd 2181	. 2 $/\$ $/\$
149		0zd 9059	. . . 4 $/\$
150		fzdcel 9813	. . . 4 $/\$ $/\$ DECID
151	122, 149, 120, 150	syl3anc 1216	. . 3 $/\$ DECID
152		exmiddc 821	. . 3 DECID $\/$
153	151, 152	syl 14	. 2 $/\$ $\/$
154	90, 148, 153	mpjaodan 787	1 $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697 DECID wdc 819 $/\$ w3a 962

wceq 1331

wcel 1480

cvv 2681 class class class wbr 3924

cid 4205

cfv 5118 (class class class)co 5767

cc 7611

cr 7612

cc0 7613

c1 7614

caddc 7616

cmul 7618

clt 7793

cle 7794

cmin 7926

cdiv 8425

cn 8713

cn0 8970

cz 9047

cuz 9319

cfz 9783

cseq 10211

cfa 10464

cbc 10486

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 ax-coll 4038 ax-sep 4041 ax-nul 4049 ax-pow 4093 ax-pr 4126 ax-un 4350 ax-setind 4447 ax-iinf 4497 ax-cnex 7704 ax-resscn 7705 ax-1cn 7706 ax-1re 7707 ax-icn 7708 ax-addcl 7709 ax-addrcl 7710 ax-mulcl 7711 ax-mulrcl 7712 ax-addcom 7713 ax-mulcom 7714 ax-addass 7715 ax-mulass 7716 ax-distr 7717 ax-i2m1 7718 ax-0lt1 7719 ax-1rid 7720 ax-0id 7721 ax-rnegex 7722 ax-precex 7723 ax-cnre 7724 ax-pre-ltirr 7725 ax-pre-ltwlin 7726 ax-pre-lttrn 7727 ax-pre-apti 7728 ax-pre-ltadd 7729 ax-pre-mulgt0 7730 ax-pre-mulext 7731

This theorem depends on definitions: df-bi 116 df-dc 820 df-3or 963 df-3an 964 df-tru 1334 df-fal 1337 df-nf 1437 df-sb 1736 df-eu 2000 df-mo 2001 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-ne 2307 df-nel 2402 df-ral 2419 df-rex 2420 df-reu 2421 df-rmo 2422 df-rab 2423 df-v 2683 df-sbc 2905 df-csb 2999 df-dif 3068 df-un 3070 df-in 3072 df-ss 3079 df-nul 3359 df-if 3470 df-pw 3507 df-sn 3528 df-pr 3529 df-op 3531 df-uni 3732 df-int 3767 df-iun 3810 df-br 3925 df-opab 3985 df-mpt 3986 df-tr 4022 df-id 4210 df-po 4213 df-iso 4214 df-iord 4283 df-on 4285 df-ilim 4286 df-suc 4288 df-iom 4500 df-xp 4540 df-rel 4541 df-cnv 4542 df-co 4543 df-dm 4544 df-rn 4545 df-res 4546 df-ima 4547 df-iota 5083 df-fun 5120 df-fn 5121 df-f 5122 df-f1 5123 df-fo 5124 df-f1o 5125 df-fv 5126 df-riota 5723 df-ov 5770 df-oprab 5771 df-mpo 5772 df-1st 6031 df-2nd 6032 df-recs 6195 df-frec 6281 df-pnf 7795 df-mnf 7796 df-xr 7797 df-ltxr 7798 df-le 7799 df-sub 7928 df-neg 7929 df-reap 8330 df-ap 8337 df-div 8426 df-inn 8714 df-n0 8971 df-z 9048 df-uz 9320 df-q 9405 df-fz 9784 df-seqfrec 10212 df-fac 10465 df-bc 10487

This theorem is referenced by: bcn2 10503

W3C validator