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

Metamath Proof Explorer

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 < 𝑁 ) )