Metamath Proof Explorer

Theorem bcp1n

Description: The proportion of one binomial coefficient to another with N increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 elfz3nn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
2 facp1 ⊢ ( 𝑁 ∈ ℕ0 → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
3 1 2 syl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 + 1 ) ) = ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) )
4 fznn0sub ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
5 facp1 ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
6 4 5 syl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
7 1 nn0cnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℂ )
8 1cnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 1 ∈ ℂ )
9 elfznn0 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
10 9 nn0cnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℂ )
11 7 8 10 addsubd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) = ( ( 𝑁 − 𝐾 ) + 1 ) )
12 11 fveq2d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
13 11 oveq2d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
14 6 12 13 3eqtr4d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) )
15 14 oveq1d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) )
16 4 faccld ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
17 16 nncnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ )
18 nn0p1nn ⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
19 4 18 syl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
20 11 19 eqeltrd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℕ )
21 20 nncnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ )
22 9 faccld ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
23 22 nncnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
24 17 21 23 mul32d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) )
25 15 24 eqtrd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) )
26 3 25 oveq12d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
27 1 faccld ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℕ )
28 27 nncnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℂ )
29 nn0p1nn ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
30 1 29 syl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℕ )
31 30 nncnd ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ℂ )
32 16 22 nnmulcld ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
33 nncn ⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ )
34 nnne0 ⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 )
35 33 34 jca ⊢ ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) )
36 32 35 syl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) )
37 20 nnne0d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 )
38 21 37 jca ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 ) )
39 divmuldiv ⊢ ( ( ( ( ! ‘ 𝑁 ) ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℂ ) ∧ ( ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ ∧ ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 ) ∧ ( ( ( 𝑁 + 1 ) − 𝐾 ) ∈ ℂ ∧ ( ( 𝑁 + 1 ) − 𝐾 ) ≠ 0 ) ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
40 28 31 36 38 39 syl22anc ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( 𝑁 + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
41 26 40 eqtr4d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
42 fzelp1 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
43 bcval2 ⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
44 42 43 syl ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( ! ‘ ( 𝑁 + 1 ) ) / ( ( ! ‘ ( ( 𝑁 + 1 ) − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
45 bcval2 ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
46 45 oveq1d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )
47 41 44 46 3eqtr4d ⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 + 1 ) C 𝐾 ) = ( ( 𝑁 C 𝐾 ) · ( ( 𝑁 + 1 ) / ( ( 𝑁 + 1 ) − 𝐾 ) ) ) )