Description: Lemma for binomfallfac . Closure law. (Contributed by Scott Fenton, 13-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | binomfallfaclem.1 | |
|
binomfallfaclem.2 | |
||
binomfallfaclem.3 | |
||
Assertion | binomfallfaclem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | binomfallfaclem.1 | |
|
2 | binomfallfaclem.2 | |
|
3 | binomfallfaclem.3 | |
|
4 | elfzelz | |
|
5 | bccl | |
|
6 | 3 4 5 | syl2an | |
7 | 6 | nn0cnd | |
8 | fznn0sub | |
|
9 | fallfaccl | |
|
10 | 1 8 9 | syl2an | |
11 | elfznn0 | |
|
12 | peano2nn0 | |
|
13 | 11 12 | syl | |
14 | fallfaccl | |
|
15 | 2 13 14 | syl2an | |
16 | 10 15 | mulcld | |
17 | 7 16 | mulcld | |