Metamath Proof Explorer

Theorem diveq0

Description: A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion diveq0 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 0 ↔ A = 0

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 divmul2 ⊢ A ∈ ℂ ∧ 0 ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 0 ↔ A = B ⋅ 0
3 1 2 mp3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 0 ↔ A = B ⋅ 0
4 3 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 0 ↔ A = B ⋅ 0
5 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
6 5 mul01d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⋅ 0 = 0
7 6 eqeq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A = B ⋅ 0 ↔ A = 0
8 4 7 bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = 0 ↔ A = 0