ZetaAppendix.cauchySeq_exp_over_nat_of_not_int

lemma cauchySeq_exp_over_nat_of_not_int {x : ℝ} (hx : ¬ ∃ k : ℤ, x = k) :    CauchySeq fun N : ℕ ↦      ∑ n ∈ range N,        ((1 : ℝ) / (n + 1 : ℝ)) •          (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ (n + 1) := by  let z : ℕ → ℂ := fun n ↦ (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ (n + 1)  let ζ : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)  have hζ_norm : ‖ζ‖ = 1 := norm_exp_two_pi_mul_I x  obtain ⟨C, _hC_nonneg, hC⟩ := exp_geometric_partial_sums_bounded hx  refine one_div_nat_add_one_antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded    (b := C + 1)    tendsto_one_div_nat_add_one ?_  intro N  calc    ‖∑ n ∈ range N, (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ (n + 1)‖        = ‖ζ * ∑ n ∈ range N, ζ ^ n‖ := by      congr 1      rw [mul_sum]      refine sum_congr rfl fun n _ ↦ ?_      rw [← pow_succ']    _ = ‖ζ‖ * ‖∑ n ∈ range N, ζ ^ n‖ := norm_mul _ _    _ = 1 * ‖∑ n ∈ range N, ζ ^ n‖ := by rw [hζ_norm]    _ ≤ 1 * C := by      exact mul_le_mul_of_nonneg_left (hC N) zero_le_one    _ ≤ C + 1 := by linarith