Theorem nnzsubs

Description: The difference of two surreal positive integers is an integer. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Assertion	nnzsubs	$$⊢\left(A\in {\mathbb{N}}_s\wedge B\in {\mathbb{N}}_s\right)\to A{-}_{s}B\in {\mathbb{Z}}_s$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A{-}_{s}B=A{-}_{s}B$$
2		rspceov	$$⊢\left(A\in {\mathbb{N}}_s\wedge B\in {\mathbb{N}}_s\wedge A{-}_{s}B=A{-}_{s}B\right)\to \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A{-}_{s}B=x{-}_{s}y$$
3	1 2	mp3an3	$$⊢\left(A\in {\mathbb{N}}_s\wedge B\in {\mathbb{N}}_s\right)\to \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A{-}_{s}B=x{-}_{s}y$$
4		elzs	$$⊢A{-}_{s}B\in {\mathbb{Z}}_s\leftrightarrow \exists x\in {\mathbb{N}}_s\exists y\in {\mathbb{N}}_{s}A{-}_{s}B=x{-}_{s}y$$
5	3 4	sylibr	$$⊢\left(A\in {\mathbb{N}}_s\wedge B\in {\mathbb{N}}_s\right)\to A{-}_{s}B\in {\mathbb{Z}}_s$$