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

Metamath Proof Explorer

Theorem xrlenltd

Description: "Less than or equal to" expressed in terms of "less than", for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xrlenltd.a ⊢ φ → A ∈ ℝ *
xrlenltd.b ⊢ φ → B ∈ ℝ *
Assertion xrlenltd ⊢ φ → A ≤ B ↔ ¬ B < A

Proof

Step Hyp Ref Expression
1 xrlenltd.a ⊢ φ → A ∈ ℝ *
2 xrlenltd.b ⊢ φ → B ∈ ℝ *
3 xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A
4 1 2 3 syl2anc ⊢ φ → A ≤ B ↔ ¬ B < A