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
|- ( ph -> A e. CC )
mulne0bad.2
|- ( ph -> B e. CC )
mulne0bad.3
|- ( ph -> ( A x. B ) =/= 0 )
Assertion mulne0bbd
|- ( ph -> B =/= 0 )

Proof

Step Hyp Ref Expression
1 mulne0bad.1
 |-  ( ph -> A e. CC )
2 mulne0bad.2
 |-  ( ph -> B e. CC )
3 mulne0bad.3
 |-  ( ph -> ( A x. B ) =/= 0 )
4 1 2 mulne0bd
 |-  ( ph -> ( ( A =/= 0 /\ B =/= 0 ) <-> ( A x. B ) =/= 0 ) )
5 3 4 mpbird
 |-  ( ph -> ( A =/= 0 /\ B =/= 0 ) )
6 5 simprd
 |-  ( ph -> B =/= 0 )