Metamath Proof Explorer


Theorem eliood

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

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

Proof

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