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 ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )

Proof

Step Hyp Ref Expression
1 nn1m1nn ( 𝑁 ∈ ℕ → ( 𝑁 = 1 ∨ ( 𝑁 − 1 ) ∈ ℕ ) )
2 oveq1 ( 𝑁 = 1 → ( 𝑁 − 1 ) = ( 1 − 1 ) )
3 1m1e0 ( 1 − 1 ) = 0
4 2 3 syl6eq ( 𝑁 = 1 → ( 𝑁 − 1 ) = 0 )
5 4 orim1i ( ( 𝑁 = 1 ∨ ( 𝑁 − 1 ) ∈ ℕ ) → ( ( 𝑁 − 1 ) = 0 ∨ ( 𝑁 − 1 ) ∈ ℕ ) )
6 1 5 syl ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) = 0 ∨ ( 𝑁 − 1 ) ∈ ℕ ) )
7 6 orcomd ( 𝑁 ∈ ℕ → ( ( 𝑁 − 1 ) ∈ ℕ ∨ ( 𝑁 − 1 ) = 0 ) )
8 elnn0 ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( ( 𝑁 − 1 ) ∈ ℕ ∨ ( 𝑁 − 1 ) = 0 ) )
9 7 8 sylibr ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )