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 12500

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 12487	. . . 4
2	1	adantl 468	. . 3 $/\$ $/\$
3		mulcl 9620	. . . . . . . . 9 $/\$
4	3	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
5		mulass 9624	. . . . . . . . 9 $/\$ $/\$
6	5	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		simplr 761	. . . . . . . . . . . . 13 $/\$ $/\$
8		elfzuz3 11794	. . . . . . . . . . . . . 14
9	8	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$
10		eluznn 11226	. . . . . . . . . . . . 13 $/\$
11	7, 9, 10	syl2anc 666	. . . . . . . . . . . 12 $/\$ $/\$
12	11	adantrr 722	. . . . . . . . . . 11 $/\$ $/\$ $/\$
13		simplr 761	. . . . . . . . . . 11 $/\$ $/\$ $/\$
14		nnre 10613	. . . . . . . . . . . 12
15		nnrp 11308	. . . . . . . . . . . 12
16		ltsubrp 11332	. . . . . . . . . . . 12 $/\$
17	14, 15, 16	syl2an 480	. . . . . . . . . . 11 $/\$
18	12, 13, 17	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$ $/\$
19	12	nnzd 11036	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
20		nnz 10956	. . . . . . . . . . . . 13
21	20	ad2antlr 732	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
22	19, 21	zsubcld 11042	. . . . . . . . . . 11 $/\$ $/\$ $/\$
23		zltp1le 10983	. . . . . . . . . . 11 $/\$
24	22, 19, 23	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$ $/\$
25	18, 24	mpbid 214	. . . . . . . . 9 $/\$ $/\$ $/\$
26	22	peano2zd 11040	. . . . . . . . . 10 $/\$ $/\$ $/\$
27		eluz 11169	. . . . . . . . . 10 $/\$
28	26, 19, 27	syl2anc 666	. . . . . . . . 9 $/\$ $/\$ $/\$
29	25, 28	mpbird 236	. . . . . . . 8 $/\$ $/\$ $/\$
30		simprr 765	. . . . . . . . 9 $/\$ $/\$ $/\$
31		nnuz 11191	. . . . . . . . 9
32	30, 31	syl6eleq 2538	. . . . . . . 8 $/\$ $/\$ $/\$
33		fvi 5920	. . . . . . . . . 10
34		elfzelz 11797	. . . . . . . . . . 11
35	34	zcnd 11038	. . . . . . . . . 10
36	33, 35	eqeltrd 2528	. . . . . . . . 9
37	36	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
38	4, 6, 29, 32, 37	seqsplit 12243	. . . . . . 7 $/\$ $/\$ $/\$
39		facnn 12458	. . . . . . . 8
40	12, 39	syl 17	. . . . . . 7 $/\$ $/\$ $/\$
41		facnn 12458	. . . . . . . . 9
42	30, 41	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$
43	42	oveq1d 6303	. . . . . . 7 $/\$ $/\$ $/\$
44	38, 40, 43	3eqtr4d 2494	. . . . . 6 $/\$ $/\$ $/\$
45	44	expr 619	. . . . 5 $/\$ $/\$
46		simpll 759	. . . . . . . . 9 $/\$ $/\$
47		faccl 12466	. . . . . . . . 9
48		nncn 10614	. . . . . . . . 9
49	46, 47, 48	3syl 18	. . . . . . . 8 $/\$ $/\$
50	49	mulid2d 9658	. . . . . . 7 $/\$ $/\$
51	11, 39	syl 17	. . . . . . . 8 $/\$ $/\$
52	51	oveq2d 6304	. . . . . . 7 $/\$ $/\$
53	50, 52	eqtr3d 2486	. . . . . 6 $/\$ $/\$
54		fveq2 5863	. . . . . . . . 9
55		fac0 12459	. . . . . . . . 9
56	54, 55	syl6eq 2500	. . . . . . . 8
57		oveq1 6295	. . . . . . . . . . 11
58		0p1e1 10718	. . . . . . . . . . 11
59	57, 58	syl6eq 2500	. . . . . . . . . 10
60	59	seqeq1d 12216	. . . . . . . . 9
61	60	fveq1d 5865	. . . . . . . 8
62	56, 61	oveq12d 6306	. . . . . . 7
63	62	eqeq2d 2460	. . . . . 6
64	53, 63	syl5ibrcom 226	. . . . 5 $/\$ $/\$
65		fznn0sub 11828	. . . . . . 7
66	65	adantl 468	. . . . . 6 $/\$ $/\$
67		elnn0 10868	. . . . . 6 $\/$
68	66, 67	sylib 200	. . . . 5 $/\$ $/\$ $\/$
69	45, 64, 68	mpjaod 383	. . . 4 $/\$ $/\$
70	69	oveq1d 6303	. . 3 $/\$ $/\$
71		eqid 2450	. . . . . 6
72		nn0z 10957	. . . . . . . . 9
73		zsubcl 10976	. . . . . . . . 9 $/\$
74	72, 20, 73	syl2an 480	. . . . . . . 8 $/\$
75	74	peano2zd 11040	. . . . . . 7 $/\$
76	75	adantr 467	. . . . . 6 $/\$ $/\$
77		fvi 5920	. . . . . . . 8
78		eluzelcn 11167	. . . . . . . 8
79	77, 78	eqeltrd 2528	. . . . . . 7
80	79	adantl 468	. . . . . 6 $/\$ $/\$ $/\$
81	3	adantl 468	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82	71, 76, 80, 81	seqf 12231	. . . . 5 $/\$ $/\$
83	11, 7, 17	syl2anc 666	. . . . . . 7 $/\$ $/\$
84	74	adantr 467	. . . . . . . 8 $/\$ $/\$
85	11	nnzd 11036	. . . . . . . 8 $/\$ $/\$
86	84, 85, 23	syl2anc 666	. . . . . . 7 $/\$ $/\$
87	83, 86	mpbid 214	. . . . . 6 $/\$ $/\$
88	76, 85, 27	syl2anc 666	. . . . . 6 $/\$ $/\$
89	87, 88	mpbird 236	. . . . 5 $/\$ $/\$
90	82, 89	ffvelrnd 6021	. . . 4 $/\$ $/\$
91		elfznn0 11884	. . . . . . 7
92	91	adantl 468	. . . . . 6 $/\$ $/\$
93		faccl 12466	. . . . . 6
94	92, 93	syl 17	. . . . 5 $/\$ $/\$
95	94	nncnd 10622	. . . 4 $/\$ $/\$
96		faccl 12466	. . . . . 6
97	66, 96	syl 17	. . . . 5 $/\$ $/\$
98	97	nncnd 10622	. . . 4 $/\$ $/\$
99	94	nnne0d 10651	. . . 4 $/\$ $/\$
100	97	nnne0d 10651	. . . 4 $/\$ $/\$
101	90, 95, 98, 99, 100	divcan5d 10406	. . 3 $/\$ $/\$
102	2, 70, 101	3eqtrd 2488	. 2 $/\$ $/\$
103		nnnn0 10873	. . . . 5
104	103	ad2antlr 732	. . . 4 $/\$ $/\$
105		nncn 10614	. . . . 5
106		nnne0 10639	. . . . 5
107	105, 106	div0d 10379	. . . 4
108	104, 93, 107	3syl 18	. . 3 $/\$ $/\$
109	3	adantl 468	. . . . 5 $/\$ $/\$ $/\$ $/\$
110		fvi 5920	. . . . . . 7
111		elfzelz 11797	. . . . . . . 8
112	111	zcnd 11038	. . . . . . 7
113	110, 112	eqeltrd 2528	. . . . . 6
114	113	adantl 468	. . . . 5 $/\$ $/\$ $/\$
115		mul02 9808	. . . . . 6
116	115	adantl 468	. . . . 5 $/\$ $/\$ $/\$
117		mul01 9809	. . . . . 6
118	117	adantl 468	. . . . 5 $/\$ $/\$ $/\$
119		simpr 463	. . . . . . . . 9 $/\$ $/\$
120		nn0uz 11190	. . . . . . . . . . . 12
121	104, 120	syl6eleq 2538	. . . . . . . . . . 11 $/\$ $/\$
122	72	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$
123		elfz5 11789	. . . . . . . . . . 11 $/\$
124	121, 122, 123	syl2anc 666	. . . . . . . . . 10 $/\$ $/\$
125		nn0re 10875	. . . . . . . . . . . 12
126	125	ad2antrr 731	. . . . . . . . . . 11 $/\$ $/\$
127		nnre 10613	. . . . . . . . . . . 12
128	127	ad2antlr 732	. . . . . . . . . . 11 $/\$ $/\$
129	126, 128	subge0d 10200	. . . . . . . . . 10 $/\$ $/\$
130	124, 129	bitr4d 260	. . . . . . . . 9 $/\$ $/\$
131	119, 130	mtbid 302	. . . . . . . 8 $/\$ $/\$
132	74	adantr 467	. . . . . . . . . 10 $/\$ $/\$
133	132	zred 11037	. . . . . . . . 9 $/\$ $/\$
134		0re 9640	. . . . . . . . 9
135		ltnle 9710	. . . . . . . . 9 $/\$
136	133, 134, 135	sylancl 667	. . . . . . . 8 $/\$ $/\$
137	131, 136	mpbird 236	. . . . . . 7 $/\$ $/\$
138		0z 10945	. . . . . . . 8
139		zltp1le 10983	. . . . . . . 8 $/\$
140	132, 138, 139	sylancl 667	. . . . . . 7 $/\$ $/\$
141	137, 140	mpbid 214	. . . . . 6 $/\$ $/\$
142		nn0ge0 10892	. . . . . . 7
143	142	ad2antrr 731	. . . . . 6 $/\$ $/\$
144		0zd 10946	. . . . . . 7 $/\$ $/\$
145	75	adantr 467	. . . . . . 7 $/\$ $/\$
146		elfz 11787	. . . . . . 7 $/\$ $/\$ $/\$
147	144, 145, 122, 146	syl3anc 1267	. . . . . 6 $/\$ $/\$ $/\$
148	141, 143, 147	mpbir2and 932	. . . . 5 $/\$ $/\$
149		simpll 759	. . . . 5 $/\$ $/\$
150		0cn 9632	. . . . . 6
151		fvi 5920	. . . . . 6
152	150, 151	mp1i 13	. . . . 5 $/\$ $/\$
153	109, 114, 116, 118, 148, 149, 152	seqz 12258	. . . 4 $/\$ $/\$
154	153	oveq1d 6303	. . 3 $/\$ $/\$
155		bcval3 12488	. . . . 5 $/\$ $/\$
156	20, 155	syl3an2 1301	. . . 4 $/\$ $/\$
157	156	3expa 1207	. . 3 $/\$ $/\$
158	108, 154, 157	3eqtr4rd 2495	. 2 $/\$ $/\$
159	102, 158	pm2.61dan 799	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886 class class class wbr 4401

cid 4743

cfv 5581 (class class class)co 6288

cc 9534

cr 9535

cc0 9536

c1 9537

caddc 9539

cmul 9541

clt 9672

cle 9673

cmin 9857

cdiv 10266

cn 10606

cn0 10866

cz 10934

cuz 11156

crp 11299

cfz 11781

cseq 12210

cfa 12456

cbc 12484

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-er 7360 df-en 7567 df-dom 7568 df-sdom 7569 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-n0 10867 df-z 10935 df-uz 11157 df-rp 11300 df-fz 11782 df-seq 12211 df-fac 12457 df-bc 12485

This theorem is referenced by: bcn2 12501

W3C validator