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	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( ! ` N ) + I ) )

Proof

Step	Hyp	Ref	Expression
1		elfzelz	|- ( I e. ( 2 ... N ) -> I e. ZZ )
2	1	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I e. ZZ )
3		nnnn0	|- ( N e. NN -> N e. NN0 )
4	3	faccld	|- ( N e. NN -> ( ! ` N ) e. NN )
5	4	nnzd	|- ( N e. NN -> ( ! ` N ) e. ZZ )
6	5	adantr	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( ! ` N ) e. ZZ )
7		elfzuz	|- ( I e. ( 2 ... N ) -> I e. ( ZZ>= ` 2 ) )
8		eluz2nn	|- ( I e. ( ZZ>= ` 2 ) -> I e. NN )
9	7 8	syl	|- ( I e. ( 2 ... N ) -> I e. NN )
10		elfzuz3	|- ( I e. ( 2 ... N ) -> N e. ( ZZ>= ` I ) )
11	9 10	jca	|- ( I e. ( 2 ... N ) -> ( I e. NN /\ N e. ( ZZ>= ` I ) ) )
12	11	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> ( I e. NN /\ N e. ( ZZ>= ` I ) ) )
13		dvdsfac	|- ( ( I e. NN /\ N e. ( ZZ>= ` I ) ) -> I || ( ! ` N ) )
14	12 13	syl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ! ` N ) )
15		iddvds	|- ( I e. ZZ -> I || I )
16	1 15	syl	|- ( I e. ( 2 ... N ) -> I || I )
17	16	adantl	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || I )
18	2 6 2 14 17	dvds2addd	|- ( ( N e. NN /\ I e. ( 2 ... N ) ) -> I || ( ( ! ` N ) + I ) )