Metamath Proof Explorer

Theorem nnsge1

Description: A positive surreal integer is greater than or equal to one. (Contributed by Scott Fenton, 26-Jul-2025)

Ref Expression
Assertion nnsge1 
|- ( N e. NN_s -> 1s <_s N )

Proof

Step Hyp Ref Expression
1 elnns 
 |-  ( N e. NN_s <-> ( N e. NN0_s /\ N =/= 0s ) )
2 n0s0suc 
 |-  ( N e. NN0_s -> ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) )
3 neneq 
 |-  ( N =/= 0s -> -. N = 0s )
4 pm2.53 
 |-  ( ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) -> ( -. N = 0s -> E. x e. NN0_s N = ( x +s 1s ) ) )
5 4 imp 
 |-  ( ( ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) /\ -. N = 0s ) -> E. x e. NN0_s N = ( x +s 1s ) )
6 1sno 
 |-  1s e. No
7 addslid 
 |-  ( 1s e. No -> ( 0s +s 1s ) = 1s )
8 6 7 ax-mp 
 |-  ( 0s +s 1s ) = 1s
9 n0sge0 
 |-  ( x e. NN0_s -> 0s <_s x )
10 n0sno 
 |-  ( x e. NN0_s -> x e. No )
11 0sno 
 |-  0s e. No
12 sleadd1 
 |-  ( ( 0s e. No /\ x e. No /\ 1s e. No ) -> ( 0s <_s x <-> ( 0s +s 1s ) <_s ( x +s 1s ) ) )
13 11 6 12 mp3an13 
 |-  ( x e. No -> ( 0s <_s x <-> ( 0s +s 1s ) <_s ( x +s 1s ) ) )
14 10 13 syl 
 |-  ( x e. NN0_s -> ( 0s <_s x <-> ( 0s +s 1s ) <_s ( x +s 1s ) ) )
15 9 14 mpbid 
 |-  ( x e. NN0_s -> ( 0s +s 1s ) <_s ( x +s 1s ) )
16 8 15 eqbrtrrid 
 |-  ( x e. NN0_s -> 1s <_s ( x +s 1s ) )
17 breq2 
 |-  ( N = ( x +s 1s ) -> ( 1s <_s N <-> 1s <_s ( x +s 1s ) ) )
18 16 17 syl5ibrcom 
 |-  ( x e. NN0_s -> ( N = ( x +s 1s ) -> 1s <_s N ) )
19 18 rexlimiv 
 |-  ( E. x e. NN0_s N = ( x +s 1s ) -> 1s <_s N )
20 5 19 syl 
 |-  ( ( ( N = 0s \/ E. x e. NN0_s N = ( x +s 1s ) ) /\ -. N = 0s ) -> 1s <_s N )
21 2 3 20 syl2an 
 |-  ( ( N e. NN0_s /\ N =/= 0s ) -> 1s <_s N )
22 1 21 sylbi 
 |-  ( N e. NN_s -> 1s <_s N )