prmgaplem2

Description: Lemma for prmgap : The factorial of a number plus an integer greater than 1 and less then or equal to the number are not coprime. (Contributed by AV, 13-Aug-2020)

		Ref	Expression
	Assertion	prmgaplem2	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to 1 < (N! + I) \gcd I$

Proof

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ I \in (2 \dots N) \to I \in ℤ_{\geq 2}$
2	1	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℤ_{\geq 2}$
3		breq1	$⊢ i = I \to (i ∥ (N! + I) \leftrightarrow I ∥ (N! + I))$
4		breq1	$⊢ i = I \to (i ∥ I \leftrightarrow I ∥ I)$
5	3 4	anbi12d	$⊢ i = I \to ((i ∥ (N! + I) \land i ∥ I) \leftrightarrow (I ∥ (N! + I) \land I ∥ I))$
6	5	adantl	$⊢ ((N \in ℕ \land I \in (2 \dots N)) \land i = I) \to ((i ∥ (N! + I) \land i ∥ I) \leftrightarrow (I ∥ (N! + I) \land I ∥ I))$
7		prmgaplem1	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ (N! + I)$
8		elfzelz	$⊢ I \in (2 \dots N) \to I \in ℤ$
9		iddvds	$⊢ I \in ℤ \to I ∥ I$
10	8 9	syl	$⊢ I \in (2 \dots N) \to I ∥ I$
11	10	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I ∥ I$
12	7 11	jca	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (I ∥ (N! + I) \land I ∥ I)$
13	2 6 12	rspcedvd	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to \exists i \in ℤ_{\geq 2} (i ∥ (N! + I) \land i ∥ I)$
14		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
15	14	faccld	$⊢ N \in ℕ \to N! \in ℕ$
16	15	adantr	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to N! \in ℕ$
17		eluz2nn	$⊢ I \in ℤ_{\geq 2} \to I \in ℕ$
18	1 17	syl	$⊢ I \in (2 \dots N) \to I \in ℕ$
19	18	adantl	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to I \in ℕ$
20	16 19	nnaddcld	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to N! + I \in ℕ$
21		ncoprmgcdgt1b	$⊢ (N! + I \in ℕ \land I \in ℕ) \to (\exists i \in ℤ_{\geq 2} (i ∥ (N! + I) \land i ∥ I) \leftrightarrow 1 < (N! + I) \gcd I)$
22	20 19 21	syl2anc	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to (\exists i \in ℤ_{\geq 2} (i ∥ (N! + I) \land i ∥ I) \leftrightarrow 1 < (N! + I) \gcd I)$
23	13 22	mpbid	$⊢ (N \in ℕ \land I \in (2 \dots N)) \to 1 < (N! + I) \gcd I$

Metamath Proof Explorer

Theorem prmgaplem2

Proof