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