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

Metamath Proof Explorer

Theorem elfz0lmr

Description: A member of a finite interval of nonnegative integers is either 0 or its upper bound or an element of its interior. (Contributed by AV, 5-Feb-2021)

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

Proof

Step Hyp Ref Expression
1 elfzlmr ⊢ K ∈ 0 … N → K = 0 ∨ K ∈ 0 + 1 ..^ N ∨ K = N
2 biid ⊢ K = 0 ↔ K = 0
3 0p1e1 ⊢ 0 + 1 = 1
4 3 oveq1i ⊢ 0 + 1 ..^ N = 1 ..^ N
5 4 eleq2i ⊢ K ∈ 0 + 1 ..^ N ↔ K ∈ 1 ..^ N
6 biid ⊢ K = N ↔ K = N
7 2 5 6 3orbi123i ⊢ K = 0 ∨ K ∈ 0 + 1 ..^ N ∨ K = N ↔ K = 0 ∨ K ∈ 1 ..^ N ∨ K = N
8 1 7 sylib ⊢ K ∈ 0 … N → K = 0 ∨ K ∈ 1 ..^ N ∨ K = N