Metamath Proof Explorer

Theorem fzo1lb

Description: 1 is the left endpoint of a half-open integer range based at 1 iff the right endpoint is an integer greater than 1. (Contributed by AV, 4-Sep-2025)

Ref Expression
Assertion fzo1lb ⊢ 1 ∈ 1 ..^ N ↔ N ∈ ℤ ≥ 2

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 3anass ⊢ 1 ∈ ℤ ∧ N ∈ ℤ ∧ 1 < N ↔ 1 ∈ ℤ ∧ N ∈ ℤ ∧ 1 < N
3 1 2 mpbiran ⊢ 1 ∈ ℤ ∧ N ∈ ℤ ∧ 1 < N ↔ N ∈ ℤ ∧ 1 < N
4 fzolb ⊢ 1 ∈ 1 ..^ N ↔ 1 ∈ ℤ ∧ N ∈ ℤ ∧ 1 < N
5 eluz2b1 ⊢ N ∈ ℤ ≥ 2 ↔ N ∈ ℤ ∧ 1 < N
6 3 4 5 3bitr4i ⊢ 1 ∈ 1 ..^ N ↔ N ∈ ℤ ≥ 2