Theorem nnzsubs

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

	Ref	Expression
Assertion	nnzsubs	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs ) → ( 𝐴 -s 𝐵 ) ∈ ℤs )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 -s 𝐵 ) = ( 𝐴 -s 𝐵 )
2		rspceov	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs ∧ ( 𝐴 -s 𝐵 ) = ( 𝐴 -s 𝐵 ) ) → ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs ( 𝐴 -s 𝐵 ) = ( 𝑥 -s 𝑦 ) )
3	1 2	mp3an3	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs ) → ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs ( 𝐴 -s 𝐵 ) = ( 𝑥 -s 𝑦 ) )
4		elzs	⊢ ( ( 𝐴 -s 𝐵 ) ∈ ℤs ↔ ∃ 𝑥 ∈ ℕs ∃ 𝑦 ∈ ℕs ( 𝐴 -s 𝐵 ) = ( 𝑥 -s 𝑦 ) )
5	3 4	sylibr	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝐵 ∈ ℕs ) → ( 𝐴 -s 𝐵 ) ∈ ℤs )