Metamath Proof Explorer
Description: Closure law for nonnegative integer exponentiation. For integer
exponents, see expclz . (Contributed by NM, 26-May-2005)
|
|
Ref |
Expression |
|
Assertion |
expcl |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
ssid |
|
2 |
|
mulcl |
|
3 |
|
ax-1cn |
|
4 |
1 2 3
|
expcllem |
|