This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) ∈ ℂ )