Metamath Proof Explorer


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 ) )