binomfallfaclem1

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

	Ref	Expression
Hypotheses	binomfallfaclem.1	$⊢ φ \to A \in ℂ$
	binomfallfaclem.2	$⊢ φ \to B \in ℂ$
	binomfallfaclem.3	$⊢ φ \to N \in ℕ_{0}$
Assertion	binomfallfaclem1	$⊢ (φ \land K \in (0 \dots N)) \to (\binom{N}{K}) (A^{\underline{(N - K)}}) (B^{\underline{(K + 1)}}) \in ℂ$

Step	Hyp	Ref	Expression
1		binomfallfaclem.1	$⊢ φ \to A \in ℂ$
2		binomfallfaclem.2	$⊢ φ \to B \in ℂ$
3		binomfallfaclem.3	$⊢ φ \to N \in ℕ_{0}$
4		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
5		bccl	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) \in ℕ_{0}$
6	3 4 5	syl2an	$⊢ (φ \land K \in (0 \dots N)) \to (\binom{N}{K}) \in ℕ_{0}$
7	6	nn0cnd	$⊢ (φ \land K \in (0 \dots N)) \to (\binom{N}{K}) \in ℂ$
8		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
9		fallfaccl	$⊢ (A \in ℂ \land N - K \in ℕ_{0}) \to A^{\underline{(N - K)}} \in ℂ$
10	1 8 9	syl2an	$⊢ (φ \land K \in (0 \dots N)) \to A^{\underline{(N - K)}} \in ℂ$
11		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
12		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
13	11 12	syl	$⊢ K \in (0 \dots N) \to K + 1 \in ℕ_{0}$
14		fallfaccl	$⊢ (B \in ℂ \land K + 1 \in ℕ_{0}) \to B^{\underline{(K + 1)}} \in ℂ$
15	2 13 14	syl2an	$⊢ (φ \land K \in (0 \dots N)) \to B^{\underline{(K + 1)}} \in ℂ$
16	10 15	mulcld	$⊢ (φ \land K \in (0 \dots N)) \to (A^{\underline{(N - K)}}) (B^{\underline{(K + 1)}}) \in ℂ$
17	7 16	mulcld	$⊢ (φ \land K \in (0 \dots N)) \to (\binom{N}{K}) (A^{\underline{(N - K)}}) (B^{\underline{(K + 1)}}) \in ℂ$

Metamath Proof Explorer