Theorem recclnq

Description: Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	recclnq	$$⊢A\in 𝑸\to {*}_{𝑸}\left(A\right)\in 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		recidnq	$$⊢A\in 𝑸\to A{\cdot }_{𝑸}{*}_{𝑸}\left(A\right)=1_{𝑸}$$
2		1nq	$$⊢1_{𝑸}\in 𝑸$$
3	1 2	eqeltrdi	$$⊢A\in 𝑸\to A{\cdot }_{𝑸}{*}_{𝑸}\left(A\right)\in 𝑸$$
4		mulnqf	$$⊢{\cdot }_{𝑸}:𝑸\times 𝑸⟶𝑸$$
5	4	fdmi	$$⊢\mathrm{dom}{\cdot }_{𝑸}=𝑸\times 𝑸$$
6		0nnq	$$⊢\neg \varnothing \in 𝑸$$
7	5 6	ndmovrcl	$$⊢A{\cdot }_{𝑸}{*}_{𝑸}\left(A\right)\in 𝑸\to \left(A\in 𝑸\wedge {*}_{𝑸}\left(A\right)\in 𝑸\right)$$
8	3 7	syl	$$⊢A\in 𝑸\to \left(A\in 𝑸\wedge {*}_{𝑸}\left(A\right)\in 𝑸\right)$$
9	8	simprd	$$⊢A\in 𝑸\to {*}_{𝑸}\left(A\right)\in 𝑸$$