Theorem zn0subs

Description: The non-negative difference of surreal integers is a non-negative integer. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Assertion	zn0subs	⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )

Proof

Step	Hyp	Ref	Expression
1		zno	⊢ ( 𝑁 ∈ ℤs → 𝑁 ∈ No )
2	1	adantr	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → 𝑁 ∈ No )
3		zno	⊢ ( 𝑀 ∈ ℤs → 𝑀 ∈ No )
4	3	adantl	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → 𝑀 ∈ No )
5	2 4	subsge0d	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → ( 0s ≤s ( 𝑁 -s 𝑀 ) ↔ 𝑀 ≤s 𝑁 ) )
6		simpl	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → 𝑁 ∈ ℤs )
7		simpr	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → 𝑀 ∈ ℤs )
8	6 7	zsubscld	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → ( 𝑁 -s 𝑀 ) ∈ ℤs )
9	8	biantrurd	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → ( 0s ≤s ( 𝑁 -s 𝑀 ) ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℤs ∧ 0s ≤s ( 𝑁 -s 𝑀 ) ) ) )
10	5 9	bitr3d	⊢ ( ( 𝑁 ∈ ℤs ∧ 𝑀 ∈ ℤs ) → ( 𝑀 ≤s 𝑁 ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℤs ∧ 0s ≤s ( 𝑁 -s 𝑀 ) ) ) )
11	10	ancoms	⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ) → ( 𝑀 ≤s 𝑁 ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℤs ∧ 0s ≤s ( 𝑁 -s 𝑀 ) ) ) )
12		eln0zs	⊢ ( ( 𝑁 -s 𝑀 ) ∈ ℕ0s ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℤs ∧ 0s ≤s ( 𝑁 -s 𝑀 ) ) )
13	11 12	bitr4di	⊢ ( ( 𝑀 ∈ ℤs ∧ 𝑁 ∈ ℤs ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )