Description: Lemma for prmgap : The factorial of a number plus an integer greater than 1 and less then or equal to the number is divisible by that integer. (Contributed by AV, 13-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | prmgaplem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzelz | |
|
2 | 1 | adantl | |
3 | nnnn0 | |
|
4 | 3 | faccld | |
5 | 4 | nnzd | |
6 | 5 | adantr | |
7 | elfzuz | |
|
8 | eluz2nn | |
|
9 | 7 8 | syl | |
10 | elfzuz3 | |
|
11 | 9 10 | jca | |
12 | 11 | adantl | |
13 | dvdsfac | |
|
14 | 12 13 | syl | |
15 | iddvds | |
|
16 | 1 15 | syl | |
17 | 16 | adantl | |
18 | 2 6 2 14 17 | dvds2addd | |