Metamath Proof Explorer


Theorem elnnnn0

Description: The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004)

Ref Expression
Assertion elnnnn0 N N N 1 0

Proof

Step Hyp Ref Expression
1 nncn N N
2 npcan1 N N - 1 + 1 = N
3 2 eleq1d N N - 1 + 1 N
4 peano2cnm N N 1
5 4 biantrurd N N - 1 + 1 N 1 N - 1 + 1
6 3 5 bitr3d N N N 1 N - 1 + 1
7 elnn0nn N 1 0 N 1 N - 1 + 1
8 6 7 bitr4di N N N 1 0
9 1 8 biadanii N N N 1 0