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 e. Q. -> ( *Q ` A ) e. Q. )

Proof

Step	Hyp	Ref	Expression
1		recidnq	|- ( A e. Q. -> ( A .Q ( *Q ` A ) ) = 1Q )
2		1nq	|- 1Q e. Q.
3	1 2	eqeltrdi	|- ( A e. Q. -> ( A .Q ( *Q ` A ) ) e. Q. )
4		mulnqf	|- .Q : ( Q. X. Q. ) --> Q.
5	4	fdmi	|- dom .Q = ( Q. X. Q. )
6		0nnq	|- -. (/) e. Q.
7	5 6	ndmovrcl	|- ( ( A .Q ( *Q ` A ) ) e. Q. -> ( A e. Q. /\ ( *Q ` A ) e. Q. ) )
8	3 7	syl	|- ( A e. Q. -> ( A e. Q. /\ ( *Q ` A ) e. Q. ) )
9	8	simprd	|- ( A e. Q. -> ( *Q ` A ) e. Q. )