bcm1k - Metamath Proof Explorer

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

Theorem bcm1k 12212

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 11577	. . . . . . . . 9
2		nnuz 11011	. . . . . . . . 9
3	1, 2	syl6eleqr 2553	. . . . . . . 8
4	3	nnnn0d 10751	. . . . . . 7
5		faccl 12182	. . . . . . 7
6	4, 5	syl 16	. . . . . 6
7	6	nncnd 10453	. . . . 5
8		fznn0sub 11608	. . . . . . 7
9		nn0p1nn 10734	. . . . . . 7
10	8, 9	syl 16	. . . . . 6
11	10	nncnd 10453	. . . . 5
12	10	nnnn0d 10751	. . . . . . . 8
13		faccl 12182	. . . . . . . 8
14	12, 13	syl 16	. . . . . . 7
15		elfznn 11599	. . . . . . . 8
16		nnm1nn0 10736	. . . . . . . 8
17		faccl 12182	. . . . . . . 8
18	15, 16, 17	3syl 20	. . . . . . 7
19	14, 18	nnmulcld 10484	. . . . . 6
20		nncn 10445	. . . . . . 7
21		nnne0 10469	. . . . . . 7
22	20, 21	jca 532	. . . . . 6 $/\$
23	19, 22	syl 16	. . . . 5 $/\$
24	15	nncnd 10453	. . . . . 6
25	15	nnne0d 10481	. . . . . 6
26	24, 25	jca 532	. . . . 5 $/\$
27		divmuldiv 10146	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
28	7, 11, 23, 26, 27	syl22anc 1220	. . . 4
29		elfzel2 11572	. . . . . . . . . 10
30	29	zcnd 10863	. . . . . . . . 9
31		ax-1cn 9455	. . . . . . . . . 10
32	31	a1i 11	. . . . . . . . 9
33	30, 24, 32	subsubd 9862	. . . . . . . 8
34	33	fveq2d 5806	. . . . . . 7
35	34	oveq1d 6218	. . . . . 6
36	35	oveq2d 6219	. . . . 5
37	33	oveq1d 6218	. . . . 5
38	36, 37	oveq12d 6221	. . . 4
39		facp1 12177	. . . . . . . . 9
40	8, 39	syl 16	. . . . . . . 8
41	40	eqcomd 2462	. . . . . . 7
42		facnn2 12181	. . . . . . . 8
43	15, 42	syl 16	. . . . . . 7
44	41, 43	oveq12d 6221	. . . . . 6
45		faccl 12182	. . . . . . . . 9
46	8, 45	syl 16	. . . . . . . 8
47	46	nncnd 10453	. . . . . . 7
48	15	nnnn0d 10751	. . . . . . . . 9
49		faccl 12182	. . . . . . . . 9
50	48, 49	syl 16	. . . . . . . 8
51	50	nncnd 10453	. . . . . . 7
52	47, 51, 11	mul32d 9694	. . . . . 6
53	14	nncnd 10453	. . . . . . 7
54	18	nncnd 10453	. . . . . . 7
55	53, 54, 24	mulassd 9524	. . . . . 6
56	44, 52, 55	3eqtr4d 2505	. . . . 5
57	56	oveq2d 6219	. . . 4
58	28, 38, 57	3eqtr4d 2505	. . 3
59	7, 11	mulcomd 9522	. . . 4
60	46, 50	nnmulcld 10484	. . . . . 6
61	60	nncnd 10453	. . . . 5
62	61, 11	mulcomd 9522	. . . 4
63	59, 62	oveq12d 6221	. . 3
64	60	nnne0d 10481	. . . 4
65	10	nnne0d 10481	. . . 4
66	7, 61, 11, 64, 65	divcan5d 10248	. . 3
67	58, 63, 66	3eqtrrd 2500	. 2
68		0p1e1 10548	. . . . . 6
69	68	oveq1i 6213	. . . . 5
70		0z 10772	. . . . . 6
71		fzp1ss 11627	. . . . . 6
72	70, 71	ax-mp 5	. . . . 5
73	69, 72	eqsstr3i 3498	. . . 4
74	73	sseli 3463	. . 3
75		bcval2 12202	. . 3
76	74, 75	syl 16	. 2
77		npcan 9734	. . . . . . . 8 $/\$
78	30, 31, 77	sylancl 662	. . . . . . 7
79		peano2zm 10803	. . . . . . . 8
80		uzid 10990	. . . . . . . 8
81		peano2uz 11023	. . . . . . . 8
82	29, 79, 80, 81	4syl 21	. . . . . . 7
83	78, 82	eqeltrrd 2543	. . . . . 6
84		fzss2 11619	. . . . . 6
85	83, 84	syl 16	. . . . 5
86		elfzelz 11574	. . . . . . 7
87		elfzm1b 11659	. . . . . . 7 $/\$
88	86, 29, 87	syl2anc 661	. . . . . 6
89	88	ibi 241	. . . . 5
90	85, 89	sseldd 3468	. . . 4
91		bcval2 12202	. . . 4
92	90, 91	syl 16	. . 3
93	92	oveq1d 6218	. 2
94	67, 76, 93	3eqtr4d 2505	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1370

wcel 1758

wne 2648

wss 3439

cfv 5529 (class class class)co 6203

cc 9395

cc0 9397

c1 9398

caddc 9400

cmul 9402

cmin 9710

cdiv 10108

cn 10437

cn0 10694

cz 10761

cuz 10976

cfz 11558

cfa 12172

cbc 12199

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-sep 4524 ax-nul 4532 ax-pow 4581 ax-pr 4642 ax-un 6485 ax-cnex 9453 ax-resscn 9454 ax-1cn 9455 ax-icn 9456 ax-addcl 9457 ax-addrcl 9458 ax-mulcl 9459 ax-mulrcl 9460 ax-mulcom 9461 ax-addass 9462 ax-mulass 9463 ax-distr 9464 ax-i2m1 9465 ax-1ne0 9466 ax-1rid 9467 ax-rnegex 9468 ax-rrecex 9469 ax-cnre 9470 ax-pre-lttri 9471 ax-pre-lttrn 9472 ax-pre-ltadd 9473 ax-pre-mulgt0 9474

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rmo 2807 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3399 df-dif 3442 df-un 3444 df-in 3446 df-ss 3453 df-pss 3455 df-nul 3749 df-if 3903 df-pw 3973 df-sn 3989 df-pr 3991 df-tp 3993 df-op 3995 df-uni 4203 df-iun 4284 df-br 4404 df-opab 4462 df-mpt 4463 df-tr 4497 df-eprel 4743 df-id 4747 df-po 4752 df-so 4753 df-fr 4790 df-we 4792 df-ord 4833 df-on 4834 df-lim 4835 df-suc 4836 df-xp 4957 df-rel 4958 df-cnv 4959 df-co 4960 df-dm 4961 df-rn 4962 df-res 4963 df-ima 4964 df-iota 5492 df-fun 5531 df-fn 5532 df-f 5533 df-f1 5534 df-fo 5535 df-f1o 5536 df-fv 5537 df-riota 6164 df-ov 6206 df-oprab 6207 df-mpt2 6208 df-om 6590 df-1st 6690 df-2nd 6691 df-recs 6945 df-rdg 6979 df-er 7214 df-en 7424 df-dom 7425 df-sdom 7426 df-pnf 9535 df-mnf 9536 df-xr 9537 df-ltxr 9538 df-le 9539 df-sub 9712 df-neg 9713 df-div 10109 df-nn 10438 df-n0 10695 df-z 10762 df-uz 10977 df-fz 11559 df-seq 11928 df-fac 12173 df-bc 12200

This theorem is referenced by: bcp1nk 12214 bcpasc 12218 basellem5 22565 bpolydiflem 28364

W3C validator