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 ) ∈ ℕ )