bcval5 - Metamath Proof Explorer

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

Theorem bcval5 12489

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 12476	. . . 4
2	1	adantl 467	. . 3 $/\$ $/\$
3		mulcl 9612	. . . . . . . . 9 $/\$
4	3	adantl 467	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
5		mulass 9616	. . . . . . . . 9 $/\$ $/\$
6	5	adantl 467	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simplr 760	. . . . . . . . . . . . 13 $/\$ $/\$
8		elfzuz3 11784	. . . . . . . . . . . . . 14
9	8	adantl 467	. . . . . . . . . . . . 13 $/\$ $/\$
10		eluznn 11218	. . . . . . . . . . . . 13 $/\$
11	7, 9, 10	syl2anc 665	. . . . . . . . . . . 12 $/\$ $/\$
12	11	adantrr 721	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13		simplr 760	. . . . . . . . . . 11 $/\$ $/\$ $/\$
14		nnre 10605	. . . . . . . . . . . 12
15		nnrp 11300	. . . . . . . . . . . 12
16		ltsubrp 11324	. . . . . . . . . . . 12 $/\$
17	14, 15, 16	syl2an 479	. . . . . . . . . . 11 $/\$
18	12, 13, 17	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
19	12	nnzd 11028	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		nnz 10948	. . . . . . . . . . . . 13
21	20	ad2antlr 731	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
22	19, 21	zsubcld 11034	. . . . . . . . . . 11 $/\$ $/\$ $/\$
23		zltp1le 10975	. . . . . . . . . . 11 $/\$
24	22, 19, 23	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
25	18, 24	mpbid 213	. . . . . . . . 9 $/\$ $/\$ $/\$
26	22	peano2zd 11032	. . . . . . . . . 10 $/\$ $/\$ $/\$
27		eluz 11161	. . . . . . . . . 10 $/\$
28	26, 19, 27	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$
29	25, 28	mpbird 235	. . . . . . . 8 $/\$ $/\$ $/\$
30		simprr 764	. . . . . . . . 9 $/\$ $/\$ $/\$
31		nnuz 11183	. . . . . . . . 9
32	30, 31	syl6eleq 2518	. . . . . . . 8 $/\$ $/\$ $/\$
33		fvi 5929	. . . . . . . . . 10
34		elfzelz 11787	. . . . . . . . . . 11
35	34	zcnd 11030	. . . . . . . . . 10
36	33, 35	eqeltrd 2508	. . . . . . . . 9
37	36	adantl 467	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
38	4, 6, 29, 32, 37	seqsplit 12232	. . . . . . 7 $/\$ $/\$ $/\$
39		facnn 12447	. . . . . . . 8
40	12, 39	syl 17	. . . . . . 7 $/\$ $/\$ $/\$
41		facnn 12447	. . . . . . . . 9
42	30, 41	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	oveq1d 6311	. . . . . . 7 $/\$ $/\$ $/\$
44	38, 40, 43	3eqtr4d 2471	. . . . . 6 $/\$ $/\$ $/\$
45	44	expr 618	. . . . 5 $/\$ $/\$
46		simpll 758	. . . . . . . . 9 $/\$ $/\$
47		faccl 12455	. . . . . . . . 9
48		nncn 10606	. . . . . . . . 9
49	46, 47, 48	3syl 18	. . . . . . . 8 $/\$ $/\$
50	49	mulid2d 9650	. . . . . . 7 $/\$ $/\$
51	11, 39	syl 17	. . . . . . . 8 $/\$ $/\$
52	51	oveq2d 6312	. . . . . . 7 $/\$ $/\$
53	50, 52	eqtr3d 2463	. . . . . 6 $/\$ $/\$
54		fveq2 5872	. . . . . . . . 9
55		fac0 12448	. . . . . . . . 9
56	54, 55	syl6eq 2477	. . . . . . . 8
57		oveq1 6303	. . . . . . . . . . 11
58		0p1e1 10710	. . . . . . . . . . 11
59	57, 58	syl6eq 2477	. . . . . . . . . 10
60	59	seqeq1d 12205	. . . . . . . . 9
61	60	fveq1d 5874	. . . . . . . 8
62	56, 61	oveq12d 6314	. . . . . . 7
63	62	eqeq2d 2434	. . . . . 6
64	53, 63	syl5ibrcom 225	. . . . 5 $/\$ $/\$
65		fznn0sub 11818	. . . . . . 7
66	65	adantl 467	. . . . . 6 $/\$ $/\$
67		elnn0 10860	. . . . . 6 $\/$
68	66, 67	sylib 199	. . . . 5 $/\$ $/\$ $\/$
69	45, 64, 68	mpjaod 382	. . . 4 $/\$ $/\$
70	69	oveq1d 6311	. . 3 $/\$ $/\$
71		eqid 2420	. . . . . 6
72		nn0z 10949	. . . . . . . . 9
73		zsubcl 10968	. . . . . . . . 9 $/\$
74	72, 20, 73	syl2an 479	. . . . . . . 8 $/\$
75	74	peano2zd 11032	. . . . . . 7 $/\$
76	75	adantr 466	. . . . . 6 $/\$ $/\$
77		fvi 5929	. . . . . . . 8
78		eluzelcn 11159	. . . . . . . 8
79	77, 78	eqeltrd 2508	. . . . . . 7
80	79	adantl 467	. . . . . 6 $/\$ $/\$ $/\$
81	3	adantl 467	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82	71, 76, 80, 81	seqf 12220	. . . . 5 $/\$ $/\$
83	11, 7, 17	syl2anc 665	. . . . . . 7 $/\$ $/\$
84	74	adantr 466	. . . . . . . 8 $/\$ $/\$
85	11	nnzd 11028	. . . . . . . 8 $/\$ $/\$
86	84, 85, 23	syl2anc 665	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbid 213	. . . . . 6 $/\$ $/\$
88	76, 85, 27	syl2anc 665	. . . . . 6 $/\$ $/\$
89	87, 88	mpbird 235	. . . . 5 $/\$ $/\$
90	82, 89	ffvelrnd 6029	. . . 4 $/\$ $/\$
91		elfznn0 11874	. . . . . . 7
92	91	adantl 467	. . . . . 6 $/\$ $/\$
93		faccl 12455	. . . . . 6
94	92, 93	syl 17	. . . . 5 $/\$ $/\$
95	94	nncnd 10614	. . . 4 $/\$ $/\$
96		faccl 12455	. . . . . 6
97	66, 96	syl 17	. . . . 5 $/\$ $/\$
98	97	nncnd 10614	. . . 4 $/\$ $/\$
99	94	nnne0d 10643	. . . 4 $/\$ $/\$
100	97	nnne0d 10643	. . . 4 $/\$ $/\$
101	90, 95, 98, 99, 100	divcan5d 10398	. . 3 $/\$ $/\$
102	2, 70, 101	3eqtrd 2465	. 2 $/\$ $/\$
103		nnnn0 10865	. . . . 5
104	103	ad2antlr 731	. . . 4 $/\$ $/\$
105		nncn 10606	. . . . 5
106		nnne0 10631	. . . . 5
107	105, 106	div0d 10371	. . . 4
108	104, 93, 107	3syl 18	. . 3 $/\$ $/\$
109	3	adantl 467	. . . . 5 $/\$ $/\$ $/\$ $/\$
110		fvi 5929	. . . . . . 7
111		elfzelz 11787	. . . . . . . 8
112	111	zcnd 11030	. . . . . . 7
113	110, 112	eqeltrd 2508	. . . . . 6
114	113	adantl 467	. . . . 5 $/\$ $/\$ $/\$
115		mul02 9800	. . . . . 6
116	115	adantl 467	. . . . 5 $/\$ $/\$ $/\$
117		mul01 9801	. . . . . 6
118	117	adantl 467	. . . . 5 $/\$ $/\$ $/\$
119		simpr 462	. . . . . . . . 9 $/\$ $/\$
120		nn0uz 11182	. . . . . . . . . . . 12
121	104, 120	syl6eleq 2518	. . . . . . . . . . 11 $/\$ $/\$
122	72	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$
123		elfz5 11779	. . . . . . . . . . 11 $/\$
124	121, 122, 123	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$
125		nn0re 10867	. . . . . . . . . . . 12
126	125	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$
127		nnre 10605	. . . . . . . . . . . 12
128	127	ad2antlr 731	. . . . . . . . . . 11 $/\$ $/\$
129	126, 128	subge0d 10192	. . . . . . . . . 10 $/\$ $/\$
130	124, 129	bitr4d 259	. . . . . . . . 9 $/\$ $/\$
131	119, 130	mtbid 301	. . . . . . . 8 $/\$ $/\$
132	74	adantr 466	. . . . . . . . . 10 $/\$ $/\$
133	132	zred 11029	. . . . . . . . 9 $/\$ $/\$
134		0re 9632	. . . . . . . . 9
135		ltnle 9702	. . . . . . . . 9 $/\$
136	133, 134, 135	sylancl 666	. . . . . . . 8 $/\$ $/\$
137	131, 136	mpbird 235	. . . . . . 7 $/\$ $/\$
138		0z 10937	. . . . . . . 8
139		zltp1le 10975	. . . . . . . 8 $/\$
140	132, 138, 139	sylancl 666	. . . . . . 7 $/\$ $/\$
141	137, 140	mpbid 213	. . . . . 6 $/\$ $/\$
142		nn0ge0 10884	. . . . . . 7
143	142	ad2antrr 730	. . . . . 6 $/\$ $/\$
144		0zd 10938	. . . . . . 7 $/\$ $/\$
145	75	adantr 466	. . . . . . 7 $/\$ $/\$
146		elfz 11777	. . . . . . 7 $/\$ $/\$ $/\$
147	144, 145, 122, 146	syl3anc 1264	. . . . . 6 $/\$ $/\$ $/\$
148	141, 143, 147	mpbir2and 930	. . . . 5 $/\$ $/\$
149		simpll 758	. . . . 5 $/\$ $/\$
150		0cn 9624	. . . . . 6
151		fvi 5929	. . . . . 6
152	150, 151	mp1i 13	. . . . 5 $/\$ $/\$
153	109, 114, 116, 118, 148, 149, 152	seqz 12247	. . . 4 $/\$ $/\$
154	153	oveq1d 6311	. . 3 $/\$ $/\$
155		bcval3 12477	. . . . 5 $/\$ $/\$
156	20, 155	syl3an2 1298	. . . 4 $/\$ $/\$
157	156	3expa 1205	. . 3 $/\$ $/\$
158	108, 154, 157	3eqtr4rd 2472	. 2 $/\$ $/\$
159	102, 158	pm2.61dan 798	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $\/$ wo 369 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1867 class class class wbr 4417

cid 4755

cfv 5592 (class class class)co 6296

cc 9526

cr 9527

cc0 9528

c1 9529

caddc 9531

cmul 9533

clt 9664

cle 9665

cmin 9849

cdiv 10258

cn 10598

cn0 10858

cz 10926

cuz 11148

crp 11291

cfz 11771

cseq 12199

cfa 12445

cbc 12473

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rmo 2781 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-er 7362 df-en 7569 df-dom 7570 df-sdom 7571 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-div 10259 df-nn 10599 df-n0 10859 df-z 10927 df-uz 11149 df-rp 11292 df-fz 11772 df-seq 12200 df-fac 12446 df-bc 12474

This theorem is referenced by: bcn2 12490

W3C validator