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 ) )