Metamath Proof Explorer


Theorem ltnegcon1

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

Ref Expression
Assertion ltnegcon1 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < 𝐴 ) )

Proof

Step Hyp Ref Expression
1 renegcl ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
2 ltneg ( ( - 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < - - 𝐴 ) )
3 1 2 sylan ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < - - 𝐴 ) )
4 simpl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
5 4 recnd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
6 5 negnegd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → - - 𝐴 = 𝐴 )
7 6 breq2d ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐵 < - - 𝐴 ↔ - 𝐵 < 𝐴 ) )
8 3 7 bitrd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 < 𝐵 ↔ - 𝐵 < 𝐴 ) )