Theorem lelttric

Description: Trichotomy law. (Contributed by NM, 4-Apr-2005)

	Ref	Expression
Assertion	lelttric	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.1	⊢ ( ¬ 𝐵 < 𝐴 ∨ 𝐵 < 𝐴 )
2		lenlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 ) )
3	2	orbi1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴 ) ↔ ( ¬ 𝐵 < 𝐴 ∨ 𝐵 < 𝐴 ) ) )
4	1 3	mpbiri	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴 ) )