Metamath Proof Explorer

Theorem mulgt0b2d

Description: Biconditional, deductive form of mulgt0 . The second factor is positive iff the product is. Note that the commuted form cannot be proven since resubdi does not have a commuted form. (Contributed by SN, 26-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 mulgt0b2d.a 
 |-  ( ph -> A e. RR )
2 mulgt0b2d.b 
 |-  ( ph -> B e. RR )
3 mulgt0b2d.1 
 |-  ( ph -> 0 < A )
4 1 adantr 
 |-  ( ( ph /\ 0 < B ) -> A e. RR )
5 2 adantr 
 |-  ( ( ph /\ 0 < B ) -> B e. RR )
6 3 adantr 
 |-  ( ( ph /\ 0 < B ) -> 0 < A )
7 simpr 
 |-  ( ( ph /\ 0 < B ) -> 0 < B )
8 4 5 6 7 mulgt0d 
 |-  ( ( ph /\ 0 < B ) -> 0 < ( A x. B ) )
9 8 ex 
 |-  ( ph -> ( 0 < B -> 0 < ( A x. B ) ) )
10 1 adantr 
 |-  ( ( ph /\ ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) -> A e. RR )
11 1re 
 |-  1 e. RR
12 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
13 11 12 mp1i 
 |-  ( ph -> ( 0 -R 1 ) e. RR )
14 2 13 remulcld 
 |-  ( ph -> ( B x. ( 0 -R 1 ) ) e. RR )
15 14 adantr 
 |-  ( ( ph /\ ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) -> ( B x. ( 0 -R 1 ) ) e. RR )
16 3 adantr 
 |-  ( ( ph /\ ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) -> 0 < A )
17 1 recnd 
 |-  ( ph -> A e. CC )
18 2 recnd 
 |-  ( ph -> B e. CC )
19 13 recnd 
 |-  ( ph -> ( 0 -R 1 ) e. CC )
20 17 18 19 mulassd 
 |-  ( ph -> ( ( A x. B ) x. ( 0 -R 1 ) ) = ( A x. ( B x. ( 0 -R 1 ) ) ) )
21 20 breq1d 
 |-  ( ph -> ( ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 <-> ( A x. ( B x. ( 0 -R 1 ) ) ) < 0 ) )
22 21 biimpa 
 |-  ( ( ph /\ ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) -> ( A x. ( B x. ( 0 -R 1 ) ) ) < 0 )
23 10 15 16 22 mulgt0con2d 
 |-  ( ( ph /\ ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) -> ( B x. ( 0 -R 1 ) ) < 0 )
24 23 ex 
 |-  ( ph -> ( ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 -> ( B x. ( 0 -R 1 ) ) < 0 ) )
25 1 2 remulcld 
 |-  ( ph -> ( A x. B ) e. RR )
26 relt0neg2 
 |-  ( ( A x. B ) e. RR -> ( 0 < ( A x. B ) <-> ( 0 -R ( A x. B ) ) < 0 ) )
27 25 26 syl 
 |-  ( ph -> ( 0 < ( A x. B ) <-> ( 0 -R ( A x. B ) ) < 0 ) )
28 1red 
 |-  ( ph -> 1 e. RR )
29 25 28 remulneg2d 
 |-  ( ph -> ( ( A x. B ) x. ( 0 -R 1 ) ) = ( 0 -R ( ( A x. B ) x. 1 ) ) )
30 ax-1rid 
 |-  ( ( A x. B ) e. RR -> ( ( A x. B ) x. 1 ) = ( A x. B ) )
31 25 30 syl 
 |-  ( ph -> ( ( A x. B ) x. 1 ) = ( A x. B ) )
32 31 oveq2d 
 |-  ( ph -> ( 0 -R ( ( A x. B ) x. 1 ) ) = ( 0 -R ( A x. B ) ) )
33 29 32 eqtrd 
 |-  ( ph -> ( ( A x. B ) x. ( 0 -R 1 ) ) = ( 0 -R ( A x. B ) ) )
34 33 breq1d 
 |-  ( ph -> ( ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 <-> ( 0 -R ( A x. B ) ) < 0 ) )
35 27 34 bitr4d 
 |-  ( ph -> ( 0 < ( A x. B ) <-> ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) )
36 relt0neg2 
 |-  ( B e. RR -> ( 0 < B <-> ( 0 -R B ) < 0 ) )
37 2 36 syl 
 |-  ( ph -> ( 0 < B <-> ( 0 -R B ) < 0 ) )
38 2 28 remulneg2d 
 |-  ( ph -> ( B x. ( 0 -R 1 ) ) = ( 0 -R ( B x. 1 ) ) )
39 ax-1rid 
 |-  ( B e. RR -> ( B x. 1 ) = B )
40 2 39 syl 
 |-  ( ph -> ( B x. 1 ) = B )
41 40 oveq2d 
 |-  ( ph -> ( 0 -R ( B x. 1 ) ) = ( 0 -R B ) )
42 38 41 eqtrd 
 |-  ( ph -> ( B x. ( 0 -R 1 ) ) = ( 0 -R B ) )
43 42 breq1d 
 |-  ( ph -> ( ( B x. ( 0 -R 1 ) ) < 0 <-> ( 0 -R B ) < 0 ) )
44 37 43 bitr4d 
 |-  ( ph -> ( 0 < B <-> ( B x. ( 0 -R 1 ) ) < 0 ) )
45 24 35 44 3imtr4d 
 |-  ( ph -> ( 0 < ( A x. B ) -> 0 < B ) )
46 9 45 impbid 
 |-  ( ph -> ( 0 < B <-> 0 < ( A x. B ) ) )