Theorem expclz

Description: Closure law for integer exponentiation of complex numnbers. (Contributed by Mario Carneiro, 4-Jun-2014)

	Ref	Expression
Assertion	expclz	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		expclzlem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ( ℂ ∖ { 0 } ) )
2	1	eldifad	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )