This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn0ge2m1nn0

Description: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018)

Ref Expression
Assertion nn0ge2m1nn0 ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 nn0ge2m1nn ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ
2 1 nnnn0d ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ 0