Theorem rei

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

	Ref	Expression
Assertion	rei	$$⊢\Re \left(\mathrm{i}\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		ax-1cn	$$⊢1\in ℂ$$
3	1 2	mulcli	$$⊢\mathrm{i}\cdot 1\in ℂ$$
4	3	addlidi	$$⊢0+\mathrm{i}\cdot 1=\mathrm{i}\cdot 1$$
5	4	fveq2i	$$⊢\Re \left(0+\mathrm{i}\cdot 1\right)=\Re \left(\mathrm{i}\cdot 1\right)$$
6		0re	$$⊢0\in ℝ$$
7		1re	$$⊢1\in ℝ$$
8		crre	$$⊢\left(0\in ℝ\wedge 1\in ℝ\right)\to \Re \left(0+\mathrm{i}\cdot 1\right)=0$$
9	6 7 8	mp2an	$$⊢\Re \left(0+\mathrm{i}\cdot 1\right)=0$$
10	1	mulridi	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
11	10	fveq2i	$$⊢\Re \left(\mathrm{i}\cdot 1\right)=\Re \left(\mathrm{i}\right)$$
12	5 9 11	3eqtr3ri	$$⊢\Re \left(\mathrm{i}\right)=0$$