Theorem expcl

Description: Closure law for nonnegative integer exponentiation. (Contributed by NM, 26-May-2005)

	Ref	Expression
Assertion	expcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ℂ ⊆ ℂ
2		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
3		ax-1cn	⊢ 1 ∈ ℂ
4	1 2 3	expcllem	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑁 ) ∈ ℂ )