Theorem binomfallfaclem1

Description: Lemma for binomfallfac . Closure law. (Contributed by Scott Fenton, 13-Mar-2018)

	Ref	Expression
Hypotheses	binomfallfaclem.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	binomfallfaclem.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	binomfallfaclem.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	binomfallfaclem1	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝐾 ) ) · ( 𝐵 FallFac ( 𝐾 + 1 ) ) ) ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		binomfallfaclem.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		binomfallfaclem.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		binomfallfaclem.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		elfzelz	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℤ )
5		bccl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
6	3 4 5	syl2an	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) ∈ ℕ0 )
7	6	nn0cnd	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝐾 ) ∈ ℂ )
8		fznn0sub	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
9		fallfaccl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 − 𝐾 ) ∈ ℕ0 ) → ( 𝐴 FallFac ( 𝑁 − 𝐾 ) ) ∈ ℂ )
10	1 8 9	syl2an	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐴 FallFac ( 𝑁 − 𝐾 ) ) ∈ ℂ )
11		elfznn0	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
12		peano2nn0	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
13	11 12	syl	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ℕ0 )
14		fallfaccl	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐾 + 1 ) ∈ ℕ0 ) → ( 𝐵 FallFac ( 𝐾 + 1 ) ) ∈ ℂ )
15	2 13 14	syl2an	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( 𝐵 FallFac ( 𝐾 + 1 ) ) ∈ ℂ )
16	10 15	mulcld	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐴 FallFac ( 𝑁 − 𝐾 ) ) · ( 𝐵 FallFac ( 𝐾 + 1 ) ) ) ∈ ℂ )
17	7 16	mulcld	⊢ ( ( 𝜑 ∧ 𝐾 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝐾 ) · ( ( 𝐴 FallFac ( 𝑁 − 𝐾 ) ) · ( 𝐵 FallFac ( 𝐾 + 1 ) ) ) ) ∈ ℂ )