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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		elfzelz	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℤ )
2	1	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∈ ℤ )
3		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
4	3	faccld	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℕ )
5	4	nnzd	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) ∈ ℤ )
6	5	adantr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℤ )
7		elfzuz	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ( ℤ≥ ‘ 2 ) )
8		eluz2nn	⊢ ( 𝐼 ∈ ( ℤ≥ ‘ 2 ) → 𝐼 ∈ ℕ )
9	7 8	syl	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∈ ℕ )
10		elfzuz3	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) )
11	9 10	jca	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) )
12	11	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) )
13		dvdsfac	⊢ ( ( 𝐼 ∈ ℕ ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐼 ) ) → 𝐼 ∥ ( ! ‘ 𝑁 ) )
14	12 13	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ! ‘ 𝑁 ) )
15		iddvds	⊢ ( 𝐼 ∈ ℤ → 𝐼 ∥ 𝐼 )
16	1 15	syl	⊢ ( 𝐼 ∈ ( 2 ... 𝑁 ) → 𝐼 ∥ 𝐼 )
17	16	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ 𝐼 )
18	2 6 2 14 17	dvds2addd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐼 ∈ ( 2 ... 𝑁 ) ) → 𝐼 ∥ ( ( ! ‘ 𝑁 ) + 𝐼 ) )