Metamath Proof Explorer


Theorem nnm1nn0

Description: A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007) (Revised by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nnm1nn0 N N 1 0

Proof

Step Hyp Ref Expression
1 nn1m1nn N N = 1 N 1
2 oveq1 N = 1 N 1 = 1 1
3 1m1e0 1 1 = 0
4 2 3 eqtrdi N = 1 N 1 = 0
5 4 orim1i N = 1 N 1 N 1 = 0 N 1
6 1 5 syl N N 1 = 0 N 1
7 6 orcomd N N 1 N 1 = 0
8 elnn0 N 1 0 N 1 N 1 = 0
9 7 8 sylibr N N 1 0