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 syl6eq ⊢ 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