This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-abs

Description: Define the function for the absolute value (modulus) of a complex number. See abscli for its closure and absval or absval2i for its value. For example, ( abs-u 2 ) = 2 ( ex-abs ). (Contributed by NM, 27-Jul-1999)

		Ref	Expression
	Assertion	df-abs	$⊢ abs = (x \in ℂ ⟼ \sqrt{x \overline{x}})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cabs	$class abs$
1		vx	$setvar x$
2		cc	$class ℂ$
3		csqrt	$class \sqrt$
4	1	cv	$setvar x$
5		cmul	$class \times$
6		ccj	$class *$
7	4 6	cfv	$class \overline{x}$
8	4 7 5	co	$class x \overline{x}$
9	8 3	cfv	$class \sqrt{x \overline{x}}$
10	1 2 9	cmpt	$class (x \in ℂ ⟼ \sqrt{x \overline{x}})$
11	0 10	wceq	$wff abs = (x \in ℂ ⟼ \sqrt{x \overline{x}})$