Theorem mulltgt0d

Description: Negative times positive is negative. (Contributed by SN, 26-Nov-2025)

	Ref	Expression
Hypotheses	mullt0b1d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	mullt0b1d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	mullt0b1d.1	⊢ ( 𝜑 → 𝐴 < 0 )
	mulltgt0d.2	⊢ ( 𝜑 → 0 < 𝐵 )
Assertion	mulltgt0d	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		mullt0b1d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		mullt0b1d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		mullt0b1d.1	⊢ ( 𝜑 → 𝐴 < 0 )
4		mulltgt0d.2	⊢ ( 𝜑 → 0 < 𝐵 )
5	3	lt0ne0d	⊢ ( 𝜑 → 𝐴 ≠ 0 )
6	4	gt0ne0d	⊢ ( 𝜑 → 𝐵 ≠ 0 )
7	5 6	jca	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) )
8		neanior	⊢ ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ↔ ¬ ( 𝐴 = 0 ∨ 𝐵 = 0 ) )
9	7 8	sylib	⊢ ( 𝜑 → ¬ ( 𝐴 = 0 ∨ 𝐵 = 0 ) )
10	1 2	sn-remul0ord	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) )
11	9 10	mtbird	⊢ ( 𝜑 → ¬ ( 𝐴 · 𝐵 ) = 0 )
12		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
13	1 12 3	ltnsymd	⊢ ( 𝜑 → ¬ 0 < 𝐴 )
14	1 2 4	mulgt0b2d	⊢ ( 𝜑 → ( 0 < 𝐴 ↔ 0 < ( 𝐴 · 𝐵 ) ) )
15	13 14	mtbid	⊢ ( 𝜑 → ¬ 0 < ( 𝐴 · 𝐵 ) )
16		ioran	⊢ ( ¬ ( ( 𝐴 · 𝐵 ) = 0 ∨ 0 < ( 𝐴 · 𝐵 ) ) ↔ ( ¬ ( 𝐴 · 𝐵 ) = 0 ∧ ¬ 0 < ( 𝐴 · 𝐵 ) ) )
17	11 15 16	sylanbrc	⊢ ( 𝜑 → ¬ ( ( 𝐴 · 𝐵 ) = 0 ∨ 0 < ( 𝐴 · 𝐵 ) ) )
18	1 2	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
19	18 12	lttrid	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) < 0 ↔ ¬ ( ( 𝐴 · 𝐵 ) = 0 ∨ 0 < ( 𝐴 · 𝐵 ) ) ) )
20	17 19	mpbird	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) < 0 )