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 eluzge3nn ( 𝑁 ∈ ( ℤ ‘ 3 ) → 𝑁 ∈ ℕ )
14 nnsub ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 2 < 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ ) )
15 12 13 14 sylancr ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 2 < 𝑁 ↔ ( 𝑁 − 2 ) ∈ ℕ ) )
16 11 15 mpbid ( 𝑁 ∈ ( ℤ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )