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