Metamath Proof Explorer


Theorem eliocre

Description: A member of a left-open right-closed interval of reals is real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion eliocre B C A B C

Proof

Step Hyp Ref Expression
1 df-ioc . = x * , y * z * | x < z z y
2 1 elixx3g C A B A * B * C * A < C C B
3 2 biimpi C A B A * B * C * A < C C B
4 3 simpld C A B A * B * C *
5 4 simp3d C A B C *
6 5 adantl B C A B C *
7 simpl B C A B B
8 mnfxr −∞ *
9 8 a1i C A B −∞ *
10 4 simp1d C A B A *
11 mnfle A * −∞ A
12 10 11 syl C A B −∞ A
13 3 simprd C A B A < C C B
14 13 simpld C A B A < C
15 9 10 5 12 14 xrlelttrd C A B −∞ < C
16 15 adantl B C A B −∞ < C
17 13 simprd C A B C B
18 17 adantl B C A B C B
19 xrre C * B −∞ < C C B C
20 6 7 16 18 19 syl22anc B C A B C