Metamath Proof Explorer

Theorem elfzlmr

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

Ref Expression
Assertion elfzlmr ⊢ K ∈ M … N → K = M ∨ K ∈ M + 1 ..^ N ∨ K = N

Proof

Step Hyp Ref Expression
1 elfzuz2 ⊢ K ∈ M … N → N ∈ ℤ ≥ M
2 fzpred ⊢ N ∈ ℤ ≥ M → M … N = M ∪ M + 1 … N
3 2 eleq2d ⊢ N ∈ ℤ ≥ M → K ∈ M … N ↔ K ∈ M ∪ M + 1 … N
4 elsni ⊢ K ∈ M → K = M
5 elfzr ⊢ K ∈ M + 1 … N → K ∈ M + 1 ..^ N ∨ K = N
6 4 5 orim12i ⊢ K ∈ M ∨ K ∈ M + 1 … N → K = M ∨ K ∈ M + 1 ..^ N ∨ K = N
7 elun ⊢ K ∈ M ∪ M + 1 … N ↔ K ∈ M ∨ K ∈ M + 1 … N
8 3orass ⊢ K = M ∨ K ∈ M + 1 ..^ N ∨ K = N ↔ K = M ∨ K ∈ M + 1 ..^ N ∨ K = N
9 6 7 8 3imtr4i ⊢ K ∈ M ∪ M + 1 … N → K = M ∨ K ∈ M + 1 ..^ N ∨ K = N
10 3 9 biimtrdi ⊢ N ∈ ℤ ≥ M → K ∈ M … N → K = M ∨ K ∈ M + 1 ..^ N ∨ K = N
11 1 10 mpcom ⊢ K ∈ M … N → K = M ∨ K ∈ M + 1 ..^ N ∨ K = N