field_simp [h, nterm, cpow_add _ _ (Nat.cast_ne_zero.mpr h)]
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ ‖term f (↑σ' + ↑x * I) n‖ = nterm f σ' n
case neg
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : Summable (nterm f σ')
l1 : ∀ (i : ℕ), Continuous fun x => term f (↑σ' + ↑x * I) i
n : ℕ
x : ℝ
h : ¬n = 0
⊢ Complex.abs (↑n ^ (↑x * I)) = 1 ∨ f n = 0