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

Metamath Proof Explorer

Theorem mulgt0con1d

Description: Counterpart to mulgt0con2d , though not a lemma. This is the first use of ax-pre-mulgt0 . One direction of mulgt0b2d . (Contributed by SN, 26-Jun-2024)

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

Proof

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