Metamath Proof Explorer

Theorem mullt0b2d

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

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

Proof

Step Hyp Ref Expression
1 mullt0b2d.a 
 |-  ( ph -> A e. RR )
2 mullt0b2d.b 
 |-  ( ph -> B e. RR )
3 mullt0b2d.1 
 |-  ( ph -> B < 0 )
4 simpr 
 |-  ( ( ph /\ 0 < A ) -> 0 < A )
5 4 gt0ne0d 
 |-  ( ( ph /\ 0 < A ) -> A =/= 0 )
6 3 adantr 
 |-  ( ( ph /\ 0 < A ) -> B < 0 )
7 6 lt0ne0d 
 |-  ( ( ph /\ 0 < A ) -> B =/= 0 )
8 5 7 jca 
 |-  ( ( ph /\ 0 < A ) -> ( A =/= 0 /\ B =/= 0 ) )
9 neanior 
 |-  ( ( A =/= 0 /\ B =/= 0 ) <-> -. ( A = 0 \/ B = 0 ) )
10 8 9 sylib 
 |-  ( ( ph /\ 0 < A ) -> -. ( A = 0 \/ B = 0 ) )
11 1 adantr 
 |-  ( ( ph /\ 0 < A ) -> A e. RR )
12 2 adantr 
 |-  ( ( ph /\ 0 < A ) -> B e. RR )
13 11 12 sn-remul0ord 
 |-  ( ( ph /\ 0 < A ) -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )
14 10 13 mtbird 
 |-  ( ( ph /\ 0 < A ) -> -. ( A x. B ) = 0 )
15 0red 
 |-  ( ph -> 0 e. RR )
16 2 15 3 ltnsymd 
 |-  ( ph -> -. 0 < B )
17 16 adantr 
 |-  ( ( ph /\ 0 < A ) -> -. 0 < B )
18 11 12 4 mulgt0b1d 
 |-  ( ( ph /\ 0 < A ) -> ( 0 < B <-> 0 < ( A x. B ) ) )
19 17 18 mtbid 
 |-  ( ( ph /\ 0 < A ) -> -. 0 < ( A x. B ) )
20 ioran 
 |-  ( -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) <-> ( -. ( A x. B ) = 0 /\ -. 0 < ( A x. B ) ) )
21 14 19 20 sylanbrc 
 |-  ( ( ph /\ 0 < A ) -> -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) )
22 1 2 remulcld 
 |-  ( ph -> ( A x. B ) e. RR )
23 22 15 lttrid 
 |-  ( ph -> ( ( A x. B ) < 0 <-> -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) ) )
24 23 adantr 
 |-  ( ( ph /\ 0 < A ) -> ( ( A x. B ) < 0 <-> -. ( ( A x. B ) = 0 \/ 0 < ( A x. B ) ) ) )
25 21 24 mpbird 
 |-  ( ( ph /\ 0 < A ) -> ( A x. B ) < 0 )
26 remul02 
 |-  ( B e. RR -> ( 0 x. B ) = 0 )
27 2 26 syl 
 |-  ( ph -> ( 0 x. B ) = 0 )
28 15 ltnrd 
 |-  ( ph -> -. 0 < 0 )
29 27 28 eqnbrtrd 
 |-  ( ph -> -. ( 0 x. B ) < 0 )
30 oveq1 
 |-  ( 0 = A -> ( 0 x. B ) = ( A x. B ) )
31 30 breq1d 
 |-  ( 0 = A -> ( ( 0 x. B ) < 0 <-> ( A x. B ) < 0 ) )
32 31 notbid 
 |-  ( 0 = A -> ( -. ( 0 x. B ) < 0 <-> -. ( A x. B ) < 0 ) )
33 29 32 syl5ibcom 
 |-  ( ph -> ( 0 = A -> -. ( A x. B ) < 0 ) )
34 33 con2d 
 |-  ( ph -> ( ( A x. B ) < 0 -> -. 0 = A ) )
35 34 imp 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> -. 0 = A )
36 16 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> -. 0 < B )
37 simplr 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( A x. B ) < 0 )
38 1 ad2antrr 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A e. RR )
39 2 ad2antrr 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> B e. RR )
40 simpr 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> A < 0 )
41 38 39 40 mullt0b1d 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> ( 0 < B <-> ( A x. B ) < 0 ) )
42 37 41 mpbird 
 |-  ( ( ( ph /\ ( A x. B ) < 0 ) /\ A < 0 ) -> 0 < B )
43 36 42 mtand 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> -. A < 0 )
44 ioran 
 |-  ( -. ( 0 = A \/ A < 0 ) <-> ( -. 0 = A /\ -. A < 0 ) )
45 35 43 44 sylanbrc 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> -. ( 0 = A \/ A < 0 ) )
46 15 1 lttrid 
 |-  ( ph -> ( 0 < A <-> -. ( 0 = A \/ A < 0 ) ) )
47 46 adantr 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> ( 0 < A <-> -. ( 0 = A \/ A < 0 ) ) )
48 45 47 mpbird 
 |-  ( ( ph /\ ( A x. B ) < 0 ) -> 0 < A )
49 25 48 impbida 
 |-  ( ph -> ( 0 < A <-> ( A x. B ) < 0 ) )