Theorem lenegcon1

Description: Contraposition of negative in 'less than or equal to'. (Contributed by NM, 10-May-2004)

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

Proof

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