Metamath Proof Explorer

Theorem n0expscl

Description: Closure law for non-negative surreal integer exponentiation. (Contributed by Scott Fenton, 7-Nov-2025)

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

Proof

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