Metamath Proof Explorer

Theorem eln0zs

Description: Non-negative surreal integer property expressed in terms of integers. (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Assertion eln0zs 
|- ( N e. NN0_s <-> ( N e. ZZ_s /\ 0s <_s N ) )

Proof

Step Hyp Ref Expression
1 n0zs 
 |-  ( N e. NN0_s -> N e. ZZ_s )
2 n0sge0 
 |-  ( N e. NN0_s -> 0s <_s N )
3 1 2 jca 
 |-  ( N e. NN0_s -> ( N e. ZZ_s /\ 0s <_s N ) )
4 elzs 
 |-  ( N e. ZZ_s <-> E. x e. NN_s E. y e. NN_s N = ( x -s y ) )
5 nnsno 
 |-  ( x e. NN_s -> x e. No )
6 5 adantr 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> x e. No )
7 nnsno 
 |-  ( y e. NN_s -> y e. No )
8 7 adantl 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> y e. No )
9 6 8 subsge0d 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> ( 0s <_s ( x -s y ) <-> y <_s x ) )
10 nnn0s 
 |-  ( y e. NN_s -> y e. NN0_s )
11 nnn0s 
 |-  ( x e. NN_s -> x e. NN0_s )
12 n0subs 
 |-  ( ( y e. NN0_s /\ x e. NN0_s ) -> ( y <_s x <-> ( x -s y ) e. NN0_s ) )
13 10 11 12 syl2anr 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> ( y <_s x <-> ( x -s y ) e. NN0_s ) )
14 9 13 bitrd 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> ( 0s <_s ( x -s y ) <-> ( x -s y ) e. NN0_s ) )
15 14 biimpd 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> ( 0s <_s ( x -s y ) -> ( x -s y ) e. NN0_s ) )
16 breq2 
 |-  ( N = ( x -s y ) -> ( 0s <_s N <-> 0s <_s ( x -s y ) ) )
17 eleq1 
 |-  ( N = ( x -s y ) -> ( N e. NN0_s <-> ( x -s y ) e. NN0_s ) )
18 16 17 imbi12d 
 |-  ( N = ( x -s y ) -> ( ( 0s <_s N -> N e. NN0_s ) <-> ( 0s <_s ( x -s y ) -> ( x -s y ) e. NN0_s ) ) )
19 15 18 syl5ibrcom 
 |-  ( ( x e. NN_s /\ y e. NN_s ) -> ( N = ( x -s y ) -> ( 0s <_s N -> N e. NN0_s ) ) )
20 19 rexlimivv 
 |-  ( E. x e. NN_s E. y e. NN_s N = ( x -s y ) -> ( 0s <_s N -> N e. NN0_s ) )
21 4 20 sylbi 
 |-  ( N e. ZZ_s -> ( 0s <_s N -> N e. NN0_s ) )
22 21 imp 
 |-  ( ( N e. ZZ_s /\ 0s <_s N ) -> N e. NN0_s )
23 3 22 impbii 
 |-  ( N e. NN0_s <-> ( N e. ZZ_s /\ 0s <_s N ) )