Metamath Proof Explorer


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. )