Metamath Proof Explorer


Theorem recrecnq

Description: Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996) (Revised by Mario Carneiro, 29-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion recrecnq A𝑸*𝑸*𝑸A=A

Proof

Step Hyp Ref Expression
1 2fveq3 x=A*𝑸*𝑸x=*𝑸*𝑸A
2 id x=Ax=A
3 1 2 eqeq12d x=A*𝑸*𝑸x=x*𝑸*𝑸A=A
4 mulcomnq *𝑸x𝑸x=x𝑸*𝑸x
5 recidnq x𝑸x𝑸*𝑸x=1𝑸
6 4 5 eqtrid x𝑸*𝑸x𝑸x=1𝑸
7 recclnq x𝑸*𝑸x𝑸
8 recmulnq *𝑸x𝑸*𝑸*𝑸x=x*𝑸x𝑸x=1𝑸
9 7 8 syl x𝑸*𝑸*𝑸x=x*𝑸x𝑸x=1𝑸
10 6 9 mpbird x𝑸*𝑸*𝑸x=x
11 3 10 vtoclga A𝑸*𝑸*𝑸A=A