Metamath Proof Explorer


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 ( 𝜑𝐴 ∈ ℂ )
mulne0bad.2 ( 𝜑𝐵 ∈ ℂ )
mulne0bad.3 ( 𝜑 → ( 𝐴 · 𝐵 ) ≠ 0 )
Assertion mulne0bad ( 𝜑𝐴 ≠ 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 simpld ( 𝜑𝐴 ≠ 0 )