Theorem zexpscl

Description: Closure law for surreal integer exponentiation. (Contributed by Scott Fenton, 11-Dec-2025)

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

Proof

Step	Hyp	Ref	Expression
1		zssno	|- ZZ_s C_ No
2		simpl	|- ( ( x e. ZZ_s /\ y e. ZZ_s ) -> x e. ZZ_s )
3		simpr	|- ( ( x e. ZZ_s /\ y e. ZZ_s ) -> y e. ZZ_s )
4	2 3	zmulscld	|- ( ( x e. ZZ_s /\ y e. ZZ_s ) -> ( x x.s y ) e. ZZ_s )
5		1zs	|- 1s e. ZZ_s
6	1 4 5	expscllem	|- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A ^su N ) e. ZZ_s )