Theorem rei

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

	Ref	Expression
Assertion	rei	⊢ ( ℜ ‘ i ) = 0

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	fveq2i	⊢ ( ℜ ‘ ( 0 + ( i · 1 ) ) ) = ( ℜ ‘ ( i · 1 ) )
6		0re	⊢ 0 ∈ ℝ
7		1re	⊢ 1 ∈ ℝ
8		crre	⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ) → ( ℜ ‘ ( 0 + ( i · 1 ) ) ) = 0 )
9	6 7 8	mp2an	⊢ ( ℜ ‘ ( 0 + ( i · 1 ) ) ) = 0
10	1	mulid1i	⊢ ( i · 1 ) = i
11	10	fveq2i	⊢ ( ℜ ‘ ( i · 1 ) ) = ( ℜ ‘ i )
12	5 9 11	3eqtr3ri	⊢ ( ℜ ‘ i ) = 0