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	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ (N! + I)$

Proof

Step	Hyp	Ref	Expression
1		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
2	1	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℤ$
3		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
4	3	faccld	$⊢ N \in ℕ \to N! \in ℕ$
5	4	nnzd	$⊢ N \in ℕ \to N! \in ℤ$
6	5	adantr	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to N! \in ℤ$
7		elfzuz	$⊢ I \in (2 \dots N) \to I \in ℤ_{\geq 2}$
8		eluz2nn	$⊢ I \in ℤ_{\geq 2} \to I \in ℕ$
9	7 8	syl	$⊢ I \in (2 \dots N) \to I \in ℕ$
10		elfzuz3	$⊢ I \in (2 \dots N) \to N \in ℤ_{\geq I}$
11	9 10	jca	$⊢ I \in (2 \dots N) \to (I \in ℕ \land N \in ℤ_{\geq I})$
12	11	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (I \in ℕ \land N \in ℤ_{\geq I})$
13		dvdsfac	$⊢ (I \in ℕ \land N \in ℤ_{\geq I}) \to I ∥ N!$
14	12 13	syl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ N!$
15		iddvds	$⊢ I \in ℤ \to I ∥ I$
16	1 15	syl	$⊢ I \in (2 \dots N) \to I ∥ I$
17	16	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ I$
18	2 6 2 14 17	dvds2addd	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ (N! + I)$