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_of_lt_of_le 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_le_exp]
no goals
x y z : ℝ
hx : 1 ≤ x
hyz : y ≤ z
⊢ log x * y ≤ log x * z
exact mul_le_mul_of_nonneg_left hyz (log_nonneg 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_of_lt_of_le zero_lt_one hx)]