Metamath Proof Explorer

Theorem recrecnq

Description: Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 29-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion recrecnq 
|- ( A e. Q. -> ( *Q ` ( *Q ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( x = A -> ( *Q ` ( *Q ` x ) ) = ( *Q ` ( *Q ` A ) ) )
2 id 
 |-  ( x = A -> x = A )
3 1 2 eqeq12d 
 |-  ( x = A -> ( ( *Q ` ( *Q ` x ) ) = x <-> ( *Q ` ( *Q ` A ) ) = A ) )
4 mulcomnq 
 |-  ( ( *Q ` x ) .Q x ) = ( x .Q ( *Q ` x ) )
5 recidnq 
 |-  ( x e. Q. -> ( x .Q ( *Q ` x ) ) = 1Q )
6 4 5 syl5eq 
 |-  ( x e. Q. -> ( ( *Q ` x ) .Q x ) = 1Q )
7 recclnq 
 |-  ( x e. Q. -> ( *Q ` x ) e. Q. )
8 recmulnq 
 |-  ( ( *Q ` x ) e. Q. -> ( ( *Q ` ( *Q ` x ) ) = x <-> ( ( *Q ` x ) .Q x ) = 1Q ) )
9 7 8 syl 
 |-  ( x e. Q. -> ( ( *Q ` ( *Q ` x ) ) = x <-> ( ( *Q ` x ) .Q x ) = 1Q ) )
10 6 9 mpbird 
 |-  ( x e. Q. -> ( *Q ` ( *Q ` x ) ) = x )
11 3 10 vtoclga 
 |-  ( A e. Q. -> ( *Q ` ( *Q ` A ) ) = A )