Theorem rereccli

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

	Ref	Expression
Hypotheses	redivcl.1	$$⊢A\in ℝ$$
	rereccl.2	$$⊢A\ne 0$$
Assertion	rereccli	$$⊢\frac{1}{A}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		redivcl.1	$$⊢A\in ℝ$$
2		rereccl.2	$$⊢A\ne 0$$
3	1	rerecclzi	$$⊢A\ne 0\to \frac{1}{A}\in ℝ$$
4	2 3	ax-mp	$$⊢\frac{1}{A}\in ℝ$$