Theorem eluz2b2

Description: Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012)

	Ref	Expression
Assertion	eluz2b2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2b1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
2		1re	⊢ 1 ∈ ℝ
3		zre	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
4		ltle	⊢ ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 1 < 𝑁 → 1 ≤ 𝑁 ) )
5	2 3 4	sylancr	⊢ ( 𝑁 ∈ ℤ → ( 1 < 𝑁 → 1 ≤ 𝑁 ) )
6	5	imdistani	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) )
7		elnnz1	⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℤ ∧ 1 ≤ 𝑁 ) )
8	6 7	sylibr	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) → 𝑁 ∈ ℕ )
9		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) → 1 < 𝑁 )
10	8 9	jca	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) → ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
11		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
12	11	anim1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) → ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) )
13	10 12	impbii	⊢ ( ( 𝑁 ∈ ℤ ∧ 1 < 𝑁 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
14	1 13	bitri	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )