Theorem reccl

Description: Closure law for reciprocal. (Contributed by NM, 30-Apr-2005)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	|- 1 e. CC
2		divcl	|- ( ( 1 e. CC /\ A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
3	1 2	mp3an1	|- ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )