Metamath Proof Explorer


Theorem recclnq

Description: Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion recclnq A𝑸*𝑸A𝑸

Proof

Step Hyp Ref Expression
1 recidnq A𝑸A𝑸*𝑸A=1𝑸
2 1nq 1𝑸𝑸
3 1 2 eqeltrdi A𝑸A𝑸*𝑸A𝑸
4 mulnqf 𝑸:𝑸×𝑸𝑸
5 4 fdmi dom𝑸=𝑸×𝑸
6 0nnq ¬𝑸
7 5 6 ndmovrcl A𝑸*𝑸A𝑸A𝑸*𝑸A𝑸
8 3 7 syl A𝑸A𝑸*𝑸A𝑸
9 8 simprd A𝑸*𝑸A𝑸