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 φN0
Assertion binomfallfaclem1 φK0N(NK)ANK_BK+1_

Proof

Step Hyp Ref Expression
1 binomfallfaclem.1 φA
2 binomfallfaclem.2 φB
3 binomfallfaclem.3 φN0
4 elfzelz K0NK
5 bccl N0K(NK)0
6 3 4 5 syl2an φK0N(NK)0
7 6 nn0cnd φK0N(NK)
8 fznn0sub K0NNK0
9 fallfaccl ANK0ANK_
10 1 8 9 syl2an φK0NANK_
11 elfznn0 K0NK0
12 peano2nn0 K0K+10
13 11 12 syl K0NK+10
14 fallfaccl BK+10BK+1_
15 2 13 14 syl2an φK0NBK+1_
16 10 15 mulcld φK0NANK_BK+1_
17 7 16 mulcld φK0N(NK)ANK_BK+1_