absi

Description: The absolute value of the imaginary unit. (Contributed by NM, 26-Mar-2005)

		Ref	Expression
	Assertion	absi	$⊢ \|i\| = 1$

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		absval	$⊢ i \in ℂ \to \|i\| = \sqrt{i \overline{i}}$
3	1 2	ax-mp	$⊢ \|i\| = \sqrt{i \overline{i}}$
4		cji	$⊢ \overline{i} = - i$
5	4	oveq2i	$⊢ i \overline{i} = i (- i)$
6	1 1	mulneg2i	$⊢ i (- i) = - i i$
7		ixi	$⊢ i i = - 1$
8	7	negeqi	$⊢ - i i = - -1$
9		negneg1e1	$⊢ - -1 = 1$
10	8 9	eqtri	$⊢ - i i = 1$
11	5 6 10	3eqtri	$⊢ i \overline{i} = 1$
12	11	fveq2i	$⊢ \sqrt{i \overline{i}} = \sqrt{1}$
13		sqrt1	$⊢ \sqrt{1} = 1$
14	3 12 13	3eqtri	$⊢ \|i\| = 1$

Metamath Proof Explorer