b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ abs x = -x
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ b ^ logb b x = -x
rw [rpow_logb_eq_abs b_pos b_ne_one (ne_of_lt hx)]
no goals
b x y : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
hx : x < 0
⊢ abs x = -x
exact abs_of_neg hx