Metamath Proof Explorer

Theorem lenegcon2

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005)

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

Proof

Step Hyp Ref Expression
1 renegcl ⊢ B ∈ ℝ → − B ∈ ℝ
2 leneg ⊢ A ∈ ℝ ∧ − B ∈ ℝ → A ≤ − B ↔ − − B ≤ − A
3 1 2 sylan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ − B ↔ − − B ≤ − A
4 recn ⊢ B ∈ ℝ → B ∈ ℂ
5 4 negnegd ⊢ B ∈ ℝ → − − B = B
6 5 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − B = B
7 6 breq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − B ≤ − A ↔ B ≤ − A
8 3 7 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ − B ↔ B ≤ − A