Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Reciprocals
mulne0bbd
Metamath Proof Explorer
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 )