Theorem zsubscld

Description: The surreal integers are closed under subtraction. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Hypotheses	zsubscld.1	|- ( ph -> A e. ZZ_s )
	zsubscld.2	|- ( ph -> B e. ZZ_s )
Assertion	zsubscld	|- ( ph -> ( A -s B ) e. ZZ_s )

Proof

Step	Hyp	Ref	Expression
1		zsubscld.1	|- ( ph -> A e. ZZ_s )
2		zsubscld.2	|- ( ph -> B e. ZZ_s )
3	1	znod	|- ( ph -> A e. No )
4	2	znod	|- ( ph -> B e. No )
5	3 4	subsvald	|- ( ph -> ( A -s B ) = ( A +s ( -us ` B ) ) )
6	2	znegscld	|- ( ph -> ( -us ` B ) e. ZZ_s )
7	1 6	zaddscld	|- ( ph -> ( A +s ( -us ` B ) ) e. ZZ_s )
8	5 7	eqeltrd	|- ( ph -> ( A -s B ) e. ZZ_s )