Metamath Proof Explorer


Theorem imi

Description: The imaginary part of _i . (Contributed by Scott Fenton, 9-Jun-2006)

Ref Expression
Assertion imi ( ℑ ‘ i ) = 1

Proof

Step Hyp Ref Expression
1 ax-icn i ∈ ℂ
2 ax-1cn 1 ∈ ℂ
3 1 2 mulcli ( i · 1 ) ∈ ℂ
4 3 addid2i ( 0 + ( i · 1 ) ) = ( i · 1 )
5 4 eqcomi ( i · 1 ) = ( 0 + ( i · 1 ) )
6 5 fveq2i ( ℑ ‘ ( i · 1 ) ) = ( ℑ ‘ ( 0 + ( i · 1 ) ) )
7 1 mulid1i ( i · 1 ) = i
8 7 fveq2i ( ℑ ‘ ( i · 1 ) ) = ( ℑ ‘ i )
9 0re 0 ∈ ℝ
10 1re 1 ∈ ℝ
11 crim ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ℑ ‘ ( 0 + ( i · 1 ) ) ) = 1 )
12 9 10 11 mp2an ( ℑ ‘ ( 0 + ( i · 1 ) ) ) = 1
13 6 8 12 3eqtr3i ( ℑ ‘ i ) = 1