Theorem eliccelicod

Description: A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	eliccelicod.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	eliccelicod.b	$$⊢\phi \to B\in {ℝ}^{*}$$
	eliccelicod.c	$$⊢\phi \to C\in \left[A,B\right]$$
	eliccelicod.d	$$⊢\phi \to C\ne B$$
Assertion	eliccelicod	$$⊢\phi \to C\in \left[A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eliccelicod.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		eliccelicod.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		eliccelicod.c	$$⊢\phi \to C\in \left[A,B\right]$$
4		eliccelicod.d	$$⊢\phi \to C\ne B$$
5		eliccxr	$$⊢C\in \left[A,B\right]\to C\in {ℝ}^{*}$$
6	3 5	syl	$$⊢\phi \to C\in {ℝ}^{*}$$
7		iccgelb	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in \left[A,B\right]\right)\to A\le C$$
8	1 2 3 7	syl3anc	$$⊢\phi \to A\le C$$
9		iccleub	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in \left[A,B\right]\right)\to C\le B$$
10	1 2 3 9	syl3anc	$$⊢\phi \to C\le B$$
11	6 2 10 4	xrleneltd	$$⊢\phi \to C<B$$
12	1 2 6 8 11	elicod	$$⊢\phi \to C\in \left[A,B\right)$$