Metamath Proof Explorer

Theorem n0ltsp1le

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

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

Proof

Step Hyp Ref Expression
1 n0subs2 ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M < s N ↔ N - s M ∈ ℕ s
2 nnsge1 ⊢ N - s M ∈ ℕ s → 1 s ≤ s N - s M
3 1no ⊢ 1 s ∈ No
4 3 a1i ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → 1 s ∈ No
5 simpr ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N ∈ ℕ 0s
6 n0no ⊢ N ∈ ℕ 0s → N ∈ No
7 5 6 syl ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N ∈ No
8 n0no ⊢ M ∈ ℕ 0s → M ∈ No
9 8 adantr ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M ∈ No
10 7 9 subscld ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N - s M ∈ No
11 4 10 9 leadds2d ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → 1 s ≤ s N - s M ↔ M + s 1 s ≤ s M + s N - s M
12 pncan3s ⊢ M ∈ No ∧ N ∈ No → M + s N - s M = N
13 8 6 12 syl2an ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M + s N - s M = N
14 13 breq2d ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M + s 1 s ≤ s M + s N - s M ↔ M + s 1 s ≤ s N
15 11 14 bitrd ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → 1 s ≤ s N - s M ↔ M + s 1 s ≤ s N
16 2 15 imbitrid ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → N - s M ∈ ℕ s → M + s 1 s ≤ s N
17 1 16 sylbid ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M < s N → M + s 1 s ≤ s N
18 8 ad2antrr ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s ∧ M + s 1 s ≤ s N → M ∈ No
19 peano2no ⊢ M ∈ No → M + s 1 s ∈ No
20 18 19 syl ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s ∧ M + s 1 s ≤ s N → M + s 1 s ∈ No
21 6 ad2antlr ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s ∧ M + s 1 s ≤ s N → N ∈ No
22 18 ltsp1d ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s ∧ M + s 1 s ≤ s N → M < s M + s 1 s
23 simpr ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s ∧ M + s 1 s ≤ s N → M + s 1 s ≤ s N
24 18 20 21 22 23 ltlestrd ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s ∧ M + s 1 s ≤ s N → M < s N
25 24 ex ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M + s 1 s ≤ s N → M < s N
26 17 25 impbid ⊢ M ∈ ℕ 0s ∧ N ∈ ℕ 0s → M < s N ↔ M + s 1 s ≤ s N