Theorem zexpscl

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

	Ref	Expression
Assertion	zexpscl	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ ℤs )

Proof

Step	Hyp	Ref	Expression
1		zssno	⊢ ℤs ⊆ No
2		simpl	⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℤs ) → 𝑥 ∈ ℤs )
3		simpr	⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℤs ) → 𝑦 ∈ ℤs )
4	2 3	zmulscld	⊢ ( ( 𝑥 ∈ ℤs ∧ 𝑦 ∈ ℤs ) → ( 𝑥 ·s 𝑦 ) ∈ ℤs )
5		1zs	⊢ 1s ∈ ℤs
6	1 4 5	expscllem	⊢ ( ( 𝐴 ∈ ℤs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ ℤs )