Metamath Proof Explorer


Theorem binomfallfaclem1

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

Ref Expression
Hypotheses binomfallfaclem.1 φ A
binomfallfaclem.2 φ B
binomfallfaclem.3 φ N 0
Assertion binomfallfaclem1 φ K 0 N ( N K) A N K _ B K + 1 _

Proof

Step Hyp Ref Expression
1 binomfallfaclem.1 φ A
2 binomfallfaclem.2 φ B
3 binomfallfaclem.3 φ N 0
4 elfzelz K 0 N K
5 bccl N 0 K ( N K) 0
6 3 4 5 syl2an φ K 0 N ( N K) 0
7 6 nn0cnd φ K 0 N ( N K)
8 fznn0sub K 0 N N K 0
9 fallfaccl A N K 0 A N K _
10 1 8 9 syl2an φ K 0 N A N K _
11 elfznn0 K 0 N K 0
12 peano2nn0 K 0 K + 1 0
13 11 12 syl K 0 N K + 1 0
14 fallfaccl B K + 1 0 B K + 1 _
15 2 13 14 syl2an φ K 0 N B K + 1 _
16 10 15 mulcld φ K 0 N A N K _ B K + 1 _
17 7 16 mulcld φ K 0 N ( N K) A N K _ B K + 1 _