Theorem lenegcon2

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 8-Oct-2005)

	Ref	Expression
Assertion	lenegcon2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ - 𝐵 ↔ 𝐵 ≤ - 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		renegcl	⊢ ( 𝐵 ∈ ℝ → - 𝐵 ∈ ℝ )
2		leneg	⊢ ( ( 𝐴 ∈ ℝ ∧ - 𝐵 ∈ ℝ ) → ( 𝐴 ≤ - 𝐵 ↔ - - 𝐵 ≤ - 𝐴 ) )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ - 𝐵 ↔ - - 𝐵 ≤ - 𝐴 ) )
4		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
5	4	negnegd	⊢ ( 𝐵 ∈ ℝ → - - 𝐵 = 𝐵 )
6	5	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → - - 𝐵 = 𝐵 )
7	6	breq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - - 𝐵 ≤ - 𝐴 ↔ 𝐵 ≤ - 𝐴 ) )
8	3 7	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ - 𝐵 ↔ 𝐵 ≤ - 𝐴 ) )