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