Metamath Proof Explorer


Theorem elnn0nn

Description: The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion elnn0nn N 0 N N + 1

Proof

Step Hyp Ref Expression
1 nn0cn N 0 N
2 nn0p1nn N 0 N + 1
3 1 2 jca N 0 N N + 1
4 simpl N N + 1 N
5 ax-1cn 1
6 pncan N 1 N + 1 - 1 = N
7 4 5 6 sylancl N N + 1 N + 1 - 1 = N
8 nnm1nn0 N + 1 N + 1 - 1 0
9 8 adantl N N + 1 N + 1 - 1 0
10 7 9 eqeltrrd N N + 1 N 0
11 3 10 impbii N 0 N N + 1