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

Metamath Proof Explorer

Theorem lenegcon1

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004)

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

Proof

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