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

Metamath Proof Explorer

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