Theorem leneg

Description: Negative of both sides of 'less than or equal to'. (Contributed by NM, 12-Sep-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2		lesub2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 0 − 𝐵 ) ≤ ( 0 − 𝐴 ) ) )
3	1 2	mp3an3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ ( 0 − 𝐵 ) ≤ ( 0 − 𝐴 ) ) )
4		df-neg	⊢ - 𝐵 = ( 0 − 𝐵 )
5		df-neg	⊢ - 𝐴 = ( 0 − 𝐴 )
6	4 5	breq12i	⊢ ( - 𝐵 ≤ - 𝐴 ↔ ( 0 − 𝐵 ) ≤ ( 0 − 𝐴 ) )
7	3 6	bitr4di	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ≤ 𝐵 ↔ - 𝐵 ≤ - 𝐴 ) )