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

Metamath Proof Explorer

Theorem leneg2d

Description: Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses leneg2d.1 ⊢ φ → A ∈ ℝ
leneg2d.2 ⊢ φ → B ∈ ℝ
Assertion leneg2d ⊢ φ → A ≤ − B ↔ B ≤ − A

Proof

Step Hyp Ref Expression
1 leneg2d.1 ⊢ φ → A ∈ ℝ
2 leneg2d.2 ⊢ φ → B ∈ ℝ
3 2 renegcld ⊢ φ → − B ∈ ℝ
4 1 3 lenegd ⊢ φ → A ≤ − B ↔ − − B ≤ − A
5 2 recnd ⊢ φ → B ∈ ℂ
6 5 negnegd ⊢ φ → − − B = B
7 6 breq1d ⊢ φ → − − B ≤ − A ↔ B ≤ − A
8 4 7 bitrd ⊢ φ → A ≤ − B ↔ B ≤ − A