Theorem expclz

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

	Ref	Expression
Assertion	expclz	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		expclzlem	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. ( CC \ { 0 } ) )
2	1	eldifad	|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) e. CC )