This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem le2tri3i

Description: Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000)

Ref Expression
Hypotheses lt.1 
|- A e. RR
lt.2 
|- B e. RR
lt.3 
|- C e. RR
Assertion le2tri3i 
|- ( ( A <_ B /\ B <_ C /\ C <_ A ) <-> ( A = B /\ B = C /\ C = A ) )

Proof

Step Hyp Ref Expression
1 lt.1 
 |-  A e. RR
2 lt.2 
 |-  B e. RR
3 lt.3 
 |-  C e. RR
4 2 3 1 letri 
 |-  ( ( B <_ C /\ C <_ A ) -> B <_ A )
5 1 2 letri3i 
 |-  ( A = B <-> ( A <_ B /\ B <_ A ) )
6 5 biimpri 
 |-  ( ( A <_ B /\ B <_ A ) -> A = B )
7 4 6 sylan2 
 |-  ( ( A <_ B /\ ( B <_ C /\ C <_ A ) ) -> A = B )
8 7 3impb 
 |-  ( ( A <_ B /\ B <_ C /\ C <_ A ) -> A = B )
9 3 1 2 letri 
 |-  ( ( C <_ A /\ A <_ B ) -> C <_ B )
10 2 3 letri3i 
 |-  ( B = C <-> ( B <_ C /\ C <_ B ) )
11 10 biimpri 
 |-  ( ( B <_ C /\ C <_ B ) -> B = C )
12 9 11 sylan2 
 |-  ( ( B <_ C /\ ( C <_ A /\ A <_ B ) ) -> B = C )
13 12 3impb 
 |-  ( ( B <_ C /\ C <_ A /\ A <_ B ) -> B = C )
14 13 3comr 
 |-  ( ( A <_ B /\ B <_ C /\ C <_ A ) -> B = C )
15 1 2 3 letri 
 |-  ( ( A <_ B /\ B <_ C ) -> A <_ C )
16 1 3 letri3i 
 |-  ( A = C <-> ( A <_ C /\ C <_ A ) )
17 16 biimpri 
 |-  ( ( A <_ C /\ C <_ A ) -> A = C )
18 17 eqcomd 
 |-  ( ( A <_ C /\ C <_ A ) -> C = A )
19 15 18 stoic3 
 |-  ( ( A <_ B /\ B <_ C /\ C <_ A ) -> C = A )
20 8 14 19 3jca 
 |-  ( ( A <_ B /\ B <_ C /\ C <_ A ) -> ( A = B /\ B = C /\ C = A ) )
21 1 eqlei 
 |-  ( A = B -> A <_ B )
22 2 eqlei 
 |-  ( B = C -> B <_ C )
23 3 eqlei 
 |-  ( C = A -> C <_ A )
24 21 22 23 3anim123i 
 |-  ( ( A = B /\ B = C /\ C = A ) -> ( A <_ B /\ B <_ C /\ C <_ A ) )
25 20 24 impbii 
 |-  ( ( A <_ B /\ B <_ C /\ C <_ A ) <-> ( A = B /\ B = C /\ C = A ) )