Metamath Proof Explorer

Theorem nn0ge2m1nnALT

Description: Alternate proof of nn0ge2m1nn : If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 , a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn . (Contributed by Alexander van der Vekens, 1-Aug-2018) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 a1i ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → 2 ∈ ℤ
3 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
4 3 adantr ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N ∈ ℤ
5 simpr ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → 2 ≤ N
6 eluz2 ⊢ N ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ N ∈ ℤ ∧ 2 ≤ N
7 2 4 5 6 syl3anbrc ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N ∈ ℤ ≥ 2
8 uz2m1nn ⊢ N ∈ ℤ ≥ 2 → N − 1 ∈ ℕ
9 7 8 syl ⊢ N ∈ ℕ 0 ∧ 2 ≤ N → N − 1 ∈ ℕ