Theorem eliccxrd

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

	Ref	Expression
Hypotheses	eliccxrd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	eliccxrd.2	$$⊢\phi \to B\in {ℝ}^{*}$$
	eliccxrd.3	$$⊢\phi \to C\in {ℝ}^{*}$$
	eliccxrd.4	$$⊢\phi \to A\le C$$
	eliccxrd.5	$$⊢\phi \to C\le B$$
Assertion	eliccxrd	$$⊢\phi \to C\in \left[A,B\right]$$

Proof

Step	Hyp	Ref	Expression
1		eliccxrd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		eliccxrd.2	$$⊢\phi \to B\in {ℝ}^{*}$$
3		eliccxrd.3	$$⊢\phi \to C\in {ℝ}^{*}$$
4		eliccxrd.4	$$⊢\phi \to A\le C$$
5		eliccxrd.5	$$⊢\phi \to C\le B$$
6	4 5	jca	$$⊢\phi \to \left(A\le C\wedge C\le B\right)$$
7		elicc4	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge C\in {ℝ}^{*}\right)\to \left(C\in \left[A,B\right]\leftrightarrow \left(A\le C\wedge C\le B\right)\right)$$
8	1 2 3 7	syl3anc	$$⊢\phi \to \left(C\in \left[A,B\right]\leftrightarrow \left(A\le C\wedge C\le B\right)\right)$$
9	6 8	mpbird	$$⊢\phi \to C\in \left[A,B\right]$$