Metamath Proof Explorer


Theorem zexpcld

Description: Closure of exponentiation of integers, deductive form. (Contributed by SN, 15-Sep-2024)

Ref Expression
Hypotheses zexpcld.1 φ A
zexpcld.2 φ N 0
Assertion zexpcld φ A N

Proof

Step Hyp Ref Expression
1 zexpcld.1 φ A
2 zexpcld.2 φ N 0
3 zexpcl A N 0 A N
4 1 2 3 syl2anc φ A N