Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfrq  Structured version Unicode version 
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 dfc 9498, and is intended to be used only by the construction. From Proposition 92.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation. (Contributed by NM, 6Mar1996.) (New usage is discouraged.) 
Ref  Expression 

dfrq 
Step  Hyp  Ref  Expression 

1  crq 9235  . 2  
2  cmq 9234  . . . 4  
3  2  ccnv 4998  . . 3 
4  c1q 9231  . . . 4  
5  4  csn 4027  . . 3 
6  3, 5  cima 5002  . 2 
7  1, 6  wceq 1379  1 
Colors of variables: wff setvar class 
This definition is referenced by: recmulnq 9342 dmrecnq 9346 
Copyright terms: Public domain  W3C validator 