Metamath Proof Explorer

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 ) ) ) )