Metamath Proof Explorer


Theorem prmgaplcmlem1

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 NI2NIlcm_1N+I

Proof

Step Hyp Ref Expression
1 elfzelz I2NI
2 1 adantl NI2NI
3 fzssz 1N
4 fzfi 1NFin
5 3 4 pm3.2i 1N1NFin
6 lcmfcl 1N1NFinlcm_1N0
7 6 nn0zd 1N1NFinlcm_1N
8 5 7 mp1i NI2Nlcm_1N
9 breq1 x=Ixlcm_1NIlcm_1N
10 dvdslcmf 1N1NFinx1Nxlcm_1N
11 5 10 mp1i NI2Nx1Nxlcm_1N
12 2eluzge1 21
13 fzss1 212N1N
14 12 13 mp1i N2N1N
15 14 sselda NI2NI1N
16 9 11 15 rspcdva NI2NIlcm_1N
17 iddvds III
18 1 17 syl I2NII
19 18 adantl NI2NII
20 2 8 2 16 19 dvds2addd NI2NIlcm_1N+I