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	eqtrdi	⊢ ( 𝑁 = 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 )