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 ⊢ 𝐴 ∈ ℝ
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 ⊢ ( ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ↔ ( 𝐴 = 𝐵 ∧ 𝐵 = 𝐶 ∧ 𝐶 = 𝐴 ) )