bcval5 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bcval5		Structured version Unicode version

Theorem bcval5 12364

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.)

**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 12351	. . . 4
2	1	adantl 466	. . 3 $/\$ $/\$
3		mulcl 9576	. . . . . . . . 9 $/\$
4	3	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
5		mulass 9580	. . . . . . . . 9 $/\$ $/\$
6	5	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simplr 754	. . . . . . . . . . . . 13 $/\$ $/\$
8		elfzuz3 11685	. . . . . . . . . . . . . 14
9	8	adantl 466	. . . . . . . . . . . . 13 $/\$ $/\$
10		eluznn 11152	. . . . . . . . . . . . 13 $/\$
11	7, 9, 10	syl2anc 661	. . . . . . . . . . . 12 $/\$ $/\$
12	11	adantrr 716	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13		simplr 754	. . . . . . . . . . 11 $/\$ $/\$ $/\$
14		nnre 10543	. . . . . . . . . . . 12
15		nnrp 11229	. . . . . . . . . . . 12
16		ltsubrp 11251	. . . . . . . . . . . 12 $/\$
17	14, 15, 16	syl2an 477	. . . . . . . . . . 11 $/\$
18	12, 13, 17	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
19	12	nnzd 10965	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		nnz 10886	. . . . . . . . . . . . 13
21	20	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
22	19, 21	zsubcld 10971	. . . . . . . . . . 11 $/\$ $/\$ $/\$
23		zltp1le 10912	. . . . . . . . . . 11 $/\$
24	22, 19, 23	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$
25	18, 24	mpbid 210	. . . . . . . . 9 $/\$ $/\$ $/\$
26	22	peano2zd 10969	. . . . . . . . . 10 $/\$ $/\$ $/\$
27		eluz 11095	. . . . . . . . . 10 $/\$
28	26, 19, 27	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$
29	25, 28	mpbird 232	. . . . . . . 8 $/\$ $/\$ $/\$
30		simprr 756	. . . . . . . . 9 $/\$ $/\$ $/\$
31		nnuz 11117	. . . . . . . . 9
32	30, 31	syl6eleq 2565	. . . . . . . 8 $/\$ $/\$ $/\$
33		fvi 5924	. . . . . . . . . 10
34		elfzelz 11688	. . . . . . . . . . 11
35	34	zcnd 10967	. . . . . . . . . 10
36	33, 35	eqeltrd 2555	. . . . . . . . 9
37	36	adantl 466	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
38	4, 6, 29, 32, 37	seqsplit 12108	. . . . . . 7 $/\$ $/\$ $/\$
39		facnn 12323	. . . . . . . 8
40	12, 39	syl 16	. . . . . . 7 $/\$ $/\$ $/\$
41		facnn 12323	. . . . . . . . 9
42	30, 41	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	oveq1d 6299	. . . . . . 7 $/\$ $/\$ $/\$
44	38, 40, 43	3eqtr4d 2518	. . . . . 6 $/\$ $/\$ $/\$
45	44	expr 615	. . . . 5 $/\$ $/\$
46		simpll 753	. . . . . . . . 9 $/\$ $/\$
47		faccl 12331	. . . . . . . . 9
48		nncn 10544	. . . . . . . . 9
49	46, 47, 48	3syl 20	. . . . . . . 8 $/\$ $/\$
50	49	mulid2d 9614	. . . . . . 7 $/\$ $/\$
51	11, 39	syl 16	. . . . . . . 8 $/\$ $/\$
52	51	oveq2d 6300	. . . . . . 7 $/\$ $/\$
53	50, 52	eqtr3d 2510	. . . . . 6 $/\$ $/\$
54		fveq2 5866	. . . . . . . . 9
55		fac0 12324	. . . . . . . . 9
56	54, 55	syl6eq 2524	. . . . . . . 8
57		oveq1 6291	. . . . . . . . . . 11
58		0p1e1 10647	. . . . . . . . . . 11
59	57, 58	syl6eq 2524	. . . . . . . . . 10
60	59	seqeq1d 12081	. . . . . . . . 9
61	60	fveq1d 5868	. . . . . . . 8
62	56, 61	oveq12d 6302	. . . . . . 7
63	62	eqeq2d 2481	. . . . . 6
64	53, 63	syl5ibrcom 222	. . . . 5 $/\$ $/\$
65		fznn0sub 11716	. . . . . . 7
66	65	adantl 466	. . . . . 6 $/\$ $/\$
67		elnn0 10797	. . . . . 6 $\/$
68	66, 67	sylib 196	. . . . 5 $/\$ $/\$ $\/$
69	45, 64, 68	mpjaod 381	. . . 4 $/\$ $/\$
70	69	oveq1d 6299	. . 3 $/\$ $/\$
71		eqid 2467	. . . . . 6
72		nn0z 10887	. . . . . . . . 9
73		zsubcl 10905	. . . . . . . . 9 $/\$
74	72, 20, 73	syl2an 477	. . . . . . . 8 $/\$
75	74	peano2zd 10969	. . . . . . 7 $/\$
76	75	adantr 465	. . . . . 6 $/\$ $/\$
77		fvi 5924	. . . . . . . 8
78		eluzelz 11091	. . . . . . . . 9
79	78	zcnd 10967	. . . . . . . 8
80	77, 79	eqeltrd 2555	. . . . . . 7
81	80	adantl 466	. . . . . 6 $/\$ $/\$ $/\$
82	3	adantl 466	. . . . . 6 $/\$ $/\$ $/\$ $/\$
83	71, 76, 81, 82	seqf 12096	. . . . 5 $/\$ $/\$
84	11, 7, 17	syl2anc 661	. . . . . . 7 $/\$ $/\$
85	74	adantr 465	. . . . . . . 8 $/\$ $/\$
86	11	nnzd 10965	. . . . . . . 8 $/\$ $/\$
87	85, 86, 23	syl2anc 661	. . . . . . 7 $/\$ $/\$
88	84, 87	mpbid 210	. . . . . 6 $/\$ $/\$
89	76, 86, 27	syl2anc 661	. . . . . 6 $/\$ $/\$
90	88, 89	mpbird 232	. . . . 5 $/\$ $/\$
91	83, 90	ffvelrnd 6022	. . . 4 $/\$ $/\$
92		elfznn0 11770	. . . . . . 7
93	92	adantl 466	. . . . . 6 $/\$ $/\$
94		faccl 12331	. . . . . 6
95	93, 94	syl 16	. . . . 5 $/\$ $/\$
96	95	nncnd 10552	. . . 4 $/\$ $/\$
97		faccl 12331	. . . . . 6
98	66, 97	syl 16	. . . . 5 $/\$ $/\$
99	98	nncnd 10552	. . . 4 $/\$ $/\$
100	95	nnne0d 10580	. . . 4 $/\$ $/\$
101	98	nnne0d 10580	. . . 4 $/\$ $/\$
102	91, 96, 99, 100, 101	divcan5d 10346	. . 3 $/\$ $/\$
103	2, 70, 102	3eqtrd 2512	. 2 $/\$ $/\$
104		nnnn0 10802	. . . . 5
105	104	ad2antlr 726	. . . 4 $/\$ $/\$
106		nncn 10544	. . . . 5
107		nnne0 10568	. . . . 5
108	106, 107	div0d 10319	. . . 4
109	105, 94, 108	3syl 20	. . 3 $/\$ $/\$
110	3	adantl 466	. . . . 5 $/\$ $/\$ $/\$ $/\$
111		fvi 5924	. . . . . . 7
112		elfzelz 11688	. . . . . . . 8
113	112	zcnd 10967	. . . . . . 7
114	111, 113	eqeltrd 2555	. . . . . 6
115	114	adantl 466	. . . . 5 $/\$ $/\$ $/\$
116		mul02 9757	. . . . . 6
117	116	adantl 466	. . . . 5 $/\$ $/\$ $/\$
118		mul01 9758	. . . . . 6
119	118	adantl 466	. . . . 5 $/\$ $/\$ $/\$
120		simpr 461	. . . . . . . . 9 $/\$ $/\$
121		nn0uz 11116	. . . . . . . . . . . 12
122	105, 121	syl6eleq 2565	. . . . . . . . . . 11 $/\$ $/\$
123	72	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
124		elfz5 11680	. . . . . . . . . . 11 $/\$
125	122, 123, 124	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$
126		nn0re 10804	. . . . . . . . . . . 12
127	126	ad2antrr 725	. . . . . . . . . . 11 $/\$ $/\$
128		nnre 10543	. . . . . . . . . . . 12
129	128	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
130	127, 129	subge0d 10142	. . . . . . . . . 10 $/\$ $/\$
131	125, 130	bitr4d 256	. . . . . . . . 9 $/\$ $/\$
132	120, 131	mtbid 300	. . . . . . . 8 $/\$ $/\$
133	74	adantr 465	. . . . . . . . . 10 $/\$ $/\$
134	133	zred 10966	. . . . . . . . 9 $/\$ $/\$
135		0re 9596	. . . . . . . . 9
136		ltnle 9664	. . . . . . . . 9 $/\$
137	134, 135, 136	sylancl 662	. . . . . . . 8 $/\$ $/\$
138	132, 137	mpbird 232	. . . . . . 7 $/\$ $/\$
139		0z 10875	. . . . . . . 8
140		zltp1le 10912	. . . . . . . 8 $/\$
141	133, 139, 140	sylancl 662	. . . . . . 7 $/\$ $/\$
142	138, 141	mpbid 210	. . . . . 6 $/\$ $/\$
143		nn0ge0 10821	. . . . . . 7
144	143	ad2antrr 725	. . . . . 6 $/\$ $/\$
145		0zd 10876	. . . . . . 7 $/\$ $/\$
146	75	adantr 465	. . . . . . 7 $/\$ $/\$
147		elfz 11678	. . . . . . 7 $/\$ $/\$ $/\$
148	145, 146, 123, 147	syl3anc 1228	. . . . . 6 $/\$ $/\$ $/\$
149	142, 144, 148	mpbir2and 920	. . . . 5 $/\$ $/\$
150		simpll 753	. . . . 5 $/\$ $/\$
151		0cn 9588	. . . . . 6
152		fvi 5924	. . . . . 6
153	151, 152	mp1i 12	. . . . 5 $/\$ $/\$
154	110, 115, 117, 119, 149, 150, 153	seqz 12123	. . . 4 $/\$ $/\$
155	154	oveq1d 6299	. . 3 $/\$ $/\$
156		bcval3 12352	. . . . 5 $/\$ $/\$
157	20, 156	syl3an2 1262	. . . 4 $/\$ $/\$
158	157	3expa 1196	. . 3 $/\$ $/\$
159	109, 155, 158	3eqtr4rd 2519	. 2 $/\$ $/\$
160	103, 159	pm2.61dan 789	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wcel 1767 class class class wbr 4447

cid 4790

cfv 5588 (class class class)co 6284

cc 9490

cr 9491

cc0 9492

c1 9493

caddc 9495

cmul 9497

clt 9628

cle 9629

cmin 9805

cdiv 10206

cn 10536

cn0 10795

cz 10864

cuz 11082

crp 11220

cfz 11672

cseq 12075

cfa 12321

cbc 12348

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6576 ax-cnex 9548 ax-resscn 9549 ax-1cn 9550 ax-icn 9551 ax-addcl 9552 ax-addrcl 9553 ax-mulcl 9554 ax-mulrcl 9555 ax-mulcom 9556 ax-addass 9557 ax-mulass 9558 ax-distr 9559 ax-i2m1 9560 ax-1ne0 9561 ax-1rid 9562 ax-rnegex 9563 ax-rrecex 9564 ax-cnre 9565 ax-pre-lttri 9566 ax-pre-lttrn 9567 ax-pre-ltadd 9568 ax-pre-mulgt0 9569

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-riota 6245 df-ov 6287 df-oprab 6288 df-mpt2 6289 df-om 6685 df-1st 6784 df-2nd 6785 df-recs 7042 df-rdg 7076 df-er 7311 df-en 7517 df-dom 7518 df-sdom 7519 df-pnf 9630 df-mnf 9631 df-xr 9632 df-ltxr 9633 df-le 9634 df-sub 9807 df-neg 9808 df-div 10207 df-nn 10537 df-n0 10796 df-z 10865 df-uz 11083 df-rp 11221 df-fz 11673 df-seq 12076 df-fac 12322 df-bc 12349

This theorem is referenced by: bcn2 12365

W3C validator