Theorem zexpscl

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

	Ref	Expression
Assertion	zexpscl	Could not format assertion : No typesetting found for |- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A ^su N ) e. ZZ_s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		zssno	$$⊢{\mathbb{Z}}_s\subseteq \mathrm{No}$$
2		simpl	$$⊢\left(x\in {\mathbb{Z}}_s\wedge y\in {\mathbb{Z}}_s\right)\to x\in {\mathbb{Z}}_s$$
3		simpr	$$⊢\left(x\in {\mathbb{Z}}_s\wedge y\in {\mathbb{Z}}_s\right)\to y\in {\mathbb{Z}}_s$$
4	2 3	zmulscld	$$⊢\left(x\in {\mathbb{Z}}_s\wedge y\in {\mathbb{Z}}_s\right)\to x{\cdot }_{s}y\in {\mathbb{Z}}_s$$
5		1zs	$$⊢1_s\in {\mathbb{Z}}_s$$
6	1 4 5	expscllem	Could not format ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A ^su N ) e. ZZ_s ) : No typesetting found for |- ( ( A e. ZZ_s /\ N e. NN0_s ) -> ( A ^su N ) e. ZZ_s ) with typecode |-