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 ⊢ ∀ n ∈ ℕ ∃ p ∈ ℙ ∃ q ∈ ℙ n ≤ q − p ∧ ∀ z ∈ p + 1 ..^ q z ∉ ℙ

Proof

Step Hyp Ref Expression
1 id ⊢ n ∈ ℕ → n ∈ ℕ
2 facmapnn ⊢ x ∈ ℕ ⟼ x ! ∈ ℕ ℕ
3 2 a1i ⊢ n ∈ ℕ → x ∈ ℕ ⟼ x ! ∈ ℕ ℕ
4 prmgaplem2 ⊢ n ∈ ℕ ∧ i ∈ 2 … n → 1 < n ! + i gcd i
5 eqidd ⊢ n ∈ ℕ ∧ i ∈ 2 … n → x ∈ ℕ ⟼ x ! = x ∈ ℕ ⟼ x !
6 fveq2 ⊢ x = n → x ! = n !
7 6 adantl ⊢ n ∈ ℕ ∧ i ∈ 2 … n ∧ x = n → x ! = n !
8 simpl ⊢ n ∈ ℕ ∧ i ∈ 2 … n → n ∈ ℕ
9 fvexd ⊢ n ∈ ℕ ∧ i ∈ 2 … n → n ! ∈ V
10 5 7 8 9 fvmptd ⊢ n ∈ ℕ ∧ i ∈ 2 … n → x ∈ ℕ ⟼ x ! ⁡ n = n !
11 10 oveq1d ⊢ n ∈ ℕ ∧ i ∈ 2 … n → x ∈ ℕ ⟼ x ! ⁡ n + i = n ! + i
12 11 oveq1d ⊢ n ∈ ℕ ∧ i ∈ 2 … n → x ∈ ℕ ⟼ x ! ⁡ n + i gcd i = n ! + i gcd i
13 4 12 breqtrrd ⊢ n ∈ ℕ ∧ i ∈ 2 … n → 1 < x ∈ ℕ ⟼ x ! ⁡ n + i gcd i
14 13 ralrimiva ⊢ n ∈ ℕ → ∀ i ∈ 2 … n 1 < x ∈ ℕ ⟼ x ! ⁡ n + i gcd i
15 1 3 14 prmgaplem8 ⊢ n ∈ ℕ → ∃ p ∈ ℙ ∃ q ∈ ℙ n ≤ q − p ∧ ∀ z ∈ p + 1 ..^ q z ∉ ℙ
16 15 rgen ⊢ ∀ n ∈ ℕ ∃ p ∈ ℙ ∃ q ∈ ℙ n ≤ q − p ∧ ∀ z ∈ p + 1 ..^ q z ∉ ℙ