FKS2.tail_row9

theorem tail_row9 : ∀ x ≥ exp (20000:ℝ),    Eπ x ≤ admissible_bound 6.60 2 2 5.5666305 x := by  intro x hx  refine le_trans (cor14_tail x hx) ?_  have hL : (20000:ℝ) ≤ Real.log x := by    rw [← Real.log_exp 20000]; exact Real.log_le_log (Real.exp_pos _) hx  have hLnn : (0:ℝ) ≤ Real.log x := le_trans (by norm_num) hL  rw [admissible_three_halves_eq 121.107 2 5.5666305 x hLnn (by norm_num),      admissible_two_eq 6.60 2 5.5666305 x hLnn (by norm_num)]  set s := Real.sqrt (Real.log x) with hs  have hsnn : (0:ℝ) ≤ s := Real.sqrt_nonneg _  have hs141 : (141:ℝ) ≤ s := by    rw [hs, show (141:ℝ) = Real.sqrt (141^2) from (Real.sqrt_sq (by norm_num)).symm]    exact Real.sqrt_le_sqrt (by nlinarith [hL])  have hR15_lo : (13.133:ℝ) ≤ (5.5666305:ℝ) ^ (1.5:ℝ) := by    rw [R5_rpow_three_halves_eq]; nlinarith [sqrtR5_lb, sqrtR5_pos]  have hcoef : (121.107:ℝ) / (5.5666305:ℝ) ^ (1.5:ℝ)      ≤ 6.60 / (5.5666305:ℝ) ^ (2:ℝ) * s := by    have h1 : (121.107:ℝ) / (5.5666305:ℝ) ^ (1.5:ℝ) ≤ 121.107 / 13.133 :=      div_le_div_of_nonneg_left (by norm_num) (by norm_num) hR15_lo    have h2 : (121.107:ℝ) / 13.133 ≤ 6.60 / (5.5666305:ℝ) ^ (2:ℝ) * 141 := by      rw [R5_rpow_two_eq]; norm_num    have h3 : (6.60:ℝ) / (5.5666305:ℝ) ^ (2:ℝ) * 141 ≤ 6.60 / (5.5666305:ℝ) ^ (2:ℝ) * s :=      mul_le_mul_of_nonneg_left hs141 (by positivity)    linarith  have hs3 : (0:ℝ) ≤ s ^ 3 := by positivity  have key : (121.107:ℝ) / (5.5666305:ℝ) ^ (1.5:ℝ) * s ^ 3      ≤ 6.60 / (5.5666305:ℝ) ^ (2:ℝ) * s ^ 4 := by    have he : (6.60:ℝ) / (5.5666305:ℝ) ^ (2:ℝ) * s ^ 4        = (6.60 / (5.5666305:ℝ) ^ (2:ℝ) * s) * s ^ 3 := by ring    rw [he]; exact mul_le_mul_of_nonneg_right hcoef hs3  exact mul_le_mul_of_nonneg_right key (Real.exp_nonneg _)