FKS2.mid_row2

theorem mid_row2 : ∀ x ∈ Set.Icc (exp (10:ℝ)) (exp (20000:ℝ)),    Eπ x ≤ admissible_bound 0.826 0.25 1 5.5666305 x := by  intro x hx  have hx_lo : exp ((10:ℕ):ℝ) ≤ x := by simpa using hx.1  have hx_hi : x ≤ exp ((lastB 10 allCells : ℕ):ℝ) := by    rw [allCells_last]; simpa using hx.2  obtain ⟨c, hcmem, hcx⟩ :=    cover_of_chainOk allCells 10 allCells_ne_nil allCells_chain hx_lo hx_hi  have hck : checkCellGenQuarter P2 c = true := List.all_eq_true.mp allCells_checked_row2 c hcmem  refine cell_Epi_le_admissible_quarter P2 0.826 1 5.5666305 (by norm_num) (by norm_num)    (by norm_num [P2]) ?_ ?_ c hck (allCells_trusted c hcmem) x hcx  · have hrhs : (((P2.c64 * 64 : ℚ)):ℝ) = 8477/10000 := by norm_num [P2]    rw [hrhs, mul_one_div, div_le_iff₀ sqrtR5_pos]    nlinarith [sqrtR5_lb]  · have hrhs : (((P2.rB : ℚ)):ℝ) = 235938/100000 := by norm_num [P2]    rw [hrhs]; linarith [sqrtR5_ub]