Metamath Proof Explorer

Theorem ltnegcon1

Description: Contraposition of negative in 'less than'. (Contributed by NM, 8-Nov-2004)

Ref Expression
Assertion ltnegcon1 ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A < B ↔ − B < A

Proof

Step Hyp Ref Expression
1 renegcl ⊢ A ∈ ℝ → − A ∈ ℝ
2 ltneg ⊢ − A ∈ ℝ ∧ B ∈ ℝ → − A < B ↔ − B < − − A
3 1 2 sylan ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A < B ↔ − B < − − A
4 simpl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℝ
5 4 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ∈ ℂ
6 5 negnegd ⊢ A ∈ ℝ ∧ B ∈ ℝ → − − A = A
7 6 breq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ → − B < − − A ↔ − B < A
8 3 7 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A < B ↔ − B < A