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 ∈ ℂ
2		absval	⊢ ( i ∈ ℂ → ( abs ‘ i ) = ( √ ‘ ( i · ( ∗ ‘ i ) ) ) )
3	1 2	ax-mp	⊢ ( abs ‘ i ) = ( √ ‘ ( i · ( ∗ ‘ i ) ) )
4		cji	⊢ ( ∗ ‘ i ) = - i
5	4	oveq2i	⊢ ( i · ( ∗ ‘ 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 · ( ∗ ‘ i ) ) = 1
12	11	fveq2i	⊢ ( √ ‘ ( i · ( ∗ ‘ i ) ) ) = ( √ ‘ 1 )
13		sqrt1	⊢ ( √ ‘ 1 ) = 1
14	3 12 13	3eqtri	⊢ ( abs ‘ i ) = 1