Metamath Proof Explorer

Theorem bccp1k

Description: Generalized binomial coefficient: C choose ( K + 1 ) . (Contributed by Steve Rodriguez, 22-Apr-2020)

Ref Expression
Hypotheses bccval.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
bccval.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion bccp1k ( 𝜑 → ( 𝐶 C𝑐 ( 𝐾 + 1 ) ) = ( ( 𝐶 C𝑐 𝐾 ) · ( ( 𝐶 − 𝐾 ) / ( 𝐾 + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 bccval.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 bccval.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 fallfacp1 ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐶 FallFac ( 𝐾 + 1 ) ) = ( ( 𝐶 FallFac 𝐾 ) · ( 𝐶 − 𝐾 ) ) )
4 1 2 3 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac ( 𝐾 + 1 ) ) = ( ( 𝐶 FallFac 𝐾 ) · ( 𝐶 − 𝐾 ) ) )
5 facp1 ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ ( 𝐾 + 1 ) ) = ( ( ! ‘ 𝐾 ) · ( 𝐾 + 1 ) ) )
6 2 5 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝐾 + 1 ) ) = ( ( ! ‘ 𝐾 ) · ( 𝐾 + 1 ) ) )
7 4 6 oveq12d ⊢ ( 𝜑 → ( ( 𝐶 FallFac ( 𝐾 + 1 ) ) / ( ! ‘ ( 𝐾 + 1 ) ) ) = ( ( ( 𝐶 FallFac 𝐾 ) · ( 𝐶 − 𝐾 ) ) / ( ( ! ‘ 𝐾 ) · ( 𝐾 + 1 ) ) ) )
8 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
9 2 8 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
10 1 9 bccval ⊢ ( 𝜑 → ( 𝐶 C𝑐 ( 𝐾 + 1 ) ) = ( ( 𝐶 FallFac ( 𝐾 + 1 ) ) / ( ! ‘ ( 𝐾 + 1 ) ) ) )
11 fallfaccl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
13 faccl ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
14 2 13 syl ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℕ )
15 14 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℂ )
16 2 nn0cnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
17 1 16 subcld ⊢ ( 𝜑 → ( 𝐶 − 𝐾 ) ∈ ℂ )
18 9 nn0cnd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℂ )
19 14 nnne0d ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ≠ 0 )
20 nn0p1nn ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ )
21 2 20 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ )
22 21 nnne0d ⊢ ( 𝜑 → ( 𝐾 + 1 ) ≠ 0 )
23 12 15 17 18 19 22 divmuldivd ⊢ ( 𝜑 → ( ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) · ( ( 𝐶 − 𝐾 ) / ( 𝐾 + 1 ) ) ) = ( ( ( 𝐶 FallFac 𝐾 ) · ( 𝐶 − 𝐾 ) ) / ( ( ! ‘ 𝐾 ) · ( 𝐾 + 1 ) ) ) )
24 7 10 23 3eqtr4d ⊢ ( 𝜑 → ( 𝐶 C𝑐 ( 𝐾 + 1 ) ) = ( ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) · ( ( 𝐶 − 𝐾 ) / ( 𝐾 + 1 ) ) ) )
25 1 2 bccval ⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
26 25 oveq1d ⊢ ( 𝜑 → ( ( 𝐶 C𝑐 𝐾 ) · ( ( 𝐶 − 𝐾 ) / ( 𝐾 + 1 ) ) ) = ( ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) · ( ( 𝐶 − 𝐾 ) / ( 𝐾 + 1 ) ) ) )
27 24 26 eqtr4d ⊢ ( 𝜑 → ( 𝐶 C𝑐 ( 𝐾 + 1 ) ) = ( ( 𝐶 C𝑐 𝐾 ) · ( ( 𝐶 − 𝐾 ) / ( 𝐾 + 1 ) ) ) )