bcm1k - Metamath Proof Explorer

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

Theorem bcm1k 11561

Description: The proportion of one binomial coefficient to another with

decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)

**Assertion**
Ref	Expression
bcm1k

**Proof of Theorem bcm1k**
Step	Hyp	Ref	Expression
1		elfzuz2 11018	. . . . . . . . 9
2		nnuz 10477	. . . . . . . . 9
3	1, 2	syl6eleqr 2495	. . . . . . . 8
4	3	nnnn0d 10230	. . . . . . 7
5		faccl 11531	. . . . . . 7
6	4, 5	syl 16	. . . . . 6
7	6	nncnd 9972	. . . . 5
8		fznn0sub 11041	. . . . . . 7
9		nn0p1nn 10215	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11	10	nncnd 9972	. . . . 5
12	10	nnnn0d 10230	. . . . . . . 8
13		faccl 11531	. . . . . . . 8
14	12, 13	syl 16	. . . . . . 7
15		elfznn 11036	. . . . . . . 8
16		nnm1nn0 10217	. . . . . . . 8
17		faccl 11531	. . . . . . . 8
18	15, 16, 17	3syl 19	. . . . . . 7
19	14, 18	nnmulcld 10003	. . . . . 6
20		nncn 9964	. . . . . . 7
21		nnne0 9988	. . . . . . 7
22	20, 21	jca 519	. . . . . 6 $/\$
23	19, 22	syl 16	. . . . 5 $/\$
24	15	nncnd 9972	. . . . . 6
25	15	nnne0d 10000	. . . . . 6
26	24, 25	jca 519	. . . . 5 $/\$
27		divmuldiv 9670	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
28	7, 11, 23, 26, 27	syl22anc 1185	. . . 4
29		elfzel2 11013	. . . . . . . . . 10
30	29	zcnd 10332	. . . . . . . . 9
31		ax-1cn 9004	. . . . . . . . . 10
32	31	a1i 11	. . . . . . . . 9
33	30, 24, 32	subsubd 9395	. . . . . . . 8
34	33	fveq2d 5691	. . . . . . 7
35	34	oveq1d 6055	. . . . . 6
36	35	oveq2d 6056	. . . . 5
37	33	oveq1d 6055	. . . . 5
38	36, 37	oveq12d 6058	. . . 4
39		facp1 11526	. . . . . . . . 9
40	8, 39	syl 16	. . . . . . . 8
41	40	eqcomd 2409	. . . . . . 7
42		facnn2 11530	. . . . . . . 8
43	15, 42	syl 16	. . . . . . 7
44	41, 43	oveq12d 6058	. . . . . 6
45		faccl 11531	. . . . . . . . 9
46	8, 45	syl 16	. . . . . . . 8
47	46	nncnd 9972	. . . . . . 7
48	15	nnnn0d 10230	. . . . . . . . 9
49		faccl 11531	. . . . . . . . 9
50	48, 49	syl 16	. . . . . . . 8
51	50	nncnd 9972	. . . . . . 7
52	47, 51, 11	mul32d 9232	. . . . . 6
53	14	nncnd 9972	. . . . . . 7
54	18	nncnd 9972	. . . . . . 7
55	53, 54, 24	mulassd 9067	. . . . . 6
56	44, 52, 55	3eqtr4d 2446	. . . . 5
57	56	oveq2d 6056	. . . 4
58	28, 38, 57	3eqtr4d 2446	. . 3
59	7, 11	mulcomd 9065	. . . 4
60	46, 50	nnmulcld 10003	. . . . . 6
61	60	nncnd 9972	. . . . 5
62	61, 11	mulcomd 9065	. . . 4
63	59, 62	oveq12d 6058	. . 3
64	60	nnne0d 10000	. . . 4
65	10	nnne0d 10000	. . . 4
66	7, 61, 11, 64, 65	divcan5d 9772	. . 3
67	58, 63, 66	3eqtrrd 2441	. 2
68		0p1e1 10049	. . . . . 6
69	68	oveq1i 6050	. . . . 5
70		0z 10249	. . . . . 6
71		fzp1ss 11054	. . . . . 6
72	70, 71	ax-mp 8	. . . . 5
73	69, 72	eqsstr3i 3339	. . . 4
74	73	sseli 3304	. . 3
75		bcval2 11551	. . 3
76	74, 75	syl 16	. 2
77		npcan 9270	. . . . . . . 8 $/\$
78	30, 31, 77	sylancl 644	. . . . . . 7
79		peano2zm 10276	. . . . . . . . 9
80	29, 79	syl 16	. . . . . . . 8
81		uzid 10456	. . . . . . . 8
82		peano2uz 10486	. . . . . . . 8
83	80, 81, 82	3syl 19	. . . . . . 7
84	78, 83	eqeltrrd 2479	. . . . . 6
85		fzss2 11048	. . . . . 6
86	84, 85	syl 16	. . . . 5
87		elfzelz 11015	. . . . . . 7
88		elfzm1b 11080	. . . . . . 7 $/\$
89	87, 29, 88	syl2anc 643	. . . . . 6
90	89	ibi 233	. . . . 5
91	86, 90	sseldd 3309	. . . 4
92		bcval2 11551	. . . 4
93	91, 92	syl 16	. . 3
94	93	oveq1d 6055	. 2
95	67, 76, 94	3eqtr4d 2446	1

Colors of variables: wff set class

Syntax hints:

wi 4

wb 177 $/\$ wa 359

wceq 1649

wcel 1721

wne 2567

wss 3280

cfv 5413 (class class class)co 6040

cc 8944

cc0 8946

c1 8947

caddc 8949

cmul 8951

cmin 9247

cdiv 9633

cn 9956

cn0 10177

cz 10238

cuz 10444

cfz 10999

cfa 11521

cbc 11548

This theorem is referenced by: bcp1nk 11563 bcpasc 11567 basellem5 20820 bpolydiflem 26004

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-div 9634 df-nn 9957 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-seq 11279 df-fac 11522 df-bc 11549

W3C validator