by_cases hN : N = 0
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)
case pos
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)

case neg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
N : ℕ
hN : ¬N = 0
⊢ ↑(primesBetween 1 ↑N) ≤ 4 * (↑N / (↑N).log) + 6 * (↑N ^ (1 / 2) * (1 + 1 / 2 * (↑N).log) ^ 3)