x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < exp (log x * z)
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ x ^ y < x ^ z
repeat' rw [rpow_def_of_pos hx0]
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < exp (log x * z)
rw [exp_lt_exp]
no goals
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ log x * y < log x * z
exact mul_lt_mul_of_neg_left hyz (log_neg hx0 hx1)
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < exp (log x * z)
x y z : ℝ
hx0 : 0 < x
hx1 : x < 1
hyz : z < y
⊢ exp (log x * y) < exp (log x * z)
rw [rpow_def_of_pos hx0]