b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ StrictMonoOn (logb b) (Iio 0)
rintro x (hx : x < 0) y (hy : y < 0) hxy
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b (abs x) < logb b (abs y)
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b x < logb b y
rw [← logb_abs y, ← logb_abs x]
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ abs y < abs x
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ logb b (abs x) < logb b (abs y)
refine' logb_lt_logb_of_base_lt_one b_pos b_lt_one (abs_pos.2 hy.ne) _
no goals
b x✝ y✝ : ℝ
b_pos : 0 < b
b_lt_one : b < 1
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
hxy : x < y
⊢ abs y < abs x
rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]