Metamath Proof Explorer


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 )