Theorem sn-remul0ord

Description: A product is zero iff one of its factors are zero. (Contributed by SN, 24-Nov-2025)

	Ref	Expression
Hypotheses	sn-remul0ord.a	$$⊢\phi \to A\in ℝ$$
	sn-remul0ord.b	$$⊢\phi \to B\in ℝ$$
Assertion	sn-remul0ord	$$⊢\phi \to \left(AB=0\leftrightarrow \left(A=0\vee B=0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sn-remul0ord.a	$$⊢\phi \to A\in ℝ$$
2		sn-remul0ord.b	$$⊢\phi \to B\in ℝ$$
3		remul02	$$⊢B\in ℝ\to 0\cdot B=0$$
4	2 3	syl	$$⊢\phi \to 0\cdot B=0$$
5	4	adantr	$$⊢\left(\phi \wedge B\ne 0\right)\to 0\cdot B=0$$
6	5	eqeq2d	$$⊢\left(\phi \wedge B\ne 0\right)\to \left(AB=0\cdot B\leftrightarrow AB=0\right)$$
7	1	adantr	$$⊢\left(\phi \wedge B\ne 0\right)\to A\in ℝ$$
8		0red	$$⊢\left(\phi \wedge B\ne 0\right)\to 0\in ℝ$$
9	2	adantr	$$⊢\left(\phi \wedge B\ne 0\right)\to B\in ℝ$$
10		simpr	$$⊢\left(\phi \wedge B\ne 0\right)\to B\ne 0$$
11	7 8 9 10	remulcan2d	$$⊢\left(\phi \wedge B\ne 0\right)\to \left(AB=0\cdot B\leftrightarrow A=0\right)$$
12	6 11	bitr3d	$$⊢\left(\phi \wedge B\ne 0\right)\to \left(AB=0\leftrightarrow A=0\right)$$
13	12	biimpd	$$⊢\left(\phi \wedge B\ne 0\right)\to \left(AB=0\to A=0\right)$$
14	13	impancom	$$⊢\left(\phi \wedge AB=0\right)\to \left(B\ne 0\to A=0\right)$$
15	14	necon1bd	$$⊢\left(\phi \wedge AB=0\right)\to \left(\neg A=0\to B=0\right)$$
16	15	orrd	$$⊢\left(\phi \wedge AB=0\right)\to \left(A=0\vee B=0\right)$$
17	16	ex	$$⊢\phi \to \left(AB=0\to \left(A=0\vee B=0\right)\right)$$
18		oveq1	$$⊢A=0\to AB=0\cdot B$$
19	18	eqeq1d	$$⊢A=0\to \left(AB=0\leftrightarrow 0\cdot B=0\right)$$
20	4 19	syl5ibrcom	$$⊢\phi \to \left(A=0\to AB=0\right)$$
21		remul01	$$⊢A\in ℝ\to A\cdot 0=0$$
22	1 21	syl	$$⊢\phi \to A\cdot 0=0$$
23		oveq2	$$⊢B=0\to AB=A\cdot 0$$
24	23	eqeq1d	$$⊢B=0\to \left(AB=0\leftrightarrow A\cdot 0=0\right)$$
25	22 24	syl5ibrcom	$$⊢\phi \to \left(B=0\to AB=0\right)$$
26	20 25	jaod	$$⊢\phi \to \left(\left(A=0\vee B=0\right)\to AB=0\right)$$
27	17 26	impbid	$$⊢\phi \to \left(AB=0\leftrightarrow \left(A=0\vee B=0\right)\right)$$