Metamath Proof Explorer

Theorem eluz2b1

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

Ref Expression
Assertion eluz2b1 ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 1 < N

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1 eluz1i ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 2 ≤ N
3 1z ⊢ 1 ∈ ℤ
4 zltp1le ⊢ 1 ∈ ℤ ∧ N ∈ ℤ → 1 < N ↔ 1 + 1 ≤ N
5 3 4 mpan ⊢ N ∈ ℤ → 1 < N ↔ 1 + 1 ≤ N
6 df-2 ⊢ 2 = 1 + 1
7 6 breq1i ⊢ 2 ≤ N ↔ 1 + 1 ≤ N
8 5 7 bitr4di ⊢ N ∈ ℤ → 1 < N ↔ 2 ≤ N
9 8 pm5.32i ⊢ N ∈ ℤ ∧ 1 < N ↔ N ∈ ℤ ∧ 2 ≤ N
10 2 9 bitr4i ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 1 < N