Metamath Proof Explorer

Theorem nn0expcl

Description: Closure of exponentiation of nonnegative integers. (Contributed by NM, 14-Dec-2005)

Ref Expression
Assertion nn0expcl ( ( ๐ด โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ โ„•0 )

Proof

Step Hyp Ref Expression
1 nn0sscn โŠข โ„•0 โŠ† โ„‚
2 nn0mulcl โŠข ( ( ๐‘ฅ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0 ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ โ„•0 )
3 1nn0 โŠข 1 โˆˆ โ„•0
4 1 2 3 expcllem โŠข ( ( ๐ด โˆˆ โ„•0 โˆง ๐‘ โˆˆ โ„•0 ) โ†’ ( ๐ด โ†‘ ๐‘ ) โˆˆ โ„•0 )