Metamath Proof Explorer

Theorem elznn0nn

Description: Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004)

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

Proof

Step Hyp Ref Expression
1 elz 
 |-  ( N e. ZZ <-> ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) )
2 andi 
 |-  ( ( N e. RR /\ ( ( N = 0 \/ N e. NN ) \/ -u N e. NN ) ) <-> ( ( N e. RR /\ ( N = 0 \/ N e. NN ) ) \/ ( N e. RR /\ -u N e. NN ) ) )
3 df-3or 
 |-  ( ( N = 0 \/ N e. NN \/ -u N e. NN ) <-> ( ( N = 0 \/ N e. NN ) \/ -u N e. NN ) )
4 3 anbi2i 
 |-  ( ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) <-> ( N e. RR /\ ( ( N = 0 \/ N e. NN ) \/ -u N e. NN ) ) )
5 nn0re 
 |-  ( N e. NN0 -> N e. RR )
6 5 pm4.71ri 
 |-  ( N e. NN0 <-> ( N e. RR /\ N e. NN0 ) )
7 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
8 orcom 
 |-  ( ( N e. NN \/ N = 0 ) <-> ( N = 0 \/ N e. NN ) )
9 7 8 bitri 
 |-  ( N e. NN0 <-> ( N = 0 \/ N e. NN ) )
10 9 anbi2i 
 |-  ( ( N e. RR /\ N e. NN0 ) <-> ( N e. RR /\ ( N = 0 \/ N e. NN ) ) )
11 6 10 bitri 
 |-  ( N e. NN0 <-> ( N e. RR /\ ( N = 0 \/ N e. NN ) ) )
12 11 orbi1i 
 |-  ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) <-> ( ( N e. RR /\ ( N = 0 \/ N e. NN ) ) \/ ( N e. RR /\ -u N e. NN ) ) )
13 2 4 12 3bitr4i 
 |-  ( ( N e. RR /\ ( N = 0 \/ N e. NN \/ -u N e. NN ) ) <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )
14 1 13 bitri 
 |-  ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) )