Metamath Proof Explorer

Theorem 1elfzo1

Description: 1 is in a half-open range of positive integers iff its upper bound is greater than 1. (Contributed by AV, 22-Nov-2022)

Ref Expression
Assertion 1elfzo1 ⊢ 1 ∈ 1 ..^ M ↔ M ∈ ℕ ∧ 1 < M

Proof

Step Hyp Ref Expression
1 elfzo1 ⊢ 1 ∈ 1 ..^ M ↔ 1 ∈ ℕ ∧ M ∈ ℕ ∧ 1 < M
2 1nn ⊢ 1 ∈ ℕ
3 3anass ⊢ 1 ∈ ℕ ∧ M ∈ ℕ ∧ 1 < M ↔ 1 ∈ ℕ ∧ M ∈ ℕ ∧ 1 < M
4 2 3 mpbiran ⊢ 1 ∈ ℕ ∧ M ∈ ℕ ∧ 1 < M ↔ M ∈ ℕ ∧ 1 < M
5 1 4 bitri ⊢ 1 ∈ 1 ..^ M ↔ M ∈ ℕ ∧ 1 < M