Metamath Proof Explorer


Theorem nn0expcld

Description: Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016)

Ref Expression
Hypotheses nn0expcld.1 φA0
nn0expcld.2 φN0
Assertion nn0expcld φAN0

Proof

Step Hyp Ref Expression
1 nn0expcld.1 φA0
2 nn0expcld.2 φN0
3 nn0expcl A0N0AN0
4 1 2 3 syl2anc φAN0