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