Metamath Proof Explorer

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 ⊢ M ∈ ℤ s ∧ N ∈ ℤ s → M ≤ s N ↔ N - s M ∈ ℕ 0s

Proof

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