x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ abs (log x * x ^ t) * t < 1
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ abs (log x * x ^ t) < 1 / t
rw [lt_div_iff ht]
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : abs (log (x ^ t) * x ^ t) < 1
⊢ abs (log x * x ^ t) * t < 1
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
⊢ abs (log x * x ^ t) * t < 1
have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)
no goals
x✝ y z x t : ℝ
h1 : 0 < x
h2 : x ≤ 1
ht : 0 < t
this : abs (log (x ^ t) * x ^ t) < 1
⊢ abs (log x * x ^ t) * t < 1
rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this