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 ) ) )