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

Definition df-abs 15187
Description: Define the function for the absolute value (modulus) of a complex number. See abscli 15346 for its closure and absval 15189 or absval2i 15348 for its value. For example, (absโ€˜-2) = 2 (ex-abs 30213). (Contributed by NM, 27-Jul-1999.)
Assertion
Ref Expression
df-abs abs = (๐‘ฅ โˆˆ โ„‚ โ†ฆ (โˆšโ€˜(๐‘ฅ ยท (โˆ—โ€˜๐‘ฅ))))

Detailed syntax breakdown of Definition df-abs
StepHypRef Expression
1 cabs 15185 . 2 class abs
2 vx . . 3 setvar ๐‘ฅ
3 cc 11107 . . 3 class โ„‚
42cv 1532 . . . . 5 class ๐‘ฅ
5 ccj 15047 . . . . . 6 class โˆ—
64, 5cfv 6536 . . . . 5 class (โˆ—โ€˜๐‘ฅ)
7 cmul 11114 . . . . 5 class ยท
84, 6, 7co 7404 . . . 4 class (๐‘ฅ ยท (โˆ—โ€˜๐‘ฅ))
9 csqrt 15184 . . . 4 class โˆš
108, 9cfv 6536 . . 3 class (โˆšโ€˜(๐‘ฅ ยท (โˆ—โ€˜๐‘ฅ)))
112, 3, 10cmpt 5224 . 2 class (๐‘ฅ โˆˆ โ„‚ โ†ฆ (โˆšโ€˜(๐‘ฅ ยท (โˆ—โ€˜๐‘ฅ))))
121, 11wceq 1533 1 wff abs = (๐‘ฅ โˆˆ โ„‚ โ†ฆ (โˆšโ€˜(๐‘ฅ ยท (โˆ—โ€˜๐‘ฅ))))
Colors of variables: wff setvar class
This definition is referenced by:  absval  15189  absf  15288  absfico  44470
  Copyright terms: Public domain W3C validator