Description: An element of a left-open right-closed interval is larger than its lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | iocgtlb | |- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,] B ) ) -> A < C ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elioc1 | |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,] B ) <-> ( C e. RR* /\ A < C /\ C <_ B ) ) ) |
|
2 | simp2 | |- ( ( C e. RR* /\ A < C /\ C <_ B ) -> A < C ) |
|
3 | 1 2 | syl6bi | |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,] B ) -> A < C ) ) |
4 | 3 | 3impia | |- ( ( A e. RR* /\ B e. RR* /\ C e. ( A (,] B ) ) -> A < C ) |