Theorem le2tri3i

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

	Ref	Expression
Hypotheses	lt.1	⊢ 𝐴 ∈ ℝ
	lt.2	⊢ 𝐵 ∈ ℝ
	lt.3	⊢ 𝐶 ∈ ℝ
Assertion	le2tri3i	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		lt.1	⊢ 𝐴 ∈ ℝ
2		lt.2	⊢ 𝐵 ∈ ℝ
3		lt.3	⊢ 𝐶 ∈ ℝ
4	2 3 1	letri	⊢ ( ( 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → 𝐵 ≤ 𝐴 )
5	1 2	letri3i	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) )
6	5	biimpri	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) → 𝐴 = 𝐵 )
7	4 6	sylan2	⊢ ( ( 𝐴 ≤ 𝐵 ∧ ( 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ) → 𝐴 = 𝐵 )
8	7	3impb	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → 𝐴 = 𝐵 )
9	3 1 2	letri	⊢ ( ( 𝐶 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) → 𝐶 ≤ 𝐵 )
10	2 3	letri3i	⊢ ( 𝐵 = 𝐶 ↔ ( 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) )
11	10	biimpri	⊢ ( ( 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) → 𝐵 = 𝐶 )
12	9 11	sylan2	⊢ ( ( 𝐵 ≤ 𝐶 ∧ ( 𝐶 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) → 𝐵 = 𝐶 )
13	12	3impb	⊢ ( ( 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) → 𝐵 = 𝐶 )
14	13	3comr	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → 𝐵 = 𝐶 )
15	1 2 3	letri	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ) → 𝐴 ≤ 𝐶 )
16	1 3	letri3i	⊢ ( 𝐴 = 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) )
17	16	biimpri	⊢ ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → 𝐴 = 𝐶 )
18	17	eqcomd	⊢ ( ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → 𝐶 = 𝐴 )
19	15 18	stoic3	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → 𝐶 = 𝐴 )
20	8 14 19	3jca	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) → ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴 ) )
21	1	eqlei	⊢ ( 𝐴 = 𝐵 → 𝐴 ≤ 𝐵 )
22	2	eqlei	⊢ ( 𝐵 = 𝐶 → 𝐵 ≤ 𝐶 )
23	3	eqlei	⊢ ( 𝐶 = 𝐴 → 𝐶 ≤ 𝐴 )
24	21 22 23	3anim123i	⊢ ( ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴 ) → ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) )
25	20 24	impbii	⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴 ) )