Metamath Proof Explorer


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
|- ( ph -> A e. RR )
leneg2d.2
|- ( ph -> B e. RR )
Assertion leneg2d
|- ( ph -> ( A <_ -u B <-> B <_ -u A ) )

Proof

Step Hyp Ref Expression
1 leneg2d.1
 |-  ( ph -> A e. RR )
2 leneg2d.2
 |-  ( ph -> B e. RR )
3 2 renegcld
 |-  ( ph -> -u B e. RR )
4 1 3 lenegd
 |-  ( ph -> ( A <_ -u B <-> -u -u B <_ -u A ) )
5 2 recnd
 |-  ( ph -> B e. CC )
6 5 negnegd
 |-  ( ph -> -u -u B = B )
7 6 breq1d
 |-  ( ph -> ( -u -u B <_ -u A <-> B <_ -u A ) )
8 4 7 bitrd
 |-  ( ph -> ( A <_ -u B <-> B <_ -u A ) )