rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ ↑n ^ ↑σ' = ↑(↑n ^ σ')
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp ((↑n).log * ↑σ') = ↑(if ↑n = 0 then if σ' = 0 then 1 else 0 else rexp ((↑n).log * σ'))