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 ⊢ N ∈ ℤ ≥ 3 → N − 2 ∈ ℕ

Proof

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