Theorem div0

Description: Division into zero is zero. (Contributed by NM, 14-Mar-2005) (Proof shortened by SN, 9-Jul-2025)

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

Proof

Step	Hyp	Ref	Expression
1		0cn	⊢ 0 ∈ ℂ
2		eqid	⊢ 0 = 0
3		diveq0	⊢ ( ( 0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( 0 / 𝐴 ) = 0 ↔ 0 = 0 ) )
4	2 3	mpbiri	⊢ ( ( 0 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )
5	1 4	mp3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )