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

Metamath Proof Explorer

Theorem xrlenlt

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A

Proof

Step Hyp Ref Expression
1 df-br ⊢ A ≤ B ↔ A B ∈ ≤
2 opelxpi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A B ∈ ℝ * × ℝ *
3 df-le ⊢ ≤ = ℝ * × ℝ * ∖ < -1
4 3 eleq2i ⊢ A B ∈ ≤ ↔ A B ∈ ℝ * × ℝ * ∖ < -1
5 eldif ⊢ A B ∈ ℝ * × ℝ * ∖ < -1 ↔ A B ∈ ℝ * × ℝ * ∧ ¬ A B ∈ < -1
6 4 5 bitri ⊢ A B ∈ ≤ ↔ A B ∈ ℝ * × ℝ * ∧ ¬ A B ∈ < -1
7 6 baib ⊢ A B ∈ ℝ * × ℝ * → A B ∈ ≤ ↔ ¬ A B ∈ < -1
8 2 7 syl ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A B ∈ ≤ ↔ ¬ A B ∈ < -1
9 1 8 bitrid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ A B ∈ < -1
10 df-br ⊢ B < A ↔ B A ∈ <
11 opelcnvg ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A B ∈ < -1 ↔ B A ∈ <
12 10 11 bitr4id ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B < A ↔ A B ∈ < -1
13 12 notbid ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → ¬ B < A ↔ ¬ A B ∈ < -1
14 9 13 bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A