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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | recmulnq | |
|
3 | 1 2 | mpbii | |