Metamath Proof Explorer

Theorem mulgt0b2d

Description: Biconditional, deductive form of mulgt0 . The first factor is positive iff the product is. (Contributed by SN, 24-Nov-2025)

Ref Expression
Hypotheses mulgt0b2d.a 
|- ( ph -> A e. RR )
mulgt0b2d.b 
|- ( ph -> B e. RR )
mulgt0b2d.1 
|- ( ph -> 0 < B )
Assertion mulgt0b2d 
|- ( ph -> ( 0 < A <-> 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 < B )
4 1 adantr 
 |-  ( ( ph /\ 0 < A ) -> A e. RR )
5 2 adantr 
 |-  ( ( ph /\ 0 < A ) -> B e. RR )
6 simpr 
 |-  ( ( ph /\ 0 < A ) -> 0 < A )
7 3 adantr 
 |-  ( ( ph /\ 0 < A ) -> 0 < B )
8 4 5 6 7 mulgt0d 
 |-  ( ( ph /\ 0 < A ) -> 0 < ( A x. B ) )
9 1 2 remulcld 
 |-  ( ph -> ( A x. B ) e. RR )
10 9 adantr 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. B ) e. RR )
11 2 adantr 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> B e. RR )
12 simpr 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( A x. B ) )
13 12 gt0ne0d 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. B ) =/= 0 )
14 oveq2 
 |-  ( B = 0 -> ( A x. B ) = ( A x. 0 ) )
15 1 adantr 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> A e. RR )
16 remul01 
 |-  ( A e. RR -> ( A x. 0 ) = 0 )
17 15 16 syl 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. 0 ) = 0 )
18 14 17 sylan9eqr 
 |-  ( ( ( ph /\ 0 < ( A x. B ) ) /\ B = 0 ) -> ( A x. B ) = 0 )
19 13 18 mteqand 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> B =/= 0 )
20 11 19 sn-rereccld 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( 1 /R B ) e. RR )
21 2 3 sn-recgt0d 
 |-  ( ph -> 0 < ( 1 /R B ) )
22 21 adantr 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( 1 /R B ) )
23 10 20 12 22 mulgt0d 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < ( ( A x. B ) x. ( 1 /R B ) ) )
24 15 recnd 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> A e. CC )
25 11 recnd 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> B e. CC )
26 20 recnd 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( 1 /R B ) e. CC )
27 24 25 26 mulassd 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( A x. B ) x. ( 1 /R B ) ) = ( A x. ( B x. ( 1 /R B ) ) ) )
28 3 gt0ne0d 
 |-  ( ph -> B =/= 0 )
29 2 28 rerecid 
 |-  ( ph -> ( B x. ( 1 /R B ) ) = 1 )
30 29 oveq2d 
 |-  ( ph -> ( A x. ( B x. ( 1 /R B ) ) ) = ( A x. 1 ) )
31 30 adantr 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. ( B x. ( 1 /R B ) ) ) = ( A x. 1 ) )
32 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
33 15 32 syl 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( A x. 1 ) = A )
34 27 31 33 3eqtrd 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> ( ( A x. B ) x. ( 1 /R B ) ) = A )
35 23 34 breqtrd 
 |-  ( ( ph /\ 0 < ( A x. B ) ) -> 0 < A )
36 8 35 impbida 
 |-  ( ph -> ( 0 < A <-> 0 < ( A x. B ) ) )