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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < - 𝐵 ↔ 𝐵 < - 𝐴 ) )