bcm1k - Metamath Proof Explorer

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

Theorem bcm1k 12367

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 11695	. . . . . . . . 9
2		nnuz 11120	. . . . . . . . 9
3	1, 2	syl6eleqr 2540	. . . . . . . 8
4	3	nnnn0d 10853	. . . . . . 7
5		faccl 12337	. . . . . . 7
6	4, 5	syl 16	. . . . . 6
7	6	nncnd 10553	. . . . 5
8		fznn0sub 11720	. . . . . . 7
9		nn0p1nn 10836	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11	10	nncnd 10553	. . . . 5
12	10	nnnn0d 10853	. . . . . . . 8
13		faccl 12337	. . . . . . . 8
14	12, 13	syl 16	. . . . . . 7
15		elfznn 11718	. . . . . . . 8
16		nnm1nn0 10838	. . . . . . . 8
17		faccl 12337	. . . . . . . 8
18	15, 16, 17	3syl 20	. . . . . . 7
19	14, 18	nnmulcld 10584	. . . . . 6
20		nncn 10545	. . . . . . 7
21		nnne0 10569	. . . . . . 7
22	20, 21	jca 532	. . . . . 6 $/\$
23	19, 22	syl 16	. . . . 5 $/\$
24	15	nncnd 10553	. . . . . 6
25	15	nnne0d 10581	. . . . . 6
26	24, 25	jca 532	. . . . 5 $/\$
27		divmuldiv 10245	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
28	7, 11, 23, 26, 27	syl22anc 1228	. . . 4
29		elfzel2 11690	. . . . . . . . . 10
30	29	zcnd 10970	. . . . . . . . 9
31		1cnd 9610	. . . . . . . . 9
32	30, 24, 31	subsubd 9959	. . . . . . . 8
33	32	fveq2d 5856	. . . . . . 7
34	33	oveq1d 6292	. . . . . 6
35	34	oveq2d 6293	. . . . 5
36	32	oveq1d 6292	. . . . 5
37	35, 36	oveq12d 6295	. . . 4
38		facp1 12332	. . . . . . . . 9
39	8, 38	syl 16	. . . . . . . 8
40	39	eqcomd 2449	. . . . . . 7
41		facnn2 12336	. . . . . . . 8
42	15, 41	syl 16	. . . . . . 7
43	40, 42	oveq12d 6295	. . . . . 6
44		faccl 12337	. . . . . . . . 9
45	8, 44	syl 16	. . . . . . . 8
46	45	nncnd 10553	. . . . . . 7
47	15	nnnn0d 10853	. . . . . . . . 9
48		faccl 12337	. . . . . . . . 9
49	47, 48	syl 16	. . . . . . . 8
50	49	nncnd 10553	. . . . . . 7
51	46, 50, 11	mul32d 9788	. . . . . 6
52	14	nncnd 10553	. . . . . . 7
53	18	nncnd 10553	. . . . . . 7
54	52, 53, 24	mulassd 9617	. . . . . 6
55	43, 51, 54	3eqtr4d 2492	. . . . 5
56	55	oveq2d 6293	. . . 4
57	28, 37, 56	3eqtr4d 2492	. . 3
58	7, 11	mulcomd 9615	. . . 4
59	45, 49	nnmulcld 10584	. . . . . 6
60	59	nncnd 10553	. . . . 5
61	60, 11	mulcomd 9615	. . . 4
62	58, 61	oveq12d 6295	. . 3
63	59	nnne0d 10581	. . . 4
64	10	nnne0d 10581	. . . 4
65	7, 60, 11, 63, 64	divcan5d 10347	. . 3
66	57, 62, 65	3eqtrrd 2487	. 2
67		0p1e1 10648	. . . . . 6
68	67	oveq1i 6287	. . . . 5
69		0z 10876	. . . . . 6
70		fzp1ss 11735	. . . . . 6
71	69, 70	ax-mp 5	. . . . 5
72	68, 71	eqsstr3i 3517	. . . 4
73	72	sseli 3482	. . 3
74		bcval2 12357	. . 3
75	73, 74	syl 16	. 2
76		ax-1cn 9548	. . . . . . . 8
77		npcan 9829	. . . . . . . 8 $/\$
78	30, 76, 77	sylancl 662	. . . . . . 7
79		peano2zm 10908	. . . . . . . 8
80		uzid 11099	. . . . . . . 8
81		peano2uz 11138	. . . . . . . 8
82	29, 79, 80, 81	4syl 21	. . . . . . 7
83	78, 82	eqeltrrd 2530	. . . . . 6
84		fzss2 11727	. . . . . 6
85	83, 84	syl 16	. . . . 5
86		elfzmlbm 11788	. . . . 5
87	85, 86	sseldd 3487	. . . 4
88		bcval2 12357	. . . 4
89	87, 88	syl 16	. . 3
90	89	oveq1d 6292	. 2
91	66, 75, 90	3eqtr4d 2492	1

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1381

wcel 1802

wne 2636

wss 3458

cfv 5574 (class class class)co 6277

cc 9488

cc0 9490

c1 9491

caddc 9493

cmul 9495

cmin 9805

cdiv 10207

cn 10537

cn0 10796

cz 10865

cuz 11085

cfz 11676

cfa 12327

cbc 12354

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rmo 2799 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-iun 4313 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6682 df-1st 6781 df-2nd 6782 df-recs 7040 df-rdg 7074 df-er 7309 df-en 7515 df-dom 7516 df-sdom 7517 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9807 df-neg 9808 df-div 10208 df-nn 10538 df-n0 10797 df-z 10866 df-uz 11086 df-fz 11677 df-seq 12082 df-fac 12328 df-bc 12355

This theorem is referenced by: bcp1nk 12369 bcpasc 12373 basellem5 23223 bpolydiflem 29784

W3C validator