Metamath Proof Explorer


Theorem absi

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

Ref Expression
Assertion absi i = 1

Proof

Step Hyp Ref Expression
1 ax-icn i
2 absval i i = i i
3 1 2 ax-mp 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 i = 1