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_le_exp]
no goals
x y z : ℝ
hx0 : 0 < x
hx1 : x ≤ 1
hyz : z ≤ y
⊢ log x * y ≤ log x * z
exact mul_le_mul_of_nonpos_left hyz (log_nonpos (le_of_lt 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]