Metamath Proof Explorer


Theorem recidnq

Description: A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( *Q ` A ) = ( *Q ` A )
2 recmulnq
 |-  ( A e. Q. -> ( ( *Q ` A ) = ( *Q ` A ) <-> ( A .Q ( *Q ` A ) ) = 1Q ) )
3 1 2 mpbii
 |-  ( A e. Q. -> ( A .Q ( *Q ` A ) ) = 1Q )