Metamath Proof Explorer

Theorem elznns

Description: Surreal integer property expressed in terms of positive integers and non-negative integers. (Contributed by Scott Fenton, 25-Jul-2025)

Ref Expression
Assertion elznns 
|- ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ ( -us ` N ) e. NN0_s ) ) )

Proof

Step Hyp Ref Expression
1 elzs2 
 |-  ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) )
2 3orass 
 |-  ( ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) <-> ( N e. NN_s \/ ( N = 0s \/ ( -us ` N ) e. NN_s ) ) )
3 eln0s 
 |-  ( ( -us ` N ) e. NN0_s <-> ( ( -us ` N ) e. NN_s \/ ( -us ` N ) = 0s ) )
4 negs0s 
 |-  ( -us ` 0s ) = 0s
5 4 eqeq2i 
 |-  ( ( -us ` N ) = ( -us ` 0s ) <-> ( -us ` N ) = 0s )
6 0sno 
 |-  0s e. No
7 negs11 
 |-  ( ( N e. No /\ 0s e. No ) -> ( ( -us ` N ) = ( -us ` 0s ) <-> N = 0s ) )
8 6 7 mpan2 
 |-  ( N e. No -> ( ( -us ` N ) = ( -us ` 0s ) <-> N = 0s ) )
9 5 8 bitr3id 
 |-  ( N e. No -> ( ( -us ` N ) = 0s <-> N = 0s ) )
10 9 orbi2d 
 |-  ( N e. No -> ( ( ( -us ` N ) e. NN_s \/ ( -us ` N ) = 0s ) <-> ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
11 3 10 bitrid 
 |-  ( N e. No -> ( ( -us ` N ) e. NN0_s <-> ( ( -us ` N ) e. NN_s \/ N = 0s ) ) )
12 orcom 
 |-  ( ( ( -us ` N ) e. NN_s \/ N = 0s ) <-> ( N = 0s \/ ( -us ` N ) e. NN_s ) )
13 11 12 bitrdi 
 |-  ( N e. No -> ( ( -us ` N ) e. NN0_s <-> ( N = 0s \/ ( -us ` N ) e. NN_s ) ) )
14 13 orbi2d 
 |-  ( N e. No -> ( ( N e. NN_s \/ ( -us ` N ) e. NN0_s ) <-> ( N e. NN_s \/ ( N = 0s \/ ( -us ` N ) e. NN_s ) ) ) )
15 2 14 bitr4id 
 |-  ( N e. No -> ( ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) <-> ( N e. NN_s \/ ( -us ` N ) e. NN0_s ) ) )
16 15 pm5.32i 
 |-  ( ( N e. No /\ ( N e. NN_s \/ N = 0s \/ ( -us ` N ) e. NN_s ) ) <-> ( N e. No /\ ( N e. NN_s \/ ( -us ` N ) e. NN0_s ) ) )
17 1 16 bitri 
 |-  ( N e. ZZ_s <-> ( N e. No /\ ( N e. NN_s \/ ( -us ` N ) e. NN0_s ) ) )