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

Metamath Proof Explorer

Theorem mul2lt0rgt0

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 mul2lt0rgt0 
|- ( ( ph /\ 0 < B ) -> A < 0 )

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 3 adantr 
 |-  ( ( ph /\ 0 < B ) -> ( A x. B ) < 0 )
5 2 adantr 
 |-  ( ( ph /\ 0 < B ) -> B e. RR )
6 5 recnd 
 |-  ( ( ph /\ 0 < B ) -> B e. CC )
7 6 mul02d 
 |-  ( ( ph /\ 0 < B ) -> ( 0 x. B ) = 0 )
8 4 7 breqtrrd 
 |-  ( ( ph /\ 0 < B ) -> ( A x. B ) < ( 0 x. B ) )
9 1 adantr 
 |-  ( ( ph /\ 0 < B ) -> A e. RR )
10 0red 
 |-  ( ( ph /\ 0 < B ) -> 0 e. RR )
11 simpr 
 |-  ( ( ph /\ 0 < B ) -> 0 < B )
12 5 11 elrpd 
 |-  ( ( ph /\ 0 < B ) -> B e. RR+ )
13 9 10 12 ltmul1d 
 |-  ( ( ph /\ 0 < B ) -> ( A < 0 <-> ( A x. B ) < ( 0 x. B ) ) )
14 8 13 mpbird 
 |-  ( ( ph /\ 0 < B ) -> A < 0 )