ext p
case e_s
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n : ℕ
⊢ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) = Finset.filter Nat.Prime (Finset.range (n + 1))
case e_s.a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
n p : ℕ
⊢ p ∈ Finset.filter Nat.Prime (Finset.Icc ⌈1⌉₊ ⌊↑n⌋₊) ↔ p ∈ Finset.filter Nat.Prime (Finset.range (n + 1))