Theorem div0i

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

	Ref	Expression
Hypotheses	divclz.1	|- A e. CC
	reccl.2	|- A =/= 0
Assertion	div0i	|- ( 0 / A ) = 0

Proof

Step	Hyp	Ref	Expression
1		divclz.1	|- A e. CC
2		reccl.2	|- A =/= 0
3		div0	|- ( ( A e. CC /\ A =/= 0 ) -> ( 0 / A ) = 0 )
4	1 2 3	mp2an	|- ( 0 / A ) = 0