This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 } ) |
| 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 } ) |