Metamath Proof Explorer

Theorem expclz

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

		Ref	Expression
	Assertion	expclz	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℂ$

Step	Hyp	Ref	Expression
1		expclzlem	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in (ℂ ∖ \{0\})$
2	1	eldifad	$⊢ (A \in ℂ \land A \neq 0 \land N \in ℤ) \to A^{N} \in ℂ$