Metamath Proof Explorer

Theorem nnexpscl

Description: Closure law for positive surreal integer exponentiation. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Assertion nnexpscl 
|- ( ( A e. NN_s /\ N e. NN0_s ) -> ( A ^su N ) e. NN_s )

Proof

Step Hyp Ref Expression
1 nnssno 
 |-  NN_s C_ No
2 nnmulscl 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> ( x x.s y ) e. NN_s )
3 1nns 
 |-  1s e. NN_s
4 1 2 3 expscllem 
 |-  ( ( A e. NN_s /\ N e. NN0_s ) -> ( A ^su N ) e. NN_s )