This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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