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

Metamath Proof Explorer

Theorem diveq0ad

Description: A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses div1d.1 ⊢ φ → A ∈ ℂ
divcld.2 ⊢ φ → B ∈ ℂ
divcld.3 ⊢ φ → B ≠ 0
Assertion diveq0ad ⊢ φ → A B = 0 ↔ A = 0

Proof

Step Hyp Ref Expression
1 div1d.1 ⊢ φ → A ∈ ℂ
2 divcld.2 ⊢ φ → B ∈ ℂ
3 divcld.3 ⊢ φ → B ≠ 0
4 diveq0 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 0 ↔ A = 0
5 1 2 3 4 syl3anc ⊢ φ → A B = 0 ↔ A = 0