FKS2.corollary_24_row9

theorem corollary_24_row9 :    ∀ x, Real.log x ∈ Set.Icc (1:ℝ) 270.8 → Eπ x ≤ x ^ (-(1:ℝ)/10) := by  intro x hlog  obtain ⟨hlo, hhi⟩ := hlog  rcases lt_trichotomy x 0 with hxneg | hx0 | hxpos  · -- x < 0: `Eπ x ≤ 0 < x^{-1/10}`    have hLpos : (0:ℝ) < Real.log x := by linarith    have hEle0 : Eπ x ≤ 0 := by      unfold Eπ      apply div_nonpos_of_nonneg_of_nonpos (abs_nonneg _)      exact le_of_lt (div_neg_of_neg_of_pos hxneg hLpos)    have hRpos : (0:ℝ) < x ^ (-(1:ℝ)/10) := by      rw [Real.rpow_def_of_neg hxneg]      apply mul_pos (Real.exp_pos _)      apply Real.cos_pos_of_mem_Ioo      constructor <;> nlinarith [Real.pi_pos, Real.pi_le_four]    linarith  · -- x = 0: `log 0 = 0` contradicts `1 ≤ log x`    exfalso; rw [hx0, Real.log_zero] at hlo; linarith  · -- x > 0: dispatch to the four segments    have cvt : ∀ a b : ℝ, a ≤ Real.log x → Real.log x ≤ b →        x ∈ Set.Icc (Real.exp a) (Real.exp b) := by      intro a b ha hb      exact ⟨by rw [← Real.exp_log hxpos]; exact Real.exp_le_exp.mpr ha,             by rw [← Real.exp_log hxpos]; exact Real.exp_le_exp.mpr hb⟩    rcases le_total (Real.log x) 4 with h1 | h1    · exact floor_trusted_row9 x (cvt 1 4 hlo h1)    · rcases le_total (Real.log x) 10 with h2 | h2      · exact floor_row9 x (cvt 4 10 h1 h2)      · rcases le_total (Real.log x) 270 with h3 | h3        · exact mid_row9 x (cvt 10 270 h2 h3)        · exact sliver_row9 x (cvt 270 270.8 h3 hhi)