Theorem drngmulne0

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

	Ref	Expression
Hypotheses	drngmuleq0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngmuleq0.o	⊢ 0 = ( 0g ‘ 𝑅 )
	drngmuleq0.t	⊢ · = ( .r ‘ 𝑅 )
	drngmuleq0.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
	drngmuleq0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	drngmuleq0.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	drngmulne0	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		drngmuleq0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngmuleq0.o	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngmuleq0.t	⊢ · = ( .r ‘ 𝑅 )
4		drngmuleq0.r	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
5		drngmuleq0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		drngmuleq0.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7	1 2 3 4 5 6	drngmul0or	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) = 0 ↔ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
8	7	necon3abid	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) ) )
9		neanior	⊢ ( ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ↔ ¬ ( 𝑋 = 0 ∨ 𝑌 = 0 ) )
10	8 9	bitr4di	⊢ ( 𝜑 → ( ( 𝑋 · 𝑌 ) ≠ 0 ↔ ( 𝑋 ≠ 0 ∧ 𝑌 ≠ 0 ) ) )