x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < exp (log x * z)
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ x ^ y < x ^ z
repeat' rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < exp (log x * z)
rw [exp_lt_exp]
no goals
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ log x * y < log x * z
exact mul_lt_mul_of_pos_left hyz (log_pos hx)
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < exp (log x * z)
x y z : ℝ
hx : 1 < x
hyz : y < z
⊢ exp (log x * y) < exp (log x * z)
rw [rpow_def_of_pos (lt_trans zero_lt_one hx)]