Metamath Proof Explorer

Theorem reorelicc

Description: Membership in and outside of a closed real interval. (Contributed by AV, 15-Feb-2023)

Ref Expression
Assertion reorelicc 
|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C < A \/ C e. ( A [,] B ) \/ B < C ) )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( C < A -> ( C < A \/ C e. ( A [,] B ) ) )
2 1 a1d 
 |-  ( C < A -> ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) -> ( C < A \/ C e. ( A [,] B ) ) ) )
3 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
4 3 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> C e. RR )
5 lenlt 
 |-  ( ( A e. RR /\ C e. RR ) -> ( A <_ C <-> -. C < A ) )
6 5 biimprd 
 |-  ( ( A e. RR /\ C e. RR ) -> ( -. C < A -> A <_ C ) )
7 6 3adant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. C < A -> A <_ C ) )
8 7 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) -> ( -. C < A -> A <_ C ) )
9 8 imp 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> A <_ C )
10 simplr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> C <_ B )
11 3simpa 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A e. RR /\ B e. RR ) )
12 11 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> ( A e. RR /\ B e. RR ) )
13 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
14 12 13 syl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) )
15 4 9 10 14 mpbir3and 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> C e. ( A [,] B ) )
16 15 olcd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) /\ -. C < A ) -> ( C < A \/ C e. ( A [,] B ) ) )
17 16 expcom 
 |-  ( -. C < A -> ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) -> ( C < A \/ C e. ( A [,] B ) ) ) )
18 2 17 pm2.61i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) -> ( C < A \/ C e. ( A [,] B ) ) )
19 18 orcd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ C <_ B ) -> ( ( C < A \/ C e. ( A [,] B ) ) \/ B < C ) )
20 19 ex 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C <_ B -> ( ( C < A \/ C e. ( A [,] B ) ) \/ B < C ) ) )
21 olc 
 |-  ( B < C -> ( ( C < A \/ C e. ( A [,] B ) ) \/ B < C ) )
22 21 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B < C -> ( ( C < A \/ C e. ( A [,] B ) ) \/ B < C ) ) )
23 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
24 lelttric 
 |-  ( ( C e. RR /\ B e. RR ) -> ( C <_ B \/ B < C ) )
25 3 23 24 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C <_ B \/ B < C ) )
26 20 22 25 mpjaod 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( C < A \/ C e. ( A [,] B ) ) \/ B < C ) )
27 df-3or 
 |-  ( ( C < A \/ C e. ( A [,] B ) \/ B < C ) <-> ( ( C < A \/ C e. ( A [,] B ) ) \/ B < C ) )
28 26 27 sylibr 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C < A \/ C e. ( A [,] B ) \/ B < C ) )