drngmulne0

Description: A product is nonzero iff both its factors are nonzero. (Contributed by NM, 18-Oct-2014)

	Ref	Expression
Hypotheses	drngmuleq0.b	$⊢ B = {Base}_{R}$
	drngmuleq0.o	$⊢ \underset{˙}{0} = 0_{R}$
	drngmuleq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	drngmuleq0.r	$⊢ φ \to R \in DivRing$
	drngmuleq0.x	$⊢ φ \to X \in B$
	drngmuleq0.y	$⊢ φ \to Y \in B$
Assertion	drngmulne0	$⊢ φ \to (X \underset{˙}{\cdot} Y \neq \underset{˙}{0} \leftrightarrow (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		drngmuleq0.b	$⊢ B = {Base}_{R}$
2		drngmuleq0.o	$⊢ \underset{˙}{0} = 0_{R}$
3		drngmuleq0.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		drngmuleq0.r	$⊢ φ \to R \in DivRing$
5		drngmuleq0.x	$⊢ φ \to X \in B$
6		drngmuleq0.y	$⊢ φ \to Y \in B$
7	1 2 3 4 5 6	drngmul0or	$⊢ φ \to (X \underset{˙}{\cdot} Y = \underset{˙}{0} \leftrightarrow (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
8	7	necon3abid	$⊢ φ \to (X \underset{˙}{\cdot} Y \neq \underset{˙}{0} \leftrightarrow \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0}))$
9		neanior	$⊢ (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}) \leftrightarrow \neg (X = \underset{˙}{0} \lor Y = \underset{˙}{0})$
10	8 9	bitr4di	$⊢ φ \to (X \underset{˙}{\cdot} Y \neq \underset{˙}{0} \leftrightarrow (X \neq \underset{˙}{0} \land Y \neq \underset{˙}{0}))$

Metamath Proof Explorer