Theorem eliccxrd

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

	Ref	Expression
Hypotheses	eliccxrd.1	|- ( ph -> A e. RR* )
	eliccxrd.2	|- ( ph -> B e. RR* )
	eliccxrd.3	|- ( ph -> C e. RR* )
	eliccxrd.4	|- ( ph -> A <_ C )
	eliccxrd.5	|- ( ph -> C <_ B )
Assertion	eliccxrd	|- ( ph -> C e. ( A [,] B ) )

Proof

Step	Hyp	Ref	Expression
1		eliccxrd.1	|- ( ph -> A e. RR* )
2		eliccxrd.2	|- ( ph -> B e. RR* )
3		eliccxrd.3	|- ( ph -> C e. RR* )
4		eliccxrd.4	|- ( ph -> A <_ C )
5		eliccxrd.5	|- ( ph -> C <_ B )
6	4 5	jca	|- ( ph -> ( A <_ C /\ C <_ B ) )
7		elicc4	|- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
8	1 2 3 7	syl3anc	|- ( ph -> ( C e. ( A [,] B ) <-> ( A <_ C /\ C <_ B ) ) )
9	6 8	mpbird	|- ( ph -> C e. ( A [,] B ) )