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

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

Proof

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