Theorem elicod

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

	Ref	Expression
Hypotheses	elicod.a	|- ( ph -> A e. RR* )
	elicod.b	|- ( ph -> B e. RR* )
	elicod.3	|- ( ph -> C e. RR* )
	elicod.4	|- ( ph -> A <_ C )
	elicod.5	|- ( ph -> C < B )
Assertion	elicod	|- ( ph -> C e. ( A [,) B ) )

Proof

Step	Hyp	Ref	Expression
1		elicod.a	|- ( ph -> A e. RR* )
2		elicod.b	|- ( ph -> B e. RR* )
3		elicod.3	|- ( ph -> C e. RR* )
4		elicod.4	|- ( ph -> A <_ C )
5		elicod.5	|- ( ph -> C < B )
6		elico1	|- ( ( 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 ) )