Metamath Proof Explorer

Theorem elzs2

Description: A surreal integer is either a positive integer, zero, or the negative of a positive integer. (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Assertion elzs2 
|- ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) )

Proof

Step Hyp Ref Expression
1 elzn0s 
 |-  ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN0_s \/ ( -us ` N ) e. NN0_s ) ) )
2 eln0s 
 |-  ( N e. NN0_s <-> ( N e. NN_s \/ N = 0s ) )
3 2 a1i 
 |-  ( N e. No -> ( N e. NN0_s <-> ( N e. NN_s \/ N = 0s ) ) )
4 eln0s 
 |-  ( ( -us ` N ) e. NN0_s <-> ( ( -us ` N ) e. NN_s \/ ( -us ` N ) = 0s ) )
5 negs0s 
 |-  ( -us ` 0s ) = 0s
6 5 eqeq2i 
 |-  ( ( -us ` N ) = ( -us ` 0s ) <-> ( -us ` N ) = 0s )
7 0sno 
 |-  0s e. No
8 negs11 
 |-  ( ( N e. No /\ 0s e. No ) -> ( ( -us ` N ) = ( -us ` 0s ) <-> N = 0s ) )
9 7 8 mpan2 
 |-  ( N e. No -> ( ( -us ` N ) = ( -us ` 0s ) <-> N = 0s ) )
10 6 9 bitr3id 
 |-  ( N e. No -> ( ( -us ` N ) = 0s <-> N = 0s ) )
11 10 orbi2d 
 |-  ( N e. No -> ( ( ( -us ` N ) e. NN_s \/ ( -us ` N ) = 0s ) <-> ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
12 4 11 bitrid 
 |-  ( N e. No -> ( ( -us ` N ) e. NN0_s <-> ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
13 3 12 orbi12d 
 |-  ( N e. No -> ( ( N e. NN0_s \/ ( -us ` N ) e. NN0_s ) <-> ( ( N e. NN_s \/ N = 0s ) \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) ) )
14 3orcoma 
 |-  ( ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) <-> ( N = 0s \/ N e. NN_s \/ ( -us ` N ) e. NN_s ) )
15 3orass 
 |-  ( ( N = 0s \/ N e. NN_s \/ ( -us ` N ) e. NN_s ) <-> ( N = 0s \/ ( N e. NN_s \/ ( -us ` N ) e. NN_s ) ) )
16 orcom 
 |-  ( ( N = 0s \/ ( N e. NN_s \/ ( -us ` N ) e. NN_s ) ) <-> ( ( N e. NN_s \/ ( -us ` N ) e. NN_s ) \/ N = 0s ) )
17 orordir 
 |-  ( ( ( N e. NN_s \/ ( -us ` N ) e. NN_s ) \/ N = 0s ) <-> ( ( N e. NN_s \/ N = 0s ) \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
18 16 17 bitri 
 |-  ( ( N = 0s \/ ( N e. NN_s \/ ( -us ` N ) e. NN_s ) ) <-> ( ( N e. NN_s \/ N = 0s ) \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
19 14 15 18 3bitrri 
 |-  ( ( ( N e. NN_s \/ N = 0s ) \/ ( ( -us ` N ) e. NN_s \/ N = 0s ) ) <-> ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) )
20 13 19 bitr2di 
 |-  ( N e. No -> ( ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) <-> ( N e. NN0_s \/ ( -us ` N ) e. NN0_s ) ) )
21 20 pm5.32i 
 |-  ( ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) <-> ( N e. No /\ ( N e. NN0_s \/ ( -us ` N ) e. NN0_s ) ) )
22 1 21 bitr4i 
 |-  ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) )