Theorem leneg3d

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

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

Proof

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