Theorem bcm1n

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016)

	Ref	Expression
Assertion	bcm1n	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) / ( 𝑁 C 𝐾 ) ) = ( ( 𝑁 − 𝐾 ) / 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		bcp1n	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) )
2		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3	2	zcnd	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
4	3	adantl	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
5		1cnd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 1 ∈ ℂ )
6	4 5	npcand	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7	6	oveq1d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( 𝑁 C 𝐾 ) )
8	6	oveq1d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) = ( 𝑁 − 𝐾 ) )
9	6 8	oveq12d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) )
10	9	oveq2d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
11	7 10	eqeq12d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
12	1 11	imbitrid	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
13	12	3impia	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
14	13	3anidm13	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
15		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ℕ0 )
16	15	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℕ0 )
17		simpr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ )
18	17	nnnn0d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℕ0 )
19		elfzelz	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ℤ )
20	19	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℤ )
21	20	zred	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℝ )
22	2	adantl	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
23	22	zred	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
24		elfzle2	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ≤ ( 𝑁 − 1 ) )
25	24	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ≤ ( 𝑁 − 1 ) )
26		zltlem1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ 𝐾 ≤ ( 𝑁 − 1 ) ) )
27	19 2 26	syl2an	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 < 𝑁 ↔ 𝐾 ≤ ( 𝑁 − 1 ) ) )
28	25 27	mpbird	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 < 𝑁 )
29	21 23 28	ltled	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ≤ 𝑁 )
30		elfz2nn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁 ) )
31	16 18 29 30	syl3anbrc	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
32		bcrpcl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
33	31 32	syl	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
34	33	rpcnd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ∈ ℂ )
35	19	zcnd	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝐾 ∈ ℂ )
36	35	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 ∈ ℂ )
37	4 36	subcld	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ∈ ℂ )
38	36 4	negsubdi2d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → - ( 𝐾 − 𝑁 ) = ( 𝑁 − 𝐾 ) )
39	21 23	resubcld	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) ∈ ℝ )
40	39	recnd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) ∈ ℂ )
41	4	addlidd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 0 + 𝑁 ) = 𝑁 )
42	28 41	breqtrrd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝐾 < ( 0 + 𝑁 ) )
43		0red	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 0 ∈ ℝ )
44	21 23 43	ltsubaddd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝐾 − 𝑁 ) < 0 ↔ 𝐾 < ( 0 + 𝑁 ) ) )
45	42 44	mpbird	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) < 0 )
46	45	lt0ne0d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 − 𝑁 ) ≠ 0 )
47	40 46	negne0d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → - ( 𝐾 − 𝑁 ) ≠ 0 )
48	38 47	eqnetrrd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 − 𝐾 ) ≠ 0 )
49	4 37 48	divcld	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 / ( 𝑁 − 𝐾 ) ) ∈ ℂ )
50		bcrpcl	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℝ+ )
51	50	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℝ+ )
52	51	rpcnne0d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 ) )
53		divmul2	⊢ ( ( ( 𝑁 C 𝐾 ) ∈ ℂ ∧ ( 𝑁 / ( 𝑁 − 𝐾 ) ) ∈ ℂ ∧ ( ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 ) ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
54	34 49 52 53	syl3anc	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) ↔ ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) ) )
55	14 54	mpbird	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) )
56	55	oveq2d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 1 / ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) ) = ( 1 / ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
57	51	rpcnd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℂ )
58		bccl2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℕ )
59	31 58	syl	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ∈ ℕ )
60	59	nnne0d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 𝑁 C 𝐾 ) ≠ 0 )
61		bccl2	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) C 𝐾 ) ∈ ℕ )
62	61	nnne0d	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 )
63	62	adantr	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( 𝑁 − 1 ) C 𝐾 ) ≠ 0 )
64	34 57 60 63	recdivd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 1 / ( ( 𝑁 C 𝐾 ) / ( ( 𝑁 − 1 ) C 𝐾 ) ) ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) / ( 𝑁 C 𝐾 ) ) )
65	17	nnne0d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≠ 0 )
66	4 37 65 48	recdivd	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( 1 / ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) = ( ( 𝑁 − 𝐾 ) / 𝑁 ) )
67	56 64 66	3eqtr3d	⊢ ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) / ( 𝑁 C 𝐾 ) ) = ( ( 𝑁 − 𝐾 ) / 𝑁 ) )