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

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 )