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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 = 0 ∨ 𝐵 = 0 ) ) )

Proof

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