Theorem mulne0bad

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	$$⊢\phi \to A\in ℂ$$
	mulne0bad.2	$$⊢\phi \to B\in ℂ$$
	mulne0bad.3	$$⊢\phi \to AB\ne 0$$
Assertion	mulne0bad	$$⊢\phi \to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		mulne0bad.1	$$⊢\phi \to A\in ℂ$$
2		mulne0bad.2	$$⊢\phi \to B\in ℂ$$
3		mulne0bad.3	$$⊢\phi \to AB\ne 0$$
4	1 2	mulne0bd	$$⊢\phi \to \left(\left(A\ne 0\wedge B\ne 0\right)\leftrightarrow AB\ne 0\right)$$
5	3 4	mpbird	$$⊢\phi \to \left(A\ne 0\wedge B\ne 0\right)$$
6	5	simpld	$$⊢\phi \to A\ne 0$$