bcval5 - Metamath Proof Explorer

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

Theorem bcval5 12541

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 12528	. . . 4
2	1	adantl 473	. . 3 $/\$ $/\$
3		mulcl 9641	. . . . . . . . 9 $/\$
4	3	adantl 473	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
5		mulass 9645	. . . . . . . . 9 $/\$ $/\$
6	5	adantl 473	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simplr 770	. . . . . . . . . . . . 13 $/\$ $/\$
8		elfzuz3 11823	. . . . . . . . . . . . . 14
9	8	adantl 473	. . . . . . . . . . . . 13 $/\$ $/\$
10		eluznn 11252	. . . . . . . . . . . . 13 $/\$
11	7, 9, 10	syl2anc 673	. . . . . . . . . . . 12 $/\$ $/\$
12	11	adantrr 731	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13		simplr 770	. . . . . . . . . . 11 $/\$ $/\$ $/\$
14		nnre 10638	. . . . . . . . . . . 12
15		nnrp 11334	. . . . . . . . . . . 12
16		ltsubrp 11358	. . . . . . . . . . . 12 $/\$
17	14, 15, 16	syl2an 485	. . . . . . . . . . 11 $/\$
18	12, 13, 17	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
19	12	nnzd 11062	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		nnz 10983	. . . . . . . . . . . . 13
21	20	ad2antlr 741	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
22	19, 21	zsubcld 11068	. . . . . . . . . . 11 $/\$ $/\$ $/\$
23		zltp1le 11010	. . . . . . . . . . 11 $/\$
24	22, 19, 23	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
25	18, 24	mpbid 215	. . . . . . . . 9 $/\$ $/\$ $/\$
26	22	peano2zd 11066	. . . . . . . . . 10 $/\$ $/\$ $/\$
27		eluz 11196	. . . . . . . . . 10 $/\$
28	26, 19, 27	syl2anc 673	. . . . . . . . 9 $/\$ $/\$ $/\$
29	25, 28	mpbird 240	. . . . . . . 8 $/\$ $/\$ $/\$
30		simprr 774	. . . . . . . . 9 $/\$ $/\$ $/\$
31		nnuz 11218	. . . . . . . . 9
32	30, 31	syl6eleq 2559	. . . . . . . 8 $/\$ $/\$ $/\$
33		fvi 5937	. . . . . . . . . 10
34		elfzelz 11826	. . . . . . . . . . 11
35	34	zcnd 11064	. . . . . . . . . 10
36	33, 35	eqeltrd 2549	. . . . . . . . 9
37	36	adantl 473	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
38	4, 6, 29, 32, 37	seqsplit 12284	. . . . . . 7 $/\$ $/\$ $/\$
39		facnn 12499	. . . . . . . 8
40	12, 39	syl 17	. . . . . . 7 $/\$ $/\$ $/\$
41		facnn 12499	. . . . . . . . 9
42	30, 41	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	oveq1d 6323	. . . . . . 7 $/\$ $/\$ $/\$
44	38, 40, 43	3eqtr4d 2515	. . . . . 6 $/\$ $/\$ $/\$
45	44	expr 626	. . . . 5 $/\$ $/\$
46		simpll 768	. . . . . . . . 9 $/\$ $/\$
47		faccl 12507	. . . . . . . . 9
48		nncn 10639	. . . . . . . . 9
49	46, 47, 48	3syl 18	. . . . . . . 8 $/\$ $/\$
50	49	mulid2d 9679	. . . . . . 7 $/\$ $/\$
51	11, 39	syl 17	. . . . . . . 8 $/\$ $/\$
52	51	oveq2d 6324	. . . . . . 7 $/\$ $/\$
53	50, 52	eqtr3d 2507	. . . . . 6 $/\$ $/\$
54		fveq2 5879	. . . . . . . . 9
55		fac0 12500	. . . . . . . . 9
56	54, 55	syl6eq 2521	. . . . . . . 8
57		oveq1 6315	. . . . . . . . . . 11
58		0p1e1 10743	. . . . . . . . . . 11
59	57, 58	syl6eq 2521	. . . . . . . . . 10
60	59	seqeq1d 12257	. . . . . . . . 9
61	60	fveq1d 5881	. . . . . . . 8
62	56, 61	oveq12d 6326	. . . . . . 7
63	62	eqeq2d 2481	. . . . . 6
64	53, 63	syl5ibrcom 230	. . . . 5 $/\$ $/\$
65		fznn0sub 11857	. . . . . . 7
66	65	adantl 473	. . . . . 6 $/\$ $/\$
67		elnn0 10895	. . . . . 6 $\/$
68	66, 67	sylib 201	. . . . 5 $/\$ $/\$ $\/$
69	45, 64, 68	mpjaod 388	. . . 4 $/\$ $/\$
70	69	oveq1d 6323	. . 3 $/\$ $/\$
71		eqid 2471	. . . . . 6
72		nn0z 10984	. . . . . . . . 9
73		zsubcl 11003	. . . . . . . . 9 $/\$
74	72, 20, 73	syl2an 485	. . . . . . . 8 $/\$
75	74	peano2zd 11066	. . . . . . 7 $/\$
76	75	adantr 472	. . . . . 6 $/\$ $/\$
77		fvi 5937	. . . . . . . 8
78		eluzelcn 11194	. . . . . . . 8
79	77, 78	eqeltrd 2549	. . . . . . 7
80	79	adantl 473	. . . . . 6 $/\$ $/\$ $/\$
81	3	adantl 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82	71, 76, 80, 81	seqf 12272	. . . . 5 $/\$ $/\$
83	11, 7, 17	syl2anc 673	. . . . . . 7 $/\$ $/\$
84	74	adantr 472	. . . . . . . 8 $/\$ $/\$
85	11	nnzd 11062	. . . . . . . 8 $/\$ $/\$
86	84, 85, 23	syl2anc 673	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbid 215	. . . . . 6 $/\$ $/\$
88	76, 85, 27	syl2anc 673	. . . . . 6 $/\$ $/\$
89	87, 88	mpbird 240	. . . . 5 $/\$ $/\$
90	82, 89	ffvelrnd 6038	. . . 4 $/\$ $/\$
91		elfznn0 11913	. . . . . . 7
92	91	adantl 473	. . . . . 6 $/\$ $/\$
93		faccl 12507	. . . . . 6
94	92, 93	syl 17	. . . . 5 $/\$ $/\$
95	94	nncnd 10647	. . . 4 $/\$ $/\$
96		faccl 12507	. . . . . 6
97	66, 96	syl 17	. . . . 5 $/\$ $/\$
98	97	nncnd 10647	. . . 4 $/\$ $/\$
99	94	nnne0d 10676	. . . 4 $/\$ $/\$
100	97	nnne0d 10676	. . . 4 $/\$ $/\$
101	90, 95, 98, 99, 100	divcan5d 10431	. . 3 $/\$ $/\$
102	2, 70, 101	3eqtrd 2509	. 2 $/\$ $/\$
103		nnnn0 10900	. . . . 5
104	103	ad2antlr 741	. . . 4 $/\$ $/\$
105		nncn 10639	. . . . 5
106		nnne0 10664	. . . . 5
107	105, 106	div0d 10404	. . . 4
108	104, 93, 107	3syl 18	. . 3 $/\$ $/\$
109	3	adantl 473	. . . . 5 $/\$ $/\$ $/\$ $/\$
110		fvi 5937	. . . . . . 7
111		elfzelz 11826	. . . . . . . 8
112	111	zcnd 11064	. . . . . . 7
113	110, 112	eqeltrd 2549	. . . . . 6
114	113	adantl 473	. . . . 5 $/\$ $/\$ $/\$
115		mul02 9829	. . . . . 6
116	115	adantl 473	. . . . 5 $/\$ $/\$ $/\$
117		mul01 9830	. . . . . 6
118	117	adantl 473	. . . . 5 $/\$ $/\$ $/\$
119		simpr 468	. . . . . . . . 9 $/\$ $/\$
120		nn0uz 11217	. . . . . . . . . . . 12
121	104, 120	syl6eleq 2559	. . . . . . . . . . 11 $/\$ $/\$
122	72	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$
123		elfz5 11818	. . . . . . . . . . 11 $/\$
124	121, 122, 123	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$
125		nn0re 10902	. . . . . . . . . . . 12
126	125	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$
127		nnre 10638	. . . . . . . . . . . 12
128	127	ad2antlr 741	. . . . . . . . . . 11 $/\$ $/\$
129	126, 128	subge0d 10224	. . . . . . . . . 10 $/\$ $/\$
130	124, 129	bitr4d 264	. . . . . . . . 9 $/\$ $/\$
131	119, 130	mtbid 307	. . . . . . . 8 $/\$ $/\$
132	74	adantr 472	. . . . . . . . . 10 $/\$ $/\$
133	132	zred 11063	. . . . . . . . 9 $/\$ $/\$
134		0re 9661	. . . . . . . . 9
135		ltnle 9731	. . . . . . . . 9 $/\$
136	133, 134, 135	sylancl 675	. . . . . . . 8 $/\$ $/\$
137	131, 136	mpbird 240	. . . . . . 7 $/\$ $/\$
138		0z 10972	. . . . . . . 8
139		zltp1le 11010	. . . . . . . 8 $/\$
140	132, 138, 139	sylancl 675	. . . . . . 7 $/\$ $/\$
141	137, 140	mpbid 215	. . . . . 6 $/\$ $/\$
142		nn0ge0 10919	. . . . . . 7
143	142	ad2antrr 740	. . . . . 6 $/\$ $/\$
144		0zd 10973	. . . . . . 7 $/\$ $/\$
145	75	adantr 472	. . . . . . 7 $/\$ $/\$
146		elfz 11816	. . . . . . 7 $/\$ $/\$ $/\$
147	144, 145, 122, 146	syl3anc 1292	. . . . . 6 $/\$ $/\$ $/\$
148	141, 143, 147	mpbir2and 936	. . . . 5 $/\$ $/\$
149		simpll 768	. . . . 5 $/\$ $/\$
150		0cn 9653	. . . . . 6
151		fvi 5937	. . . . . 6
152	150, 151	mp1i 13	. . . . 5 $/\$ $/\$
153	109, 114, 116, 118, 148, 149, 152	seqz 12299	. . . 4 $/\$ $/\$
154	153	oveq1d 6323	. . 3 $/\$ $/\$
155		bcval3 12529	. . . . 5 $/\$ $/\$
156	20, 155	syl3an2 1326	. . . 4 $/\$ $/\$
157	156	3expa 1231	. . 3 $/\$ $/\$
158	108, 154, 157	3eqtr4rd 2516	. 2 $/\$ $/\$
159	102, 158	pm2.61dan 808	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904 class class class wbr 4395

cid 4749

cfv 5589 (class class class)co 6308

cc 9555

cr 9556

cc0 9557

c1 9558

caddc 9560

cmul 9562

clt 9693

cle 9694

cmin 9880

cdiv 10291

cn 10631

cn0 10893

cz 10961

cuz 11182

crp 11325

cfz 11810

cseq 12251

cfa 12497

cbc 12525

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-nn 10632 df-n0 10894 df-z 10962 df-uz 11183 df-rp 11326 df-fz 11811 df-seq 12252 df-fac 12498 df-bc 12526

This theorem is referenced by: bcn2 12542

W3C validator