Metamath Proof Explorer

Theorem elznn

Description: Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005)

Ref Expression
Assertion elznn 
|- ( N e. ZZ <-> ( N e. RR /\ ( N e. NN \/ -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 recn 
 |-  ( N e. RR -> N e. CC )
3 2 negeq0d 
 |-  ( N e. RR -> ( N = 0 <-> -u N = 0 ) )
4 3 orbi2d 
 |-  ( N e. RR -> ( ( -u N e. NN \/ N = 0 ) <-> ( -u N e. NN \/ -u N = 0 ) ) )
5 elnn0 
 |-  ( -u N e. NN0 <-> ( -u N e. NN \/ -u N = 0 ) )
6 4 5 syl6rbbr 
 |-  ( N e. RR -> ( -u N e. NN0 <-> ( -u N e. NN \/ N = 0 ) ) )
7 6 orbi2d 
 |-  ( N e. RR -> ( ( N e. NN \/ -u N e. NN0 ) <-> ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) ) )
8 3orrot 
 |-  ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N e. NN \/ -u N e. NN \/ N = 0 ) )
9 3orass 
 |-  ( ( N e. NN \/ -u N e. NN \/ N = 0 ) <-> ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) )
10 8 9 bitri 
 |-  ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N e. NN \/ ( -u N e. NN \/ N = 0 ) ) )
11 7 10 syl6rbbr 
 |-  ( N e. RR -> ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( N e. NN \/ -u N e. NN0 ) ) )
12 11 pm5.32i 
 |-  ( ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) <-> ( N e. RR /\ ( N e. NN \/ -u N e. NN0 ) ) )
13 1 12 bitri 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N e. NN \/ -u N e. NN0 ) ) )