Metamath Proof Explorer


Theorem prmgaplem1

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 NI2NIN!+I

Proof

Step Hyp Ref Expression
1 elfzelz I2NI
2 1 adantl NI2NI
3 nnnn0 NN0
4 3 faccld NN!
5 4 nnzd NN!
6 5 adantr NI2NN!
7 elfzuz I2NI2
8 eluz2nn I2I
9 7 8 syl I2NI
10 elfzuz3 I2NNI
11 9 10 jca I2NINI
12 11 adantl NI2NINI
13 dvdsfac INIIN!
14 12 13 syl NI2NIN!
15 iddvds III
16 1 15 syl I2NII
17 16 adantl NI2NII
18 2 6 2 14 17 dvds2addd NI2NIN!+I