UpperBnd_aux6

lemma UpperBnd_aux6 {σ t : ℝ} (t_ge : 3 < |t|) (hσ : σ ∈ Ioc (1 / 2) 2)    (neOne : σ + t * I ≠ 1) (Npos : 0 < ⌊|t|⌋₊) (N_le_t : ⌊|t|⌋₊ ≤ |t|) :    ⌊|t|⌋₊ ^ (1 - σ) / ‖1 - (σ + t * I)‖ ≤ |t| ^ (1 - σ) * 2 ∧    ⌊|t|⌋₊ ^ (-σ) / 2 ≤ |t| ^ (1 - σ) ∧ ⌊|t|⌋₊ ^ (-σ) / σ ≤ 8 * |t| ^ (-σ) := by  have bnd := UpperBnd_aux5 t_ge hσ.2  have bnd' : (|t| / ⌊|t|⌋₊) ^ σ ≤ 2 * |t| := by linarith  split_ands  · apply (div_le_iff₀ <| norm_pos_iff.mpr <| sub_ne_zero_of_ne neOne.symm).mpr    conv => rw [mul_assoc]; rhs; rw [mul_comm]    apply (div_le_iff₀ <| Real.rpow_pos_of_pos (by linarith) _).mp    rw [div_rpow_eq_rpow_div_neg (by positivity) (by positivity), neg_sub]    refine le_trans₄ ?_ bnd' ?_    · exact Real.rpow_le_rpow_of_exponent_le (one_le_div (by positivity) |>.mpr N_le_t) (by simp)    · apply (mul_le_mul_iff_right₀ (by norm_num)).mpr; simpa using abs_im_le_norm (1 - (σ + t * I))  · apply div_le_iff₀ (by norm_num) |>.mpr    rw [Real.rpow_sub (by linarith), Real.rpow_one, div_mul_eq_mul_div, mul_comm]    apply div_le_iff₀ (by positivity) |>.mp    convert! bnd' using 1    rw [← Real.rpow_neg (by linarith), div_rpow_neg_eq_rpow_div (by positivity) (by positivity)]  · apply div_le_iff₀ (by linarith [hσ.1]) |>.mpr    rw [mul_assoc, mul_comm, mul_assoc]    apply div_le_iff₀' (by positivity) |>.mp    apply le_trans ?_ (by linarith [hσ.1] : 4 ≤ σ * 8)    convert! bnd using 1; exact div_rpow_neg_eq_rpow_div (by positivity) (by positivity)