⊢ ∀ (x : ℕ), ∃ y, y ∈ {p | Prime p} ∧ x < y
⊢ ¬BddAbove {p | Prime p}
rw [not_bddAbove_iff]
n : ℕ
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
⊢ ∀ (x : ℕ), ∃ y, y ∈ {p | Prime p} ∧ x < y
intro n
case intro.intro
n p : ℕ
hi : succ n ≤ p
hp : Prime p
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
n : ℕ
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ
no goals
case intro.intro
n p : ℕ
hi : succ n ≤ p
hp : Prime p
⊢ ∃ y, y ∈ {p | Prime p} ∧ n < y
exact ⟨p, hp, hi⟩