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

Metamath Proof Explorer

Theorem xrlelttric

Description: Trichotomy law for extended reals. (Contributed by Thierry Arnoux, 12-Sep-2017)

Ref Expression
Assertion xrlelttric ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∨ B < A

Proof

Step Hyp Ref Expression
1 pm2.1 ⊢ ¬ B < A ∨ B < A
2 xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A
3 2 orbi1d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∨ B < A ↔ ¬ B < A ∨ B < A
4 1 3 mpbiri ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∨ B < A