FKS2.mid_row8_lo

theorem mid_row8_lo : ∀ x ∈ Set.Icc (exp (10:ℝ)) (exp (5500:ℝ)),    Eπ x ≤ admissible_bound 121.107 1.5 2 5.5666305 x := by  intro x hx  obtain ⟨hxlo, hxhi⟩ := hx  have hxpos : (0:ℝ) < x := lt_of_lt_of_le (Real.exp_pos _) hxlo  have hx_lo10 : exp ((10:ℕ):ℝ) ≤ x := by simpa using hxlo  have hx_hi : x ≤ exp ((lastB 10 allCells : ℕ):ℝ) := by    rw [allCells_last]    exact le_trans hxhi (Real.exp_le_exp.mpr (by norm_num : (5500:ℝ) ≤ 20000))  obtain ⟨c, hcmem, hcx⟩ :=    cover_of_chainOk allCells 10 allCells_ne_nil allCells_chain hx_lo10 hx_hi  have hb : c.b ≤ 5500 := by    have hlogx : Real.log x ≤ 5500 := by      rw [← Real.log_exp 5500]; exact Real.log_le_log hxpos hxhi    have hcb : ((c.b : ℕ):ℝ) ≤ Real.log x := (Real.le_log_iff_exp_le hxpos).mpr hcx.1    have hle : ((c.b : ℕ):ℝ) ≤ 5500 := le_trans hcb hlogx    exact_mod_cast hle  have hck : checkCellGen P8 c = true := by    have h := List.all_eq_true.mp r8_sides c hcmem    simp only [Bool.or_eq_true, decide_eq_true_eq] at h    rcases h with ⟨hlt, _⟩ | hok    · omega    · exact hok  exact cell_Epi_le_admissible_gen P8 121.107 1.5 2 5.5666305 cell_hk (by norm_num)    (by norm_num) (by norm_num) (by norm_num [P8]) cell_hCge cell_hrB    c hck (allCells_trusted c hcmem) x hcx