Theorem nnzsubs

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

	Ref	Expression
Assertion	nnzsubs	|- ( ( A e. NN_s /\ B e. NN_s ) -> ( A -s B ) e. ZZ_s )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( A -s B ) = ( A -s B )
2		rspceov	|- ( ( A e. NN_s /\ B e. NN_s /\ ( A -s B ) = ( A -s B ) ) -> E. x e. NN_s E. y e. NN_s ( A -s B ) = ( x -s y ) )
3	1 2	mp3an3	|- ( ( A e. NN_s /\ B e. NN_s ) -> E. x e. NN_s E. y e. NN_s ( A -s B ) = ( x -s y ) )
4		elzs	|- ( ( A -s B ) e. ZZ_s <-> E. x e. NN_s E. y e. NN_s ( A -s B ) = ( x -s y ) )
5	3 4	sylibr	|- ( ( A e. NN_s /\ B e. NN_s ) -> ( A -s B ) e. ZZ_s )