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

Metamath Proof Explorer

Theorem xrleloe

Description: 'Less than or equal' expressed in terms of 'less than' or 'equals', for extended reals. (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrleloe ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ A < B ∨ A = B

Proof

Step Hyp Ref Expression
1 xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A
2 xrlttri ⊢ B ∈ ℝ * ∧ A ∈ ℝ * → B < A ↔ ¬ B = A ∨ A < B
3 2 ancoms ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B < A ↔ ¬ B = A ∨ A < B
4 3 con2bid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B = A ∨ A < B ↔ ¬ B < A
5 eqcom ⊢ B = A ↔ A = B
6 5 orbi1i ⊢ B = A ∨ A < B ↔ A = B ∨ A < B
7 orcom ⊢ A = B ∨ A < B ↔ A < B ∨ A = B
8 6 7 bitri ⊢ B = A ∨ A < B ↔ A < B ∨ A = B
9 4 8 bitr3di ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ¬ B < A ↔ A < B ∨ A = B
10 1 9 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ A < B ∨ A = B