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