This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltmulneg

Description: Multiplying by a negative number, swaps the order. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses ltmulneg.a 
|- ( ph -> A e. RR )
ltmulneg.b 
|- ( ph -> B e. RR )
ltmulneg.c 
|- ( ph -> C e. RR )
ltmulneg.n 
|- ( ph -> C < 0 )
Assertion ltmulneg 
|- ( ph -> ( A < B <-> ( B x. C ) < ( A x. C ) ) )

Proof

Step Hyp Ref Expression
1 ltmulneg.a 
 |-  ( ph -> A e. RR )
2 ltmulneg.b 
 |-  ( ph -> B e. RR )
3 ltmulneg.c 
 |-  ( ph -> C e. RR )
4 ltmulneg.n 
 |-  ( ph -> C < 0 )
5 3 4 negelrpd 
 |-  ( ph -> -u C e. RR+ )
6 1 2 5 ltmul1d 
 |-  ( ph -> ( A < B <-> ( A x. -u C ) < ( B x. -u C ) ) )
7 3 renegcld 
 |-  ( ph -> -u C e. RR )
8 1 7 remulcld 
 |-  ( ph -> ( A x. -u C ) e. RR )
9 2 7 remulcld 
 |-  ( ph -> ( B x. -u C ) e. RR )
10 8 9 ltnegd 
 |-  ( ph -> ( ( A x. -u C ) < ( B x. -u C ) <-> -u ( B x. -u C ) < -u ( A x. -u C ) ) )
11 2 recnd 
 |-  ( ph -> B e. CC )
12 7 recnd 
 |-  ( ph -> -u C e. CC )
13 11 12 mulneg2d 
 |-  ( ph -> ( B x. -u -u C ) = -u ( B x. -u C ) )
14 3 recnd 
 |-  ( ph -> C e. CC )
15 14 negnegd 
 |-  ( ph -> -u -u C = C )
16 15 oveq2d 
 |-  ( ph -> ( B x. -u -u C ) = ( B x. C ) )
17 13 16 eqtr3d 
 |-  ( ph -> -u ( B x. -u C ) = ( B x. C ) )
18 1 recnd 
 |-  ( ph -> A e. CC )
19 18 12 mulneg2d 
 |-  ( ph -> ( A x. -u -u C ) = -u ( A x. -u C ) )
20 15 oveq2d 
 |-  ( ph -> ( A x. -u -u C ) = ( A x. C ) )
21 19 20 eqtr3d 
 |-  ( ph -> -u ( A x. -u C ) = ( A x. C ) )
22 17 21 breq12d 
 |-  ( ph -> ( -u ( B x. -u C ) < -u ( A x. -u C ) <-> ( B x. C ) < ( A x. C ) ) )
23 6 10 22 3bitrd 
 |-  ( ph -> ( A < B <-> ( B x. C ) < ( A x. C ) ) )