# Metamath Proof Explorer

## Theorem elicod

Description: Membership in a left-closed right-open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses elicod.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
elicod.b ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
elicod.3 ${⊢}{\phi }\to {C}\in {ℝ}^{*}$
elicod.4 ${⊢}{\phi }\to {A}\le {C}$
elicod.5 ${⊢}{\phi }\to {C}<{B}$
Assertion elicod ${⊢}{\phi }\to {C}\in \left[{A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 elicod.a ${⊢}{\phi }\to {A}\in {ℝ}^{*}$
2 elicod.b ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
3 elicod.3 ${⊢}{\phi }\to {C}\in {ℝ}^{*}$
4 elicod.4 ${⊢}{\phi }\to {A}\le {C}$
5 elicod.5 ${⊢}{\phi }\to {C}<{B}$
6 elico1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left[{A},{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$
7 1 2 6 syl2anc ${⊢}{\phi }\to \left({C}\in \left[{A},{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}\le {C}\wedge {C}<{B}\right)\right)$
8 3 4 5 7 mpbir3and ${⊢}{\phi }\to {C}\in \left[{A},{B}\right)$