Description: Alternate version of nnne0 . A positive integer is nonzero. (Contributed by NM, 27-Sep-1999) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nnne0ALT | |- ( A e. NN -> A =/= 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0nnnALT | |- -. 0 e. NN |
|
| 2 | eleq1 | |- ( A = 0 -> ( A e. NN <-> 0 e. NN ) ) |
|
| 3 | 1 2 | mtbiri | |- ( A = 0 -> -. A e. NN ) |
| 4 | 3 | necon2ai | |- ( A e. NN -> A =/= 0 ) |