Theorem leneg2d

Description: Negative of one side of 'less than or equal to'. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	leneg2d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	leneg2d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
Assertion	leneg2d	⊢ ( 𝜑 → ( 𝐴 ≤ - 𝐵 ↔ 𝐵 ≤ - 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		leneg2d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		leneg2d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3	2	renegcld	⊢ ( 𝜑 → - 𝐵 ∈ ℝ )
4	1 3	lenegd	⊢ ( 𝜑 → ( 𝐴 ≤ - 𝐵 ↔ - - 𝐵 ≤ - 𝐴 ) )
5	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
6	5	negnegd	⊢ ( 𝜑 → - - 𝐵 = 𝐵 )
7	6	breq1d	⊢ ( 𝜑 → ( - - 𝐵 ≤ - 𝐴 ↔ 𝐵 ≤ - 𝐴 ) )
8	4 7	bitrd	⊢ ( 𝜑 → ( 𝐴 ≤ - 𝐵 ↔ 𝐵 ≤ - 𝐴 ) )