x y : ℝ
⊢ abs x ^ y ≤ exp (log x * y)
x y : ℝ
⊢ abs (x ^ y) ≤ exp (log x * y)
refine' (abs_rpow_le_abs_rpow x y).trans _
case pos
x y : ℝ
hx : x = 0
⊢ abs x ^ y ≤ exp (log x * y)

case neg
x y : ℝ
hx : ¬x = 0
⊢ abs x ^ y ≤ exp (log x * y)
x y : ℝ
⊢ abs x ^ y ≤ exp (log x * y)
by_cases hx : x = 0
no goals
case pos
x y : ℝ
hx : x = 0
⊢ abs x ^ y ≤ exp (log x * y)
by_cases hy : y = 0 <;> simp [hx, hy, zero_le_one]
no goals
case neg
x y : ℝ
hx : ¬x = 0
⊢ abs x ^ y ≤ exp (log x * y)
rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]