Metamath Proof Explorer

Theorem prmgap

Description: The prime gap theorem: for each positive integer there are (at least) two successive primes with a difference ("gap") at least as big as the given integer. (Contributed by AV, 13-Aug-2020)

		Ref	Expression
	Assertion	prmgap	$⊢ \forall n \in ℕ \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ n \in ℕ \to n \in ℕ$
2		facmapnn	$⊢ (x \in ℕ ⟼ x!) \in (ℕ^{ℕ})$
3	2	a1i	$⊢ n \in ℕ \to (x \in ℕ ⟼ x!) \in (ℕ^{ℕ})$
4		prmgaplem2	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to 1 < (n! + i) \gcd i$
5		eqidd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (x \in ℕ ⟼ x!) = (x \in ℕ ⟼ x!)$
6		fveq2	$⊢ x = n \to x! = n!$
7	6	adantl	$⊢ ((n \in ℕ \land i \in (2 \dots n)) \land x = n) \to x! = n!$
8		simpl	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to n \in ℕ$
9		fvexd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to n! \in V$
10	5 7 8 9	fvmptd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (x \in ℕ ⟼ x!) (n) = n!$
11	10	oveq1d	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to (x \in ℕ ⟼ x!) (n) + i = n! + i$
12	11	oveq1d	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to ((x \in ℕ ⟼ x!) (n) + i) \gcd i = (n! + i) \gcd i$
13	4 12	breqtrrd	$⊢ (n \in ℕ \land i \in (2 \dots n)) \to 1 < ((x \in ℕ ⟼ x!) (n) + i) \gcd i$
14	13	ralrimiva	$⊢ n \in ℕ \to \forall i \in (2 \dots n) 1 < ((x \in ℕ ⟼ x!) (n) + i) \gcd i$
15	1 3 14	prmgaplem8	$⊢ n \in ℕ \to \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$
16	15	rgen	$⊢ \forall n \in ℕ \exists p \in ℙ \exists q \in ℙ (n \leq q - p \land \forall z \in (p + 1 ..^q) z \notin ℙ)$