Metamath Proof Explorer


Definition df-rq

Description: Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-2.5 of Gleason p. 119, who uses an asterisk to denote this unary operation. (Contributed by NM, 6-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion df-rq
|- *Q = ( `' .Q " { 1Q } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crq
 |-  *Q
1 cmq
 |-  .Q
2 1 ccnv
 |-  `' .Q
3 c1q
 |-  1Q
4 3 csn
 |-  { 1Q }
5 2 4 cima
 |-  ( `' .Q " { 1Q } )
6 0 5 wceq
 |-  *Q = ( `' .Q " { 1Q } )