FKS2.mid_row8_hi

theorem mid_row8_hi : ∀ x ∈ Set.Icc (exp (9500:ℝ)) (exp (20000:ℝ)),    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 :=    le_trans (Real.exp_le_exp.mpr (by norm_num : ((10:ℕ):ℝ) ≤ 9500)) hxlo  have hx_hi : x ≤ exp ((lastB 10 allCells : ℕ):ℝ) := by    rw [allCells_last]; simpa using hxhi  obtain ⟨c, hcmem, hcx⟩ :=    cover_of_chainOk allCells 10 allCells_ne_nil allCells_chain hx_lo10 hx_hi  have hb' : 9500 ≤ c.b' := by    have hlogx : (9500:ℝ) ≤ Real.log x := by      rw [← Real.log_exp 9500]; exact Real.log_le_log (Real.exp_pos _) hxlo    have hcb' : Real.log x ≤ ((c.b' : ℕ):ℝ) := (Real.log_le_iff_le_exp hxpos).mpr hcx.2    have hge : (9500:ℝ) ≤ ((c.b' : ℕ):ℝ) := le_trans hlogx hcb'    exact_mod_cast hge  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