Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfmq  Unicode version 
Description: Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers dfc 8952, and is intended to be used only by the construction. From Proposition 92.4 of [Gleason] p. 119. (Contributed by NM, 24Aug1995.) (New usage is discouraged.) 
Ref  Expression 

dfmq 
Step  Hyp  Ref  Expression 

1  cmq 8687  . 2  
2  cerq 8685  . . . 4  
3  cmpq 8680  . . . 4  
4  2, 3  ccom 4841  . . 3 
5  cnq 8683  . . . 4  
6  5, 5  cxp 4835  . . 3 
7  4, 6  cres 4839  . 2 
8  1, 7  wceq 1649  1 
Colors of variables: wff set class 
This definition is referenced by: mulpqnq 8774 mulnqf 8782 
Copyright terms: Public domain  W3C validator 