Metamath Proof Explorer

Theorem mul0or

Description: If a product is zero, one of its factors must be zero. Theorem I.11 of Apostol p. 18. (Contributed by NM, 9-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion mul0or ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = 0 ↔ A = 0 ∨ B = 0

Proof

Step Hyp Ref Expression
1 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
2 1 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
3 2 mul02d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 0 ⋅ B = 0
4 3 eqeq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B = 0 ⋅ B ↔ A ⁢ B = 0
5 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
6 5 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
7 0cnd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → 0 ∈ ℂ
8 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ≠ 0
9 6 7 2 8 mulcan2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B = 0 ⋅ B ↔ A = 0
10 4 9 bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B = 0 ↔ A = 0
11 10 biimpd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ B = 0 → A = 0
12 11 impancom ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A ⁢ B = 0 → B ≠ 0 → A = 0
13 12 necon1bd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A ⁢ B = 0 → ¬ A = 0 → B = 0
14 13 orrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ A ⁢ B = 0 → A = 0 ∨ B = 0
15 14 ex ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = 0 → A = 0 ∨ B = 0
16 1 mul02d ⊢ A ∈ ℂ ∧ B ∈ ℂ → 0 ⋅ B = 0
17 oveq1 ⊢ A = 0 → A ⁢ B = 0 ⋅ B
18 17 eqeq1d ⊢ A = 0 → A ⁢ B = 0 ↔ 0 ⋅ B = 0
19 16 18 syl5ibrcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A = 0 → A ⁢ B = 0
20 5 mul01d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⋅ 0 = 0
21 oveq2 ⊢ B = 0 → A ⁢ B = A ⋅ 0
22 21 eqeq1d ⊢ B = 0 → A ⁢ B = 0 ↔ A ⋅ 0 = 0
23 20 22 syl5ibrcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → B = 0 → A ⁢ B = 0
24 19 23 jaod ⊢ A ∈ ℂ ∧ B ∈ ℂ → A = 0 ∨ B = 0 → A ⁢ B = 0
25 15 24 impbid ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = 0 ↔ A = 0 ∨ B = 0