Metamath Proof Explorer

Theorem elznn0

Description: Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion elznn0 
|- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )

Proof

Step Hyp Ref Expression
1 elz 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
3 2 a1i 
 |-  ( N e. RR -> ( N e. NN0 <-> ( N e. NN \/ N = 0 ) ) )
4 elnn0 
 |-  ( -u N e. NN0 <-> ( -u N e. NN \/ -u N = 0 ) )
5 recn 
 |-  ( N e. RR -> N e. CC )
6 0cn 
 |-  0 e. CC
7 negcon1 
 |-  ( ( N e. CC /\ 0 e. CC ) -> ( -u N = 0 <-> -u 0 = N ) )
8 5 6 7 sylancl 
 |-  ( N e. RR -> ( -u N = 0 <-> -u 0 = N ) )
9 neg0 
 |-  -u 0 = 0
10 9 eqeq1i 
 |-  ( -u 0 = N <-> 0 = N )
11 eqcom 
 |-  ( 0 = N <-> N = 0 )
12 10 11 bitri 
 |-  ( -u 0 = N <-> N = 0 )
13 8 12 bitrdi 
 |-  ( N e. RR -> ( -u N = 0 <-> N = 0 ) )
14 13 orbi2d 
 |-  ( N e. RR -> ( ( -u N e. NN \/ -u N = 0 ) <-> ( -u N e. NN \/ N = 0 ) ) )
15 4 14 syl5bb 
 |-  ( N e. RR -> ( -u N e. NN0 <-> ( -u N e. NN \/ N = 0 ) ) )
16 3 15 orbi12d 
 |-  ( N e. RR -> ( ( N e. NN0 \/ -u N e. NN0 ) <-> ( ( N e. NN \/ N = 0 ) \/ ( -u N e. NN \/ N = 0 ) ) ) )
17 3orass 
 |-  ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N = 0 \/ ( N e. NN \/ -u N e. NN ) ) )
18 orcom 
 |-  ( ( N = 0 \/ ( N e. NN \/ -u N e. NN ) ) <-> ( ( N e. NN \/ -u N e. NN ) \/ N = 0 ) )
19 orordir 
 |-  ( ( ( N e. NN \/ -u N e. NN ) \/ N = 0 ) <-> ( ( N e. NN \/ N = 0 ) \/ ( -u N e. NN \/ N = 0 ) ) )
20 17 18 19 3bitrri 
 |-  ( ( ( N e. NN \/ N = 0 ) \/ ( -u N e. NN \/ N = 0 ) ) <-> ( N = 0 \/ N e. NN \/ -u N e. NN ) )
21 16 20 bitr2di 
 |-  ( N e. RR -> ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N e. NN0 \/ -u N e. NN0 ) ) )
22 21 pm5.32i 
 |-  ( ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )
23 1 22 bitri 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN0 \/ -u N e. NN0 ) ) )