Theorem n0subs2

Description: Subtraction of non-negative surreal integers. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	n0subs2	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕs ) )

Proof

Step	Hyp	Ref	Expression
1		n0subs	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕ0s ) )
2		n0no	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ No )
3	2	adantl	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑁 ∈ No )
4		n0no	⊢ ( 𝑀 ∈ ℕ0s → 𝑀 ∈ No )
5	4	adantr	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑀 ∈ No )
6	3 5	subseq0d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑁 -s 𝑀 ) = 0s ↔ 𝑁 = 𝑀 ) )
7	6	necon3bid	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑁 -s 𝑀 ) ≠ 0s ↔ 𝑁 ≠ 𝑀 ) )
8	7	bicomd	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑁 ≠ 𝑀 ↔ ( 𝑁 -s 𝑀 ) ≠ 0s ) )
9	1 8	anbi12d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑀 ≤s 𝑁 ∧ 𝑁 ≠ 𝑀 ) ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℕ0s ∧ ( 𝑁 -s 𝑀 ) ≠ 0s ) ) )
10	5 3	ltlesnd	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s 𝑁 ↔ ( 𝑀 ≤s 𝑁 ∧ 𝑁 ≠ 𝑀 ) ) )
11		elnns	⊢ ( ( 𝑁 -s 𝑀 ) ∈ ℕs ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℕ0s ∧ ( 𝑁 -s 𝑀 ) ≠ 0s ) )
12	11	a1i	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( ( 𝑁 -s 𝑀 ) ∈ ℕs ↔ ( ( 𝑁 -s 𝑀 ) ∈ ℕ0s ∧ ( 𝑁 -s 𝑀 ) ≠ 0s ) ) )
13	9 10 12	3bitr4d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s 𝑁 ↔ ( 𝑁 -s 𝑀 ) ∈ ℕs ) )