Metamath Proof Explorer

Theorem elnnzs

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

Ref Expression
Assertion elnnzs 
|- ( N e. NN_s <-> ( N e. ZZ_s /\ 0s

Proof

Step Hyp Ref Expression
1 nnsno 
 |-  ( N e. NN_s -> N e. No )
2 orc 
 |-  ( N e. NN_s -> ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
3 nnsgt0 
 |-  ( N e. NN_s -> 0s
4 1 2 3 jca31 
 |-  ( N e. NN_s -> ( ( N e. No /\ ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) /\ 0s
5 idd 
 |-  ( ( N e. No /\ 0s  ( N e. NN_s -> N e. NN_s ) )
6 negscl 
 |-  ( N e. No -> ( -us ` N ) e. No )
7 6 adantr 
 |-  ( ( N e. No /\ 0s  ( -us ` N ) e. No )
8 0sno 
 |-  0s e. No
9 sltneg 
 |-  ( ( 0s e. No /\ N e. No ) -> ( 0s  ( -us ` N )
10 8 9 mpan 
 |-  ( N e. No -> ( 0s  ( -us ` N )
11 negs0s 
 |-  ( -us ` 0s ) = 0s
12 11 breq2i 
 |-  ( ( -us ` N )  ( -us ` N )
13 10 12 bitrdi 
 |-  ( N e. No -> ( 0s  ( -us ` N )
14 13 biimpa 
 |-  ( ( N e. No /\ 0s  ( -us ` N )
15 sltasym 
 |-  ( ( ( -us ` N ) e. No /\ 0s e. No ) -> ( ( -us ` N )  -. 0s
16 8 15 mpan2 
 |-  ( ( -us ` N ) e. No -> ( ( -us ` N )  -. 0s
17 7 14 16 sylc 
 |-  ( ( N e. No /\ 0s  -. 0s
18 nnsgt0 
 |-  ( ( -us ` N ) e. NN_s -> 0s
19 17 18 nsyl 
 |-  ( ( N e. No /\ 0s  -. ( -us ` N ) e. NN_s )
20 sgt0ne0 
 |-  ( 0s  N =/= 0s )
21 20 adantl 
 |-  ( ( N e. No /\ 0s  N =/= 0s )
22 21 neneqd 
 |-  ( ( N e. No /\ 0s  -. N = 0s )
23 ioran 
 |-  ( -. ( ( -us ` N ) e. NN_s \/ N = 0s ) <-> ( -. ( -us ` N ) e. NN_s /\ -. N = 0s ) )
24 19 22 23 sylanbrc 
 |-  ( ( N e. No /\ 0s  -. ( ( -us ` N ) e. NN_s \/ N = 0s ) )
25 24 pm2.21d 
 |-  ( ( N e. No /\ 0s  ( ( ( -us ` N ) e. NN_s \/ N = 0s ) -> N e. NN_s ) )
26 5 25 jaod 
 |-  ( ( N e. No /\ 0s  ( ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) -> N e. NN_s ) )
27 26 ex 
 |-  ( N e. No -> ( 0s  ( ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) -> N e. NN_s ) ) )
28 27 com23 
 |-  ( N e. No -> ( ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) -> ( 0s  N e. NN_s ) ) )
29 28 imp31 
 |-  ( ( ( N e. No /\ ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) /\ 0s  N e. NN_s )
30 4 29 impbii 
 |-  ( N e. NN_s <-> ( ( N e. No /\ ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) /\ 0s
31 elzs2 
 |-  ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) )
32 3orcomb 
 |-  ( ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) <-> ( N e. NN_s \/ ( -us ` N ) e. NN_s \/ N = 0s ) )
33 3orass 
 |-  ( ( N e. NN_s \/ ( -us ` N ) e. NN_s \/ N = 0s ) <-> ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
34 32 33 bitri 
 |-  ( ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) <-> ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
35 34 anbi2i 
 |-  ( ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) <-> ( N e. No /\ ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) )
36 31 35 bitri 
 |-  ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) )
37 36 anbi1i 
 |-  ( ( N e. ZZ_s /\ 0s  ( ( N e. No /\ ( N e. NN_s \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) /\ 0s
38 30 37 bitr4i 
 |-  ( N e. NN_s <-> ( N e. ZZ_s /\ 0s