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