Metamath Proof Explorer

Theorem mullt0b1d

Description: When the first term is negative, the second term is positive iff the product is negative. (Contributed by SN, 26-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 mullt0b1d.a 
 |-  ( ph -> A e. RR )
2 mullt0b1d.b 
 |-  ( ph -> B e. RR )
3 mullt0b1d.1 
 |-  ( ph -> A < 0 )
4 1 adantr 
 |-  ( ( ph /\ 0 < B ) -> A e. RR )
5 2 adantr 
 |-  ( ( ph /\ 0 < B ) -> B e. RR )
6 3 adantr 
 |-  ( ( ph /\ 0 < B ) -> A < 0 )
7 simpr 
 |-  ( ( ph /\ 0 < B ) -> 0 < B )
8 4 5 6 7 mulltgt0d 
 |-  ( ( ph /\ 0 < B ) -> ( A x. B ) < 0 )
9 3 lt0ne0d 
 |-  ( ph -> A =/= 0 )
10 1 9 sn-rereccld 
 |-  ( ph -> ( 1 /R A ) e. RR )
11 1 2 remulcld 
 |-  ( ph -> ( A x. B ) e. RR )
12 10 11 remulneg2d 
 |-  ( ph -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R ( ( 1 /R A ) x. ( A x. B ) ) ) )
13 1 9 rerecid2 
 |-  ( ph -> ( ( 1 /R A ) x. A ) = 1 )
14 13 oveq1d 
 |-  ( ph -> ( ( ( 1 /R A ) x. A ) x. B ) = ( 1 x. B ) )
15 10 recnd 
 |-  ( ph -> ( 1 /R A ) e. CC )
16 1 recnd 
 |-  ( ph -> A e. CC )
17 2 recnd 
 |-  ( ph -> B e. CC )
18 15 16 17 mulassd 
 |-  ( ph -> ( ( ( 1 /R A ) x. A ) x. B ) = ( ( 1 /R A ) x. ( A x. B ) ) )
19 remullid 
 |-  ( B e. RR -> ( 1 x. B ) = B )
20 2 19 syl 
 |-  ( ph -> ( 1 x. B ) = B )
21 14 18 20 3eqtr3d 
 |-  ( ph -> ( ( 1 /R A ) x. ( A x. B ) ) = B )
22 21 oveq2d 
 |-  ( ph -> ( 0 -R ( ( 1 /R A ) x. ( A x. B ) ) ) = ( 0 -R B ) )
23 12 22 eqtrd 
 |-  ( ph -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R B ) )
24 23 adantr 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) = ( 0 -R B ) )
25 10 adantr 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 1 /R A ) e. RR )
26 rernegcl 
 |-  ( ( A x. B ) e. RR -> ( 0 -R ( A x. B ) ) e. RR )
27 11 26 syl 
 |-  ( ph -> ( 0 -R ( A x. B ) ) e. RR )
28 27 adantr 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 0 -R ( A x. B ) ) e. RR )
29 1 3 sn-reclt0d 
 |-  ( ph -> ( 1 /R A ) < 0 )
30 29 adantr 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 1 /R A ) < 0 )
31 simpr 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> 0 < ( 0 -R ( A x. B ) ) )
32 25 28 30 31 mulltgt0d 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( ( 1 /R A ) x. ( 0 -R ( A x. B ) ) ) < 0 )
33 24 32 eqbrtrrd 
 |-  ( ( ph /\ 0 < ( 0 -R ( A x. B ) ) ) -> ( 0 -R B ) < 0 )
34 33 ex 
 |-  ( ph -> ( 0 < ( 0 -R ( A x. B ) ) -> ( 0 -R B ) < 0 ) )
35 relt0neg1 
 |-  ( ( A x. B ) e. RR -> ( ( A x. B ) < 0 <-> 0 < ( 0 -R ( A x. B ) ) ) )
36 11 35 syl 
 |-  ( ph -> ( ( A x. B ) < 0 <-> 0 < ( 0 -R ( A x. B ) ) ) )
37 relt0neg2 
 |-  ( B e. RR -> ( 0 < B <-> ( 0 -R B ) < 0 ) )
38 2 37 syl 
 |-  ( ph -> ( 0 < B <-> ( 0 -R B ) < 0 ) )
39 34 36 38 3imtr4d 
 |-  ( ph -> ( ( A x. B ) < 0 -> 0 < B ) )
40 39 imp 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> 0 < B )
41 8 40 impbida 
 |-  ( ph -> ( 0 < B <-> ( A x. B ) < 0 ) )