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 0red 
 |-  ( ph -> 0 e. RR )
29 1red 
 |-  ( ph -> 1 e. RR )
30 resubdi 
 |-  ( ( ( A x. B ) e. RR /\ 0 e. RR /\ 1 e. RR ) -> ( ( A x. B ) x. ( 0 -R 1 ) ) = ( ( ( A x. B ) x. 0 ) -R ( ( A x. B ) x. 1 ) ) )
31 25 28 29 30 syl3anc 
 |-  ( ph -> ( ( A x. B ) x. ( 0 -R 1 ) ) = ( ( ( A x. B ) x. 0 ) -R ( ( A x. B ) x. 1 ) ) )
32 remul01 
 |-  ( ( A x. B ) e. RR -> ( ( A x. B ) x. 0 ) = 0 )
33 ax-1rid 
 |-  ( ( A x. B ) e. RR -> ( ( A x. B ) x. 1 ) = ( A x. B ) )
34 32 33 oveq12d 
 |-  ( ( A x. B ) e. RR -> ( ( ( A x. B ) x. 0 ) -R ( ( A x. B ) x. 1 ) ) = ( 0 -R ( A x. B ) ) )
35 25 34 syl 
 |-  ( ph -> ( ( ( A x. B ) x. 0 ) -R ( ( A x. B ) x. 1 ) ) = ( 0 -R ( A x. B ) ) )
36 31 35 eqtrd 
 |-  ( ph -> ( ( A x. B ) x. ( 0 -R 1 ) ) = ( 0 -R ( A x. B ) ) )
37 36 breq1d 
 |-  ( ph -> ( ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 <-> ( 0 -R ( A x. B ) ) < 0 ) )
38 27 37 bitr4d 
 |-  ( ph -> ( 0 < ( A x. B ) <-> ( ( A x. B ) x. ( 0 -R 1 ) ) < 0 ) )
39 relt0neg2 
 |-  ( B e. RR -> ( 0 < B <-> ( 0 -R B ) < 0 ) )
40 2 39 syl 
 |-  ( ph -> ( 0 < B <-> ( 0 -R B ) < 0 ) )
41 resubdi 
 |-  ( ( B e. RR /\ 0 e. RR /\ 1 e. RR ) -> ( B x. ( 0 -R 1 ) ) = ( ( B x. 0 ) -R ( B x. 1 ) ) )
42 2 28 29 41 syl3anc 
 |-  ( ph -> ( B x. ( 0 -R 1 ) ) = ( ( B x. 0 ) -R ( B x. 1 ) ) )
43 remul01 
 |-  ( B e. RR -> ( B x. 0 ) = 0 )
44 ax-1rid 
 |-  ( B e. RR -> ( B x. 1 ) = B )
45 43 44 oveq12d 
 |-  ( B e. RR -> ( ( B x. 0 ) -R ( B x. 1 ) ) = ( 0 -R B ) )
46 2 45 syl 
 |-  ( ph -> ( ( B x. 0 ) -R ( B x. 1 ) ) = ( 0 -R B ) )
47 42 46 eqtrd 
 |-  ( ph -> ( B x. ( 0 -R 1 ) ) = ( 0 -R B ) )
48 47 breq1d 
 |-  ( ph -> ( ( B x. ( 0 -R 1 ) ) < 0 <-> ( 0 -R B ) < 0 ) )
49 40 48 bitr4d 
 |-  ( ph -> ( 0 < B <-> ( B x. ( 0 -R 1 ) ) < 0 ) )
50 24 38 49 3imtr4d 
 |-  ( ph -> ( 0 < ( A x. B ) -> 0 < B ) )
51 9 50 impbid 
 |-  ( ph -> ( 0 < B <-> 0 < ( A x. B ) ) )