Definition df-rq 10917

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 11121, 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.)

Assertion

Ref	Expression
df-rq	⊢ *Q = (◡ ·Q “ {1Q})

Detailed syntax breakdown of Definition df-rq

Step	Hyp	Ref	Expression
1		crq 10857	. 2 class *Q
2		cmq 10856	. . . 4 class ·Q
3	2	ccnv 5662	. . 3 class ◡ ·Q
4		c1q 10853	. . . 4 class 1Q
5	4	csn 4591	. . 3 class {1Q}
6	3, 5	cima 5666	. 2 class (◡ ·Q “ {1Q})
7	1, 6	wceq 1570	1 wff *Q = (◡ ·Q “ {1Q})

This definition is used by:  recmulnq  10964  dmrecnq  10968