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	⊢ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑛 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ )
2		facmapnn	⊢ ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ∈ ( ℕ ↑m ℕ )
3	2	a1i	⊢ ( 𝑛 ∈ ℕ → ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ∈ ( ℕ ↑m ℕ ) )
4		prmgaplem2	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → 1 < ( ( ( ! ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) )
5		eqidd	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) = ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) )
6		fveq2	⊢ ( 𝑥 = 𝑛 → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑛 ) )
7	6	adantl	⊢ ( ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) ∧ 𝑥 = 𝑛 ) → ( ! ‘ 𝑥 ) = ( ! ‘ 𝑛 ) )
8		simpl	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → 𝑛 ∈ ℕ )
9		fvexd	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ! ‘ 𝑛 ) ∈ V )
10	5 7 8 9	fvmptd	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ‘ 𝑛 ) = ( ! ‘ 𝑛 ) )
11	10	oveq1d	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ( ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ‘ 𝑛 ) + 𝑖 ) = ( ( ! ‘ 𝑛 ) + 𝑖 ) )
12	11	oveq1d	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → ( ( ( ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) = ( ( ( ! ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) )
13	4 12	breqtrrd	⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑖 ∈ ( 2 ... 𝑛 ) ) → 1 < ( ( ( ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) )
14	13	ralrimiva	⊢ ( 𝑛 ∈ ℕ → ∀ 𝑖 ∈ ( 2 ... 𝑛 ) 1 < ( ( ( ( 𝑥 ∈ ℕ ↦ ( ! ‘ 𝑥 ) ) ‘ 𝑛 ) + 𝑖 ) gcd 𝑖 ) )
15	1 3 14	prmgaplem8	⊢ ( 𝑛 ∈ ℕ → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑛 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ ) )
16	15	rgen	⊢ ∀ 𝑛 ∈ ℕ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ( 𝑛 ≤ ( 𝑞 − 𝑝 ) ∧ ∀ 𝑧 ∈ ( ( 𝑝 + 1 ) ..^ 𝑞 ) 𝑧 ∉ ℙ )