bcm1k - Metamath Proof Explorer

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

Theorem bcm1k 12373

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 11703	. . . . . . . . 9
2		nnuz 11129	. . . . . . . . 9
3	1, 2	syl6eleqr 2566	. . . . . . . 8
4	3	nnnn0d 10864	. . . . . . 7
5		faccl 12343	. . . . . . 7
6	4, 5	syl 16	. . . . . 6
7	6	nncnd 10564	. . . . 5
8		fznn0sub 11728	. . . . . . 7
9		nn0p1nn 10847	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11	10	nncnd 10564	. . . . 5
12	10	nnnn0d 10864	. . . . . . . 8
13		faccl 12343	. . . . . . . 8
14	12, 13	syl 16	. . . . . . 7
15		elfznn 11726	. . . . . . . 8
16		nnm1nn0 10849	. . . . . . . 8
17		faccl 12343	. . . . . . . 8
18	15, 16, 17	3syl 20	. . . . . . 7
19	14, 18	nnmulcld 10595	. . . . . 6
20		nncn 10556	. . . . . . 7
21		nnne0 10580	. . . . . . 7
22	20, 21	jca 532	. . . . . 6 $/\$
23	19, 22	syl 16	. . . . 5 $/\$
24	15	nncnd 10564	. . . . . 6
25	15	nnne0d 10592	. . . . . 6
26	24, 25	jca 532	. . . . 5 $/\$
27		divmuldiv 10256	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
28	7, 11, 23, 26, 27	syl22anc 1229	. . . 4
29		elfzel2 11698	. . . . . . . . . 10
30	29	zcnd 10979	. . . . . . . . 9
31		ax-1cn 9562	. . . . . . . . . 10
32	31	a1i 11	. . . . . . . . 9
33	30, 24, 32	subsubd 9970	. . . . . . . 8
34	33	fveq2d 5876	. . . . . . 7
35	34	oveq1d 6310	. . . . . 6
36	35	oveq2d 6311	. . . . 5
37	33	oveq1d 6310	. . . . 5
38	36, 37	oveq12d 6313	. . . 4
39		facp1 12338	. . . . . . . . 9
40	8, 39	syl 16	. . . . . . . 8
41	40	eqcomd 2475	. . . . . . 7
42		facnn2 12342	. . . . . . . 8
43	15, 42	syl 16	. . . . . . 7
44	41, 43	oveq12d 6313	. . . . . 6
45		faccl 12343	. . . . . . . . 9
46	8, 45	syl 16	. . . . . . . 8
47	46	nncnd 10564	. . . . . . 7
48	15	nnnn0d 10864	. . . . . . . . 9
49		faccl 12343	. . . . . . . . 9
50	48, 49	syl 16	. . . . . . . 8
51	50	nncnd 10564	. . . . . . 7
52	47, 51, 11	mul32d 9801	. . . . . 6
53	14	nncnd 10564	. . . . . . 7
54	18	nncnd 10564	. . . . . . 7
55	53, 54, 24	mulassd 9631	. . . . . 6
56	44, 52, 55	3eqtr4d 2518	. . . . 5
57	56	oveq2d 6311	. . . 4
58	28, 38, 57	3eqtr4d 2518	. . 3
59	7, 11	mulcomd 9629	. . . 4
60	46, 50	nnmulcld 10595	. . . . . 6
61	60	nncnd 10564	. . . . 5
62	61, 11	mulcomd 9629	. . . 4
63	59, 62	oveq12d 6313	. . 3
64	60	nnne0d 10592	. . . 4
65	10	nnne0d 10592	. . . 4
66	7, 61, 11, 64, 65	divcan5d 10358	. . 3
67	58, 63, 66	3eqtrrd 2513	. 2
68		0p1e1 10659	. . . . . 6
69	68	oveq1i 6305	. . . . 5
70		0z 10887	. . . . . 6
71		fzp1ss 11743	. . . . . 6
72	70, 71	ax-mp 5	. . . . 5
73	69, 72	eqsstr3i 3540	. . . 4
74	73	sseli 3505	. . 3
75		bcval2 12363	. . 3
76	74, 75	syl 16	. 2
77		npcan 9841	. . . . . . . 8 $/\$
78	30, 31, 77	sylancl 662	. . . . . . 7
79		peano2zm 10918	. . . . . . . 8
80		uzid 11108	. . . . . . . 8
81		peano2uz 11146	. . . . . . . 8
82	29, 79, 80, 81	4syl 21	. . . . . . 7
83	78, 82	eqeltrrd 2556	. . . . . 6
84		fzss2 11735	. . . . . 6
85	83, 84	syl 16	. . . . 5
86		elfzelz 11700	. . . . . . 7
87		elfzm1b 11768	. . . . . . 7 $/\$
88	86, 29, 87	syl2anc 661	. . . . . 6
89	88	ibi 241	. . . . 5
90	85, 89	sseldd 3510	. . . 4
91		bcval2 12363	. . . 4
92	90, 91	syl 16	. . 3
93	92	oveq1d 6310	. 2
94	67, 76, 93	3eqtr4d 2518	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1379

wcel 1767

wne 2662

wss 3481

cfv 5594 (class class class)co 6295

cc 9502

cc0 9504

c1 9505

caddc 9507

cmul 9509

cmin 9817

cdiv 10218

cn 10548

cn0 10807

cz 10876

cuz 11094

cfz 11684

cfa 12333

cbc 12360

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 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581

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 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-iun 4333 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6696 df-1st 6795 df-2nd 6796 df-recs 7054 df-rdg 7088 df-er 7323 df-en 7529 df-dom 7530 df-sdom 7531 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-div 10219 df-nn 10549 df-n0 10808 df-z 10877 df-uz 11095 df-fz 11685 df-seq 12088 df-fac 12334 df-bc 12361

This theorem is referenced by: bcp1nk 12375 bcpasc 12379 basellem5 23224 bpolydiflem 29743

W3C validator