Description: Lemma for prmgaplcm : The least common multiple of all positive integers less than or equal to a number plus an integer greater than 1 and less then or equal to the number is divisible by that integer. (Contributed by AV, 14-Aug-2020) (Revised by AV, 27-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | prmgaplcmlem1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elfzelz | |
|
2 | 1 | adantl | |
3 | fzssz | |
|
4 | fzfi | |
|
5 | 3 4 | pm3.2i | |
6 | lcmfcl | |
|
7 | 6 | nn0zd | |
8 | 5 7 | mp1i | |
9 | breq1 | |
|
10 | dvdslcmf | |
|
11 | 5 10 | mp1i | |
12 | 2eluzge1 | |
|
13 | fzss1 | |
|
14 | 12 13 | mp1i | |
15 | 14 | sselda | |
16 | 9 11 15 | rspcdva | |
17 | iddvds | |
|
18 | 1 17 | syl | |
19 | 18 | adantl | |
20 | 2 8 2 16 19 | dvds2addd | |