Metamath Proof Explorer


Theorem eliccelicod

Description: A member of a closed interval that is not the upper bound, is a member of the left-closed, right-open interval. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses eliccelicod.a φ A *
eliccelicod.b φ B *
eliccelicod.c φ C A B
eliccelicod.d φ C B
Assertion eliccelicod φ C A B

Proof

Step Hyp Ref Expression
1 eliccelicod.a φ A *
2 eliccelicod.b φ B *
3 eliccelicod.c φ C A B
4 eliccelicod.d φ C B
5 eliccxr C A B C *
6 3 5 syl φ C *
7 iccgelb A * B * C A B A C
8 1 2 3 7 syl3anc φ A C
9 iccleub A * B * C A B C B
10 1 2 3 9 syl3anc φ C B
11 6 2 10 4 xrleneltd φ C < B
12 1 2 6 8 11 elicod φ C A B