Theorem absi

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

	Ref	Expression
Assertion	absi	|- ( abs ` _i ) = 1

Proof

Step	Hyp	Ref	Expression
1		ax-icn	|- _i e. CC
2		absval	|- ( _i e. CC -> ( abs ` _i ) = ( sqrt ` ( _i x. ( * ` _i ) ) ) )
3	1 2	ax-mp	|- ( abs ` _i ) = ( sqrt ` ( _i x. ( * ` _i ) ) )
4		cji	|- ( * ` _i ) = -u _i
5	4	oveq2i	|- ( _i x. ( * ` _i ) ) = ( _i x. -u _i )
6	1 1	mulneg2i	|- ( _i x. -u _i ) = -u ( _i x. _i )
7		ixi	|- ( _i x. _i ) = -u 1
8	7	negeqi	|- -u ( _i x. _i ) = -u -u 1
9		negneg1e1	|- -u -u 1 = 1
10	8 9	eqtri	|- -u ( _i x. _i ) = 1
11	5 6 10	3eqtri	|- ( _i x. ( * ` _i ) ) = 1
12	11	fveq2i	|- ( sqrt ` ( _i x. ( * ` _i ) ) ) = ( sqrt ` 1 )
13		sqrt1	|- ( sqrt ` 1 ) = 1
14	3 12 13	3eqtri	|- ( abs ` _i ) = 1