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	⊢ ( 𝐴 ∈ Q → ( *Q ‘ 𝐴 ) ∈ Q )

Proof

Step	Hyp	Ref	Expression
1		recidnq	⊢ ( 𝐴 ∈ Q → ( 𝐴 ·Q ( *Q ‘ 𝐴 ) ) = 1Q )
2		1nq	⊢ 1Q ∈ Q
3	1 2	eqeltrdi	⊢ ( 𝐴 ∈ Q → ( 𝐴 ·Q ( *Q ‘ 𝐴 ) ) ∈ Q )
4		mulnqf	⊢ ·Q : ( Q × Q ) ⟶ Q
5	4	fdmi	⊢ dom ·Q = ( Q × Q )
6		0nnq	⊢ ¬ ∅ ∈ Q
7	5 6	ndmovrcl	⊢ ( ( 𝐴 ·Q ( *Q ‘ 𝐴 ) ) ∈ Q → ( 𝐴 ∈ Q ∧ ( *Q ‘ 𝐴 ) ∈ Q ) )
8	3 7	syl	⊢ ( 𝐴 ∈ Q → ( 𝐴 ∈ Q ∧ ( *Q ‘ 𝐴 ) ∈ Q ) )
9	8	simprd	⊢ ( 𝐴 ∈ Q → ( *Q ‘ 𝐴 ) ∈ Q )