Theorem rpreccl

Description: Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008)

	Ref	Expression
Assertion	rpreccl	⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		1rp	⊢ 1 ∈ ℝ+
2		rpdivcl	⊢ ( ( 1 ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( 1 / 𝐴 ) ∈ ℝ+ )
3	1 2	mpan	⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ+ )