Metamath Proof Explorer


Theorem ltnegcon2

Description: Contraposition of negative in 'less than'. (Contributed by Mario Carneiro, 25-Feb-2015)

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

Proof

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