Metamath Proof Explorer

Theorem n0sltp1le

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

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

Proof

Step Hyp Ref Expression
1 n0subs2 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( N -s M ) e. NN_s ) )
2 nnsge1 
 |-  ( ( N -s M ) e. NN_s -> 1s <_s ( N -s M ) )
3 1sno 
 |-  1s e. No
4 3 a1i 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> 1s e. No )
5 simpr 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> N e. NN0_s )
6 n0sno 
 |-  ( N e. NN0_s -> N e. No )
7 5 6 syl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> N e. No )
8 n0sno 
 |-  ( M e. NN0_s -> M e. No )
9 8 adantr 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> M e. No )
10 7 9 subscld 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( N -s M ) e. No )
11 4 10 9 sleadd2d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( 1s <_s ( N -s M ) <-> ( M +s 1s ) <_s ( M +s ( N -s M ) ) ) )
12 pncan3s 
 |-  ( ( M e. No /\ N e. No ) -> ( M +s ( N -s M ) ) = N )
13 8 6 12 syl2an 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M +s ( N -s M ) ) = N )
14 13 breq2d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( M +s 1s ) <_s ( M +s ( N -s M ) ) <-> ( M +s 1s ) <_s N ) )
15 11 14 bitrd 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( 1s <_s ( N -s M ) <-> ( M +s 1s ) <_s N ) )
16 2 15 imbitrid 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( N -s M ) e. NN_s -> ( M +s 1s ) <_s N ) )
17 1 16 sylbid 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( M +s 1s ) <_s N ) )
18 8 ad2antrr 
 |-  ( ( ( M e. NN0_s /\ N e. NN0_s ) /\ ( M +s 1s ) <_s N ) -> M e. No )
19 peano2no 
 |-  ( M e. No -> ( M +s 1s ) e. No )
20 18 19 syl 
 |-  ( ( ( M e. NN0_s /\ N e. NN0_s ) /\ ( M +s 1s ) <_s N ) -> ( M +s 1s ) e. No )
21 6 ad2antlr 
 |-  ( ( ( M e. NN0_s /\ N e. NN0_s ) /\ ( M +s 1s ) <_s N ) -> N e. No )
22 18 sltp1d 
 |-  ( ( ( M e. NN0_s /\ N e. NN0_s ) /\ ( M +s 1s ) <_s N ) -> M
23 simpr 
 |-  ( ( ( M e. NN0_s /\ N e. NN0_s ) /\ ( M +s 1s ) <_s N ) -> ( M +s 1s ) <_s N )
24 18 20 21 22 23 sltletrd 
 |-  ( ( ( M e. NN0_s /\ N e. NN0_s ) /\ ( M +s 1s ) <_s N ) -> M
25 24 ex 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( ( M +s 1s ) <_s N -> M
26 17 25 impbid 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( M +s 1s ) <_s N ) )