apply Real.logb_nonneg
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 0 ≤ (↑b).logb ↑n
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 < ↑b

case hx
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
b n : ℕ
hb : 1 < b
hn : ¬n = 0
⊢ 1 ≤ ↑n