Theorem div0i

Description: Division into zero is zero. (Contributed by NM, 12-Aug-1999)

	Ref	Expression
Hypotheses	divclz.1	⊢ 𝐴 ∈ ℂ
	reccl.2	⊢ 𝐴 ≠ 0
Assertion	div0i	⊢ ( 0 / 𝐴 ) = 0

Proof

Step	Hyp	Ref	Expression
1		divclz.1	⊢ 𝐴 ∈ ℂ
2		reccl.2	⊢ 𝐴 ≠ 0
3		div0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 0 / 𝐴 ) = 0 )
4	1 2 3	mp2an	⊢ ( 0 / 𝐴 ) = 0