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 ) ) )