FKS2.corollary_23_row8

theorem corollary_23_row8 : Eπ.classicalBound 121.107 1.5 2 5.5666305 (exp 1) := by  intro x hx  by_cases h10 : x ≤ exp 10  · exact floor_row8 x ⟨hx, h10⟩  · rw [not_le] at h10    by_cases h5500 : x ≤ exp 5500    · exact mid_row8_lo x ⟨le_of_lt h10, h5500⟩    · rw [not_le] at h5500      by_cases h9500 : x ≤ exp 9500      · exact band_row8 x ⟨le_of_lt h5500, h9500⟩      · rw [not_le] at h9500        by_cases h20k : x ≤ exp 20000        · exact mid_row8_hi x ⟨le_of_lt h9500, h20k⟩        · rw [not_le] at h20k          exact tail_row8 x (le_of_lt h20k)