Metamath Proof Explorer


Theorem mulgt0con2d

Description: Lemma for mulgt0b2d and contrapositive of mulgt0 . (Contributed by SN, 26-Jun-2024)

Ref Expression
Hypotheses mulgt0con2d.a
|- ( ph -> A e. RR )
mulgt0con2d.b
|- ( ph -> B e. RR )
mulgt0con2d.1
|- ( ph -> 0 < A )
mulgt0con2d.2
|- ( ph -> ( A x. B ) < 0 )
Assertion mulgt0con2d
|- ( ph -> B < 0 )

Proof

Step Hyp Ref Expression
1 mulgt0con2d.a
 |-  ( ph -> A e. RR )
2 mulgt0con2d.b
 |-  ( ph -> B e. RR )
3 mulgt0con2d.1
 |-  ( ph -> 0 < A )
4 mulgt0con2d.2
 |-  ( ph -> ( A x. B ) < 0 )
5 1 2 remulcld
 |-  ( ph -> ( A x. B ) e. RR )
6 1 adantr
 |-  ( ( ph /\ 0 < B ) -> A e. RR )
7 2 adantr
 |-  ( ( ph /\ 0 < B ) -> B e. RR )
8 3 adantr
 |-  ( ( ph /\ 0 < B ) -> 0 < A )
9 simpr
 |-  ( ( ph /\ 0 < B ) -> 0 < B )
10 6 7 8 9 mulgt0d
 |-  ( ( ph /\ 0 < B ) -> 0 < ( A x. B ) )
11 10 ex
 |-  ( ph -> ( 0 < B -> 0 < ( A x. B ) ) )
12 remul01
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
13 1 12 syl
 |-  ( ph -> ( A x. 0 ) = 0 )
14 oveq2
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
15 14 eqeq1d
 |-  ( B = 0 -> ( ( A x. B ) = 0 <-> ( A x. 0 ) = 0 ) )
16 13 15 syl5ibrcom
 |-  ( ph -> ( B = 0 -> ( A x. B ) = 0 ) )
17 2 5 11 16 mulgt0con1dlem
 |-  ( ph -> ( ( A x. B ) < 0 -> B < 0 ) )
18 4 17 mpd
 |-  ( ph -> B < 0 )