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