FKS2.mid_row1

theorem mid_row1 : ∀ x ∈ Set.Icc (exp (40:ℝ)) (exp (20000:ℝ)),    Eπ x ≤ admissible_bound 0.000120 0.25 1 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 (by simpa using Real.exp_le_exp.mpr (by norm_num : (10:ℝ) ≤ 40)) 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' : 40 ≤ c.b' := by    have hlogx : (40:ℝ) ≤ Real.log x := by      rw [← Real.log_exp 40]; 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 h40le : (40:ℝ) ≤ (c.b' : ℝ) := le_trans hlogx hcb'    exact_mod_cast h40le  have hck : checkCellGenQuarter P1 c = true := by    have h := List.all_eq_true.mp allCells_checked_row1_hi40 c hcmem    simp only [Bool.or_eq_true, decide_eq_true_eq] at h    rcases h with hlt | hok    · omega    · exact hok  refine cell_Epi_le_admissible_quarter P1 0.000120 1 5.5666305 (by norm_num) (by norm_num)    (by norm_num [P1]) ?_ ?_ c hck (allCells_trusted c hcmem) x hcx  · have hrhs : (((P1.c64 * 64 : ℚ)):ℝ) = 8477/10000 := by norm_num [P1]    rw [hrhs, mul_one_div, div_le_iff₀ sqrtR5_pos]; nlinarith [sqrtR5_lb]  · have hrhs : (((P1.rB : ℚ)):ℝ) = 235938/100000 := by norm_num [P1]    rw [hrhs]; linarith [sqrtR5_ub]