Description: The least common multiple of all positive integers less than or equal to an integer is less than or equal to the factorial of the integer. (Contributed by AV, 16-Aug-2020) (Revised by AV, 27-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | lcmflefac | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fzssz | |
|
2 | 1 | a1i | |
3 | fzfid | |
|
4 | 0nelfz1 | |
|
5 | 4 | a1i | |
6 | 2 3 5 | 3jca | |
7 | nnnn0 | |
|
8 | 7 | faccld | |
9 | elfznn | |
|
10 | elfzuz3 | |
|
11 | 10 | adantl | |
12 | dvdsfac | |
|
13 | 9 11 12 | syl2an2 | |
14 | 13 | ralrimiva | |
15 | 8 14 | jca | |
16 | lcmfledvds | |
|
17 | 6 15 16 | sylc | |