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)\leftrightarrow \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)\leftrightarrow \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)$$