Metamath Proof Explorer

Theorem relin01

Description: An interval law for less than or equal. (Contributed by Scott Fenton, 27-Jun-2013)

Ref Expression
Assertion relin01 
|- ( A e. RR -> ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) \/ 1 <_ A ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 letric 
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A <_ 1 \/ 1 <_ A ) )
3 1 2 mpan2 
 |-  ( A e. RR -> ( A <_ 1 \/ 1 <_ A ) )
4 0re 
 |-  0 e. RR
5 letric 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A <_ 0 \/ 0 <_ A ) )
6 4 5 mpan2 
 |-  ( A e. RR -> ( A <_ 0 \/ 0 <_ A ) )
7 pm3.21 
 |-  ( A <_ 1 -> ( 0 <_ A -> ( 0 <_ A /\ A <_ 1 ) ) )
8 7 orim2d 
 |-  ( A <_ 1 -> ( ( A <_ 0 \/ 0 <_ A ) -> ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) ) ) )
9 6 8 syl5com 
 |-  ( A e. RR -> ( A <_ 1 -> ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) ) ) )
10 9 orim1d 
 |-  ( A e. RR -> ( ( A <_ 1 \/ 1 <_ A ) -> ( ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) ) \/ 1 <_ A ) ) )
11 3 10 mpd 
 |-  ( A e. RR -> ( ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) ) \/ 1 <_ A ) )
12 df-3or 
 |-  ( ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) \/ 1 <_ A ) <-> ( ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) ) \/ 1 <_ A ) )
13 11 12 sylibr 
 |-  ( A e. RR -> ( A <_ 0 \/ ( 0 <_ A /\ A <_ 1 ) \/ 1 <_ A ) )