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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
mullt0b1d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
mullt0b1d.1 ⊢ ( 𝜑 → 𝐴 < 0 )
Assertion mullt0b1d ( 𝜑 → ( 0 < 𝐵 ↔ ( 𝐴 · 𝐵 ) < 0 ) )

Proof

Step Hyp Ref Expression
1 mullt0b1d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 mullt0b1d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 mullt0b1d.1 ⊢ ( 𝜑 → 𝐴 < 0 )
4 1 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐴 ∈ ℝ )
5 2 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐵 ∈ ℝ )
6 3 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐴 < 0 )
7 simpr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 0 < 𝐵 )
8 4 5 6 7 mulltgt0d ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → ( 𝐴 · 𝐵 ) < 0 )
9 3 lt0ne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
10 1 9 sn-rereccld ⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) ∈ ℝ )
11 1 2 remulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
12 10 11 remulneg2d ⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) = ( 0 −ℝ ( ( 1 /ℝ 𝐴 ) · ( 𝐴 · 𝐵 ) ) ) )
13 1 9 rerecid2 ⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · 𝐴 ) = 1 )
14 13 oveq1d ⊢ ( 𝜑 → ( ( ( 1 /ℝ 𝐴 ) · 𝐴 ) · 𝐵 ) = ( 1 · 𝐵 ) )
15 10 recnd ⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) ∈ ℂ )
16 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
17 2 recnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
18 15 16 17 mulassd ⊢ ( 𝜑 → ( ( ( 1 /ℝ 𝐴 ) · 𝐴 ) · 𝐵 ) = ( ( 1 /ℝ 𝐴 ) · ( 𝐴 · 𝐵 ) ) )
19 remullid ⊢ ( 𝐵 ∈ ℝ → ( 1 · 𝐵 ) = 𝐵 )
20 2 19 syl ⊢ ( 𝜑 → ( 1 · 𝐵 ) = 𝐵 )
21 14 18 20 3eqtr3d ⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · ( 𝐴 · 𝐵 ) ) = 𝐵 )
22 21 oveq2d ⊢ ( 𝜑 → ( 0 −ℝ ( ( 1 /ℝ 𝐴 ) · ( 𝐴 · 𝐵 ) ) ) = ( 0 −ℝ 𝐵 ) )
23 12 22 eqtrd ⊢ ( 𝜑 → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) = ( 0 −ℝ 𝐵 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) = ( 0 −ℝ 𝐵 ) )
25 10 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → ( 1 /ℝ 𝐴 ) ∈ ℝ )
26 rernegcl ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
27 11 26 syl ⊢ ( 𝜑 → ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ∈ ℝ )
29 1 3 sn-reclt0d ⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) < 0 )
30 29 adantr ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → ( 1 /ℝ 𝐴 ) < 0 )
31 simpr ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) )
32 25 28 30 31 mulltgt0d ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → ( ( 1 /ℝ 𝐴 ) · ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) < 0 )
33 24 32 eqbrtrrd ⊢ ( ( 𝜑 ∧ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) → ( 0 −ℝ 𝐵 ) < 0 )
34 33 ex ⊢ ( 𝜑 → ( 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) → ( 0 −ℝ 𝐵 ) < 0 ) )
35 relt0neg1 ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℝ → ( ( 𝐴 · 𝐵 ) < 0 ↔ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) )
36 11 35 syl ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ 0 < ( 0 −ℝ ( 𝐴 · 𝐵 ) ) ) )
37 relt0neg2 ⊢ ( 𝐵 ∈ ℝ → ( 0 < 𝐵 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
38 2 37 syl ⊢ ( 𝜑 → ( 0 < 𝐵 ↔ ( 0 −ℝ 𝐵 ) < 0 ) )
39 34 36 38 3imtr4d ⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 → 0 < 𝐵 ) )
40 39 imp ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐵 ) < 0 ) → 0 < 𝐵 )
41 8 40 impbida ⊢ ( 𝜑 → ( 0 < 𝐵 ↔ ( 𝐴 · 𝐵 ) < 0 ) )