Theorem recclzi

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

	Ref	Expression
Hypothesis	divclz.1	|- A e. CC
Assertion	recclzi	|- ( A =/= 0 -> ( 1 / A ) e. CC )

Proof

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