Theorem bcm1nt

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Scott Fenton, 23-Jun-2020)

	Ref	Expression
Assertion	bcm1nt	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bcp1n	⊢ ( 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) )
2	1	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) )
3		simpl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℕ )
4	3	nncnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑁 ∈ ℂ )
5		1cnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 1 ∈ ℂ )
6	4 5	npcand	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
7	6	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 − 1 ) + 1 ) C 𝐾 ) = ( 𝑁 C 𝐾 ) )
8	6	oveq1d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) = ( 𝑁 − 𝐾 ) )
9	6 8	oveq12d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) = ( 𝑁 / ( 𝑁 − 𝐾 ) ) )
10	9	oveq2d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( ( ( 𝑁 − 1 ) + 1 ) / ( ( ( 𝑁 − 1 ) + 1 ) − 𝐾 ) ) ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )
11	2 7 10	3eqtr3d	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑁 C 𝐾 ) = ( ( ( 𝑁 − 1 ) C 𝐾 ) · ( 𝑁 / ( 𝑁 − 𝐾 ) ) ) )