Description: A member of a closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | eliccre | |- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> C e. RR ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elicc2 | |- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) ) |
|
2 | 1 | biimp3a | |- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> ( C e. RR /\ A <_ C /\ C <_ B ) ) |
3 | 2 | simp1d | |- ( ( A e. RR /\ B e. RR /\ C e. ( A [,] B ) ) -> C e. RR ) |