Theorem div0

Description: Division into zero is zero. (Contributed by NM, 14-Mar-2005)

	Ref	Expression
Assertion	div0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
2	1	mul01d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 0 ) = 0 )
3		0cn	⊢ 0 ∈ ℂ
4		divmul	⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( ( 0 / 𝐴 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) )
5	3 3 4	mp3an12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 0 / 𝐴 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) )
6	2 5	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )