DerivUpperBnd_aux3

theorem DerivUpperBnd_aux3 {A σ t : ℝ} (t_gt : 3 < |t|) (hσ : σ ∈ Icc (1 - A / |t|.log) 2) :    let N := ⌊|t|⌋₊;    let s := ↑σ + ↑t * I;    0 < N → ↑N ≤ |t| → s ≠ 1 → 1 / 2 < σ →    ‖↑(N : ℝ).log * ↑N ^ (1 - s) / (1 - s)‖ ≤ A.exp * 2 * |t|.log := by  intro N s Npos N_le_t neOne σ_gt  rw [norm_div, norm_mul, mul_div_assoc, mul_comm]  apply mul_le_mul ?_ ?_ (by positivity) (by positivity)  · have h := UpperBnd_aux6 t_gt ⟨σ_gt, hσ.2⟩ neOne Npos N_le_t |>.1    convert le_trans h ?_ using 1    · simp [s, norm_natCast_cpow_of_pos Npos _, N]    · gcongr; exact UpperBnd_aux2 t_gt hσ.1  · rw [natCast_log, norm_complex_log_ofNat]    exact Real.log_le_log (by positivity) N_le_t