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

Metamath Proof Explorer

Theorem xlenegcon1

Description: Extended real version of lenegcon1 . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Assertion xlenegcon1 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A ≤ B ↔ − B ≤ A

Proof

Step Hyp Ref Expression
1 xnegcl ⊢ A ∈ ℝ * → − A ∈ ℝ *
2 xleneg ⊢ − A ∈ ℝ * ∧ B ∈ ℝ * → − A ≤ B ↔ − B ≤ − − A
3 1 2 sylan ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A ≤ B ↔ − B ≤ − − A
4 xnegneg ⊢ A ∈ ℝ * → − − A = A
5 4 breq2d ⊢ A ∈ ℝ * → − B ≤ − − A ↔ − B ≤ A
6 5 adantr ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − B ≤ − − A ↔ − B ≤ A
7 3 6 bitrd ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → − A ≤ B ↔ − B ≤ A