x y : ℝ
⊢ ∀ ⦃a : ℝ⦄, 1 ≤ a → ∀ ⦃b : ℝ⦄, 1 ≤ b → a ≤ b → log a * a ≤ log b * b
x y : ℝ
⊢ MonotoneOn (fun x => log x * x) {x | 1 ≤ x}
simp only [MonotoneOn, mem_setOf_eq]
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
⊢ log x * x ≤ log y * y
x y : ℝ
⊢ ∀ ⦃a : ℝ⦄, 1 ≤ a → ∀ ⦃b : ℝ⦄, 1 ≤ b → a ≤ b → log a * a ≤ log b * b
intro x hex y hey hxy
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log x * x ≤ log y * y
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
⊢ log x * x ≤ log y * y
have x_pos : 0 < x := lt_of_lt_of_le zero_lt_one hex
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log x * x ≤ log y * y
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
⊢ log x * x ≤ log y * y
have y_pos : 0 < y := lt_of_lt_of_le zero_lt_one hey
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 0 ≤ log y
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ log x * x ≤ log y * y
refine' mul_le_mul ((log_le_log x_pos y_pos).mpr hxy) hxy (le_of_lt x_pos) _
no goals
x✝ y✝ x : ℝ
hex : 1 ≤ x
y : ℝ
hey : 1 ≤ y
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 0 ≤ log y
rwa [le_log_iff_exp_le y_pos, Real.exp_zero]