DerivUpperBnd_aux5

theorem DerivUpperBnd_aux5 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Icc (1 - A / |t|.log) 2) :    let N := ⌊|t|⌋₊;    let s := ↑σ + ↑t * I;    0 < N → 1 / 2 < σ →    ‖1 * ∫ (x : ℝ) in Ioi (N : ℝ), (↑⌊x⌋ + 1 / 2 - ↑x) * (x : ℂ) ^ (-s - 1)‖ ≤    1 / 3 * (2 * |t| * ↑N ^ (-σ) / σ) := by  intro N s Npos σ_gt  have neZero : s ≠ 0 := by    contrapose! σ_gt    simp only [Complex.ext_iff, add_re, ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one,      sub_self, add_zero, zero_re, add_im, mul_im, zero_add, zero_im, s] at σ_gt    linarith  have : 1 = 1 / s * s := by field_simp  nth_rewrite 1 [this]  rw [mul_assoc, norm_mul]  apply mul_le_mul ?_ ?_ (by positivity) (by positivity)  · simp only [s, norm_div, norm_one]    apply one_div_le_one_div (norm_pos_iff.mpr neZero) (by norm_num) |>.mpr    apply le_trans t_gt.le ?_    convert! abs_im_le_norm (σ + t * I); simp  · have hσ : σ ∈ Ioc 0 2 := ⟨(by linarith), hσ.2⟩    simp only [s]    have := ZetaBnd_aux1 N (by omega) hσ (by linarith)    simp only [div_cpow_eq_cpow_neg] at this    convert! this using 1; congr; funext x; ring_nf