Theorem rereccli

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

	Ref	Expression
Hypotheses	redivcl.1	|- A e. RR
	rereccl.2	|- A =/= 0
Assertion	rereccli	|- ( 1 / A ) e. RR

Proof

Step	Hyp	Ref	Expression
1		redivcl.1	|- A e. RR
2		rereccl.2	|- A =/= 0
3	1	rerecclzi	|- ( A =/= 0 -> ( 1 / A ) e. RR )
4	2 3	ax-mp	|- ( 1 / A ) e. RR