b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ logb b x < logb b y
rw [logb, logb, div_lt_div_right (log_pos hb)]
no goals
b x y : ℝ
hb : 1 < b
hx : 0 < x
hxy : x < y
⊢ log x < log y
exact log_lt_log hx hxy