Theorem dividi

Description: A number divided by itself is one. (Contributed by NM, 9-Feb-1995)

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

Proof

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