Theorem div0

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

	Ref	Expression
Assertion	div0	|- ( ( A e. CC /\ A =/= 0 ) -> ( 0 / A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. CC /\ A =/= 0 ) -> A e. CC )
2	1	mul01d	|- ( ( A e. CC /\ A =/= 0 ) -> ( A x. 0 ) = 0 )
3		0cn	|- 0 e. CC
4		divmul	|- ( ( 0 e. CC /\ 0 e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( 0 / A ) = 0 <-> ( A x. 0 ) = 0 ) )
5	3 3 4	mp3an12	|- ( ( A e. CC /\ A =/= 0 ) -> ( ( 0 / A ) = 0 <-> ( A x. 0 ) = 0 ) )
6	2 5	mpbird	|- ( ( A e. CC /\ A =/= 0 ) -> ( 0 / A ) = 0 )