x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
x y z : ℝ
hx : 0 ≤ x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
rw [le_iff_eq_or_lt] at hx
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z

case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z
x y z : ℝ
hx : 0 = x ∨ 0 < x
hxy : x < y
hz : 0 < z
⊢ x ^ z < y ^ z
cases' hx with hx hx
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ x ^ z < y ^ z
rw [← hx, zero_rpow (ne_of_gt hz)]
no goals
case inl
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y ^ z
exact rpow_pos_of_pos (by rwa [← hx] at hxy) _
no goals
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 = x
⊢ 0 < y
rwa [← hx] at hxy
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ x ^ z < y ^ z
rw [rpow_def_of_pos hx, rpow_def_of_pos (lt_trans hx hxy), exp_lt_exp]
no goals
case inr
x y z : ℝ
hxy : x < y
hz : 0 < z
hx : 0 < x
⊢ log x * z < log y * z
exact mul_lt_mul_of_pos_right (log_lt_log hx hxy) hz