Metamath Proof Explorer


Theorem lcmflefac

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 Nlcm_1NN!

Proof

Step Hyp Ref Expression
1 fzssz 1N
2 1 a1i N1N
3 fzfid N1NFin
4 0nelfz1 01N
5 4 a1i N01N
6 2 3 5 3jca N1N1NFin01N
7 nnnn0 NN0
8 7 faccld NN!
9 elfznn m1Nm
10 elfzuz3 m1NNm
11 10 adantl Nm1NNm
12 dvdsfac mNmmN!
13 9 11 12 syl2an2 Nm1NmN!
14 13 ralrimiva Nm1NmN!
15 8 14 jca NN!m1NmN!
16 lcmfledvds 1N1NFin01NN!m1NmN!lcm_1NN!
17 6 15 16 sylc Nlcm_1NN!