Metamath Proof Explorer

Theorem n0slem1lt

Description: Non-negative surreal ordering relation. (Contributed by Scott Fenton, 8-Nov-2025)

Ref Expression
Assertion n0slem1lt ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M ≤ s N ↔ M - s 1 s < s N

Proof

Step Hyp Ref Expression
1 n0sleltp1 ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M ≤ s N ↔ M < s N + s 1 s
2 n0sno ⊢ M ∈ ℕ 0s → M ∈ No
3 2 adantr ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M ∈ No
4 n0sno ⊢ N ∈ ℕ 0s → N ∈ No
5 4 adantl ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N ∈ No
6 peano2no ⊢ N ∈ No → N + s 1 s ∈ No
7 5 6 syl ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N + s 1 s ∈ No
8 1sno ⊢ 1 s ∈ No
9 8 a1i ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → 1 s ∈ No
10 3 7 9 sltsub1d ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M < s N + s 1 s ↔ M - s 1 s < s N + s 1 s - s 1 s
11 pncans ⊢ N ∈ No ∧ 1 s ∈ No → N + s 1 s - s 1 s = N
12 4 8 11 sylancl ⊢ N ∈ ℕ 0s → N + s 1 s - s 1 s = N
13 12 adantl ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N + s 1 s - s 1 s = N
14 13 breq2d ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M - s 1 s < s N + s 1 s - s 1 s ↔ M - s 1 s < s N
15 1 10 14 3bitrd ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M ≤ s N ↔ M - s 1 s < s N