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

Definition df-abs 13069
Description: Define the function for the absolute value (modulus) of a complex number. See abscli 13227 for its closure and absval 13071 or absval2i 13229 for its value. (Contributed by NM, 27-Jul-1999.)
Assertion
Ref Expression
df-abs

Detailed syntax breakdown of Definition df-abs
StepHypRef Expression
1 cabs 13067 . 2
2 vx . . 3
3 cc 9511 . . 3
42cv 1394 . . . . 5
5 ccj 12929 . . . . . 6
64, 5cfv 5593 . . . . 5
7 cmul 9518 . . . . 5
84, 6, 7co 6296 . . . 4
9 csqrt 13066 . . . 4
108, 9cfv 5593 . . 3
112, 3, 10cmpt 4510 . 2
121, 11wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  absval  13071  absf  13170
  Copyright terms: Public domain W3C validator