Theorem bcp1nk

Description: The proportion of one binomial coefficient to another with N and K increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Assertion	bcp1nk	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C ( 𝐾 + 1 ) ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( 𝐾 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzel1	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 0 ∈ ℤ )
2		elfzel2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
3		elfzelz	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
4		1zzd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 1 ∈ ℤ )
5		fzaddel	⊢ ( ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 1 ∈ ℤ ) ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
6	1 2 3 4 5	syl22anc	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐾 + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
7	6	ibi	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) )
8		1e0p1	⊢ 1 = ( 0 + 1 )
9	8	oveq1i	⊢ ( 1 ... ( 𝑁 + 1 ) ) = ( ( 0 + 1 ) ... ( 𝑁 + 1 ) )
10	7 9	eleqtrrdi	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) )
11		bcm1k	⊢ ( ( 𝐾 + 1 ) ∈ ( 1 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) C ( 𝐾 + 1 ) ) = ( ( ( 𝑁 + 1 ) C ( ( 𝐾 + 1 ) − 1 ) ) · ( ( ( 𝑁 + 1 ) − ( ( 𝐾 + 1 ) − 1 ) ) / ( 𝐾 + 1 ) ) ) )
12	10 11	syl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C ( 𝐾 + 1 ) ) = ( ( ( 𝑁 + 1 ) C ( ( 𝐾 + 1 ) − 1 ) ) · ( ( ( 𝑁 + 1 ) − ( ( 𝐾 + 1 ) − 1 ) ) / ( 𝐾 + 1 ) ) ) )
13	3	zcnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℂ )
14		ax-1cn	⊢ 1 ∈ ℂ
15		pncan	⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
16	13 14 15	sylancl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
17	16	oveq2d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C ( ( 𝐾 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) C 𝐾 ) )
18		bcp1n	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
19	17 18	eqtrd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C ( ( 𝐾 + 1 ) − 1 ) ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
20	16	oveq2d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − ( ( 𝐾 + 1 ) − 1 ) ) = ( ( 𝑁 + 1 ) − 𝐾 ) )
21	20	oveq1d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − ( ( 𝐾 + 1 ) − 1 ) ) / ( 𝐾 + 1 ) ) = ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) )
22	19 21	oveq12d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) C ( ( 𝐾 + 1 ) − 1 ) ) · ( ( ( 𝑁 + 1 ) − ( ( 𝐾 + 1 ) − 1 ) ) / ( 𝐾 + 1 ) ) ) = ( ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ) )
23		bcrpcl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℝ+ )
24	23	rpcnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) ∈ ℂ )
25	2	peano2zd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℤ )
26	25	zred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℝ )
27	3	zred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℝ )
28	2	zred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℝ )
29		elfzle2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ≤ 𝑁 )
30	28	ltp1d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 < ( 𝑁 + 1 ) )
31	27 28 26 29 30	lelttrd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 < ( 𝑁 + 1 ) )
32		znnsub	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝐾 < ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℕ ) )
33	3 25 32	syl2anc	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 < ( 𝑁 + 1 ) ↔ ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℕ ) )
34	31 33	mpbid	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℕ )
35	26 34	nndivred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ∈ ℝ )
36	35	recnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ∈ ℂ )
37	34	nnred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℝ )
38		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
39		nn0p1nn	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ )
40	38 39	syl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ℕ )
41	37 40	nndivred	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ∈ ℝ )
42	41	recnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ∈ ℂ )
43	24 36 42	mulassd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ) = ( ( 𝑁 C 𝐾 ) · ( ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ) ) )
44	25	zcnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℂ )
45	34	nncnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ )
46	40	nncnd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ℂ )
47	34	nnne0d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 )
48	40	nnne0d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + 1 ) ≠ 0 )
49	44 45 46 47 48	dmdcan2d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ) = ( ( 𝑁 + 1 ) / ( 𝐾 + 1 ) ) )
50	49	oveq2d	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) · ( ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ) ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( 𝐾 + 1 ) ) ) )
51	43 50	eqtrd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) · ( ( ( 𝑁 + 1 ) − 𝐾 ) / ( 𝐾 + 1 ) ) ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( 𝐾 + 1 ) ) ) )
52	22 51	eqtrd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) C ( ( 𝐾 + 1 ) − 1 ) ) · ( ( ( 𝑁 + 1 ) − ( ( 𝐾 + 1 ) − 1 ) ) / ( 𝐾 + 1 ) ) ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( 𝐾 + 1 ) ) ) )
53	12 52	eqtrd	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C ( 𝐾 + 1 ) ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( 𝐾 + 1 ) ) ) )