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𝑸A𝑸*𝑸A=1𝑸

Proof

Step Hyp Ref Expression
1 eqid *𝑸A=*𝑸A
2 recmulnq A𝑸*𝑸A=*𝑸AA𝑸*𝑸A=1𝑸
3 1 2 mpbii A𝑸A𝑸*𝑸A=1𝑸