intro n
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ Finset.filter Nat.Prime (Finset.range N) ⊆ Finset.filter Nat.Prime (Finset.range (N + 1))
case a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N n : ℕ
⊢ n ∈ Finset.filter Nat.Prime (Finset.range N) → n ∈ Finset.filter Nat.Prime (Finset.range (N + 1))