Metamath Proof Explorer

Theorem n0slem1lt

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

Ref Expression
Assertion n0slem1lt 
|- ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> ( M -s 1s )

Proof

Step Hyp Ref Expression
1 n0sleltp1 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> M
2 n0sno 
 |-  ( M e. NN0_s -> M e. No )
3 2 adantr 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> M e. No )
4 n0sno 
 |-  ( N e. NN0_s -> N e. No )
5 4 adantl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> N e. No )
6 peano2no 
 |-  ( N e. No -> ( N +s 1s ) e. No )
7 5 6 syl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( N +s 1s ) e. No )
8 1sno 
 |-  1s e. No
9 8 a1i 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> 1s e. No )
10 3 7 9 sltsub1d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( M -s 1s )
11 pncans 
 |-  ( ( N e. No /\ 1s e. No ) -> ( ( N +s 1s ) -s 1s ) = N )
12 4 8 11 sylancl 
 |-  ( N e. NN0_s -> ( ( N +s 1s ) -s 1s ) = N )
13 12 adantl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( N +s 1s ) -s 1s ) = N )
14 13 breq2d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( M -s 1s )  ( M -s 1s )
15 1 10 14 3bitrd 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> ( M -s 1s )