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

Metamath Proof Explorer

Theorem mulne0bbd

Description: A factor of a nonzero complex number is nonzero. Partial converse of mulne0d and consequence of mulne0bd . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	mulne0bad.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	mulne0bad.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	mulne0bad.3	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ≠ 0 )
Assertion	mulne0bbd	⊢ ( 𝜑 → 𝐵 ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		mulne0bad.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		mulne0bad.2	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		mulne0bad.3	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ≠ 0 )
4	1 2	mulne0bd	⊢ ( 𝜑 → ( ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) ↔ ( 𝐴 · 𝐵 ) ≠ 0 ) )
5	3 4	mpbird	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ∧ 𝐵 ≠ 0 ) )
6	5	simprd	⊢ ( 𝜑 → 𝐵 ≠ 0 )