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 ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℕ ∧ 1 < N

Proof

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