Metamath Proof Explorer


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

Proof

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