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 ) ) )