MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-abs Structured version   Unicode version

Definition df-abs 12072
Description: Define the function for the absolute value (modulus) of a complex number. See abscli 12229 for its closure and absval 12074 or absval2i 12231 for its value. (Contributed by NM, 27-Jul-1999.)
Assertion
Ref Expression
df-abs  |-  abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  ( * `  x ) ) ) )

Detailed syntax breakdown of Definition df-abs
StepHypRef Expression
1 cabs 12070 . 2  class  abs
2 vx . . 3  set  x
3 cc 9019 . . 3  class  CC
42cv 1652 . . . . 5  class  x
5 ccj 11932 . . . . . 6  class  *
64, 5cfv 5483 . . . . 5  class  ( * `
 x )
7 cmul 9026 . . . . 5  class  x.
84, 6, 7co 6110 . . . 4  class  ( x  x.  ( * `  x ) )
9 csqr 12069 . . . 4  class  sqr
108, 9cfv 5483 . . 3  class  ( sqr `  ( x  x.  (
* `  x )
) )
112, 3, 10cmpt 4291 . 2  class  ( x  e.  CC  |->  ( sqr `  ( x  x.  (
* `  x )
) ) )
121, 11wceq 1653 1  wff  abs  =  ( x  e.  CC  |->  ( sqr `  ( x  x.  ( * `  x ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  absval  12074  absf  12172
  Copyright terms: Public domain W3C validator