Theorem mul2lt0rlt0

Description: If the result of a multiplication is strictly negative, then multiplicands are of different signs. (Contributed by Thierry Arnoux, 19-Sep-2018)

	Ref	Expression
Hypotheses	mul2lt0.1	|- ( ph -> A e. RR )
	mul2lt0.2	|- ( ph -> B e. RR )
	mul2lt0.3	|- ( ph -> ( A x. B ) < 0 )
Assertion	mul2lt0rlt0	|- ( ( ph /\ B < 0 ) -> 0 < A )

Proof

Step	Hyp	Ref	Expression
1		mul2lt0.1	|- ( ph -> A e. RR )
2		mul2lt0.2	|- ( ph -> B e. RR )
3		mul2lt0.3	|- ( ph -> ( A x. B ) < 0 )
4	1 2	remulcld	|- ( ph -> ( A x. B ) e. RR )
5	4	adantr	|- ( ( ph /\ B < 0 ) -> ( A x. B ) e. RR )
6		0red	|- ( ( ph /\ B < 0 ) -> 0 e. RR )
7		negelrp	|- ( B e. RR -> ( -u B e. RR+ <-> B < 0 ) )
8	2 7	syl	|- ( ph -> ( -u B e. RR+ <-> B < 0 ) )
9	8	biimpar	|- ( ( ph /\ B < 0 ) -> -u B e. RR+ )
10	3	adantr	|- ( ( ph /\ B < 0 ) -> ( A x. B ) < 0 )
11	5 6 9 10	ltdiv1dd	|- ( ( ph /\ B < 0 ) -> ( ( A x. B ) / -u B ) < ( 0 / -u B ) )
12	1	recnd	|- ( ph -> A e. CC )
13	12	adantr	|- ( ( ph /\ B < 0 ) -> A e. CC )
14	2	recnd	|- ( ph -> B e. CC )
15	14	adantr	|- ( ( ph /\ B < 0 ) -> B e. CC )
16	13 15	mulcld	|- ( ( ph /\ B < 0 ) -> ( A x. B ) e. CC )
17		simpr	|- ( ( ph /\ B < 0 ) -> B < 0 )
18	17	lt0ne0d	|- ( ( ph /\ B < 0 ) -> B =/= 0 )
19	16 15 18	divneg2d	|- ( ( ph /\ B < 0 ) -> -u ( ( A x. B ) / B ) = ( ( A x. B ) / -u B ) )
20	13 15 18	divcan4d	|- ( ( ph /\ B < 0 ) -> ( ( A x. B ) / B ) = A )
21	20	negeqd	|- ( ( ph /\ B < 0 ) -> -u ( ( A x. B ) / B ) = -u A )
22	19 21	eqtr3d	|- ( ( ph /\ B < 0 ) -> ( ( A x. B ) / -u B ) = -u A )
23	15	negcld	|- ( ( ph /\ B < 0 ) -> -u B e. CC )
24	15 18	negne0d	|- ( ( ph /\ B < 0 ) -> -u B =/= 0 )
25	23 24	div0d	|- ( ( ph /\ B < 0 ) -> ( 0 / -u B ) = 0 )
26	11 22 25	3brtr3d	|- ( ( ph /\ B < 0 ) -> -u A < 0 )
27	1	adantr	|- ( ( ph /\ B < 0 ) -> A e. RR )
28	27	lt0neg2d	|- ( ( ph /\ B < 0 ) -> ( 0 < A <-> -u A < 0 ) )
29	26 28	mpbird	|- ( ( ph /\ B < 0 ) -> 0 < A )