apply IsBigO.add
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun N =>
      ↑(Finset.filter Nat.Prime (Finset.range N)).card +
        ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑N⌉₊ ×ˢ Finset.range (Nat.log 2 N + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log
case h₁
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.filter Nat.Prime (Finset.range x)).card) =O[atTop] fun N => ↑N / (↑N).log

case h₂
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (fun x => ↑(Finset.image (fun p => p.1 ^ p.2) (Finset.Ico 1 ⌈√↑x⌉₊ ×ˢ Finset.range (Nat.log 2 x + 1))).card) =O[atTop]
    fun N => ↑N / (↑N).log