Metamath Proof Explorer

Theorem elfzo0l

Description: A member of a half-open range of nonnegative integers is either 0 or a member of the corresponding half-open range of positive integers. (Contributed by AV, 5-Feb-2021)

Ref Expression
Assertion elfzo0l ⊢ K ∈ 0 ..^ N → K = 0 ∨ K ∈ 1 ..^ N

Proof

Step Hyp Ref Expression
1 elfzo0 ⊢ K ∈ 0 ..^ N ↔ K ∈ ℕ 0 ∧ N ∈ ℕ ∧ K < N
2 1 simp2bi ⊢ K ∈ 0 ..^ N → N ∈ ℕ
3 fzo0sn0fzo1 ⊢ N ∈ ℕ → 0 ..^ N = 0 ∪ 1 ..^ N
4 3 eleq2d ⊢ N ∈ ℕ → K ∈ 0 ..^ N ↔ K ∈ 0 ∪ 1 ..^ N
5 elun ⊢ K ∈ 0 ∪ 1 ..^ N ↔ K ∈ 0 ∨ K ∈ 1 ..^ N
6 elsni ⊢ K ∈ 0 → K = 0
7 6 orim1i ⊢ K ∈ 0 ∨ K ∈ 1 ..^ N → K = 0 ∨ K ∈ 1 ..^ N
8 5 7 sylbi ⊢ K ∈ 0 ∪ 1 ..^ N → K = 0 ∨ K ∈ 1 ..^ N
9 4 8 biimtrdi ⊢ N ∈ ℕ → K ∈ 0 ..^ N → K = 0 ∨ K ∈ 1 ..^ N
10 2 9 mpcom ⊢ K ∈ 0 ..^ N → K = 0 ∨ K ∈ 1 ..^ N