Theorem eliocd

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

	Ref	Expression
Hypotheses	eliocd.a	|- ( ph -> A e. RR* )
	eliocd.b	|- ( ph -> B e. RR* )
	eliocd.c	|- ( ph -> C e. RR* )
	eliocd.altc	|- ( ph -> A < C )
	eliocd.cleb	|- ( ph -> C <_ B )
Assertion	eliocd	|- ( ph -> C e. ( A (,] B ) )

Proof

Step	Hyp	Ref	Expression
1		eliocd.a	|- ( ph -> A e. RR* )
2		eliocd.b	|- ( ph -> B e. RR* )
3		eliocd.c	|- ( ph -> C e. RR* )
4		eliocd.altc	|- ( ph -> A < C )
5		eliocd.cleb	|- ( ph -> C <_ B )
6		elioc1	|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
7	1 2 6	syl2anc	|- ( ph -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) )
8	3 4 5 7	mpbir3and	|- ( ph -> C e. ( A (,] B ) )