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

Metamath Proof Explorer

Theorem uz3m2nn

Description: An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn . (Contributed by Alexander van der Vekens, 17-Sep-2018)

Ref Expression
Assertion uz3m2nn ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ↔ ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) )
2 2lt3 ⊢ 2 < 3
3 2re ⊢ 2 ∈ ℝ
4 3re ⊢ 3 ∈ ℝ
5 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
6 ltletr ⊢ ( ( 2 ∈ ℝ ∧ 3 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 2 < 3 ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 ) )
7 3 4 5 6 mp3an12i ⊢ ( 𝑁 ∈ ℤ → ( ( 2 < 3 ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 ) )
8 2 7 mpani ⊢ ( 𝑁 ∈ ℤ → ( 3 ≤ 𝑁 → 2 < 𝑁 ) )
9 8 imp ⊢ ( ( 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 )
10 9 3adant1 ⊢ ( ( 3 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 3 ≤ 𝑁 ) → 2 < 𝑁 )
11 1 10 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 2 < 𝑁 )
12 2nn ⊢ 2 ∈ ℕ
13 eluz3nn ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℕ )
14 nnsub ⊢ ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 < 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ ) )
15 12 13 14 sylancr ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 2 < 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ ) )
16 11 15 mpbid ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )