Theorem divid

Description: A number divided by itself is one. (Contributed by NM, 1-Aug-2004)

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

Proof

Step	Hyp	Ref	Expression
1		divrec	|- ( ( A e. CC /\ A e. CC /\ A =/= 0 ) -> ( A / A ) = ( A x. ( 1 / A ) ) )
2	1	3anidm12	|- ( ( A e. CC /\ A =/= 0 ) -> ( A / A ) = ( A x. ( 1 / A ) ) )
3		recid	|- ( ( A e. CC /\ A =/= 0 ) -> ( A x. ( 1 / A ) ) = 1 )
4	2 3	eqtrd	|- ( ( A e. CC /\ A =/= 0 ) -> ( A / A ) = 1 )