Metamath Proof Explorer


Theorem expclzd

Description: Closure law for integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses expcld.1 ( 𝜑𝐴 ∈ ℂ )
sqrecd.1 ( 𝜑𝐴 ≠ 0 )
expclzd.3 ( 𝜑𝑁 ∈ ℤ )
Assertion expclzd ( 𝜑 → ( 𝐴𝑁 ) ∈ ℂ )

Proof

Step Hyp Ref Expression
1 expcld.1 ( 𝜑𝐴 ∈ ℂ )
2 sqrecd.1 ( 𝜑𝐴 ≠ 0 )
3 expclzd.3 ( 𝜑𝑁 ∈ ℤ )
4 expclz ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝐴𝑁 ) ∈ ℂ )
5 1 2 3 4 syl3anc ( 𝜑 → ( 𝐴𝑁 ) ∈ ℂ )