Metamath Proof Explorer

Theorem n0subs2

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

Ref Expression
Assertion n0subs2 ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M < s N ↔ N - s M ∈ ℕ s

Proof

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