Description: Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002)
Ref | Expression | ||
---|---|---|---|
Assertion | elnnz | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnre | |
|
2 | orc | |
|
3 | nngt0 | |
|
4 | 1 2 3 | jca31 | |
5 | idd | |
|
6 | lt0neg2 | |
|
7 | renegcl | |
|
8 | 0re | |
|
9 | ltnsym | |
|
10 | 7 8 9 | sylancl | |
11 | 6 10 | sylbid | |
12 | 11 | imp | |
13 | nngt0 | |
|
14 | 12 13 | nsyl | |
15 | gt0ne0 | |
|
16 | 15 | neneqd | |
17 | ioran | |
|
18 | 14 16 17 | sylanbrc | |
19 | 18 | pm2.21d | |
20 | 5 19 | jaod | |
21 | 20 | ex | |
22 | 21 | com23 | |
23 | 22 | imp31 | |
24 | 4 23 | impbii | |
25 | elz | |
|
26 | 3orrot | |
|
27 | 3orass | |
|
28 | 26 27 | bitri | |
29 | 28 | anbi2i | |
30 | 25 29 | bitri | |
31 | 30 | anbi1i | |
32 | 24 31 | bitr4i | |