This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 = 0 ∨ 𝐾 ∈ ( 1 ..^ 𝑁 ) ) )

Proof

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