| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elznn0nn |
|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) ) |
| 2 |
|
df-neg |
|- -u N = ( 0 - N ) |
| 3 |
|
0re |
|- 0 e. RR |
| 4 |
|
resubeqsub |
|- ( ( 0 e. RR /\ N e. RR ) -> ( 0 -R N ) = ( 0 - N ) ) |
| 5 |
3 4
|
mpan |
|- ( N e. RR -> ( 0 -R N ) = ( 0 - N ) ) |
| 6 |
2 5
|
eqtr4id |
|- ( N e. RR -> -u N = ( 0 -R N ) ) |
| 7 |
6
|
eleq1d |
|- ( N e. RR -> ( -u N e. NN <-> ( 0 -R N ) e. NN ) ) |
| 8 |
7
|
pm5.32i |
|- ( ( N e. RR /\ -u N e. NN ) <-> ( N e. RR /\ ( 0 -R N ) e. NN ) ) |
| 9 |
8
|
orbi2i |
|- ( ( N e. NN0 \/ ( N e. RR /\ -u N e. NN ) ) <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) ) |
| 10 |
1 9
|
bitri |
|- ( N e. ZZ <-> ( N e. NN0 \/ ( N e. RR /\ ( 0 -R N ) e. NN ) ) ) |