Theorem imi

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

	Ref	Expression
Assertion	imi	$$⊢\Im \left(\mathrm{i}\right)=1$$

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	eqcomi	$$⊢\mathrm{i}\cdot 1=0+\mathrm{i}\cdot 1$$
6	5	fveq2i	$$⊢\Im \left(\mathrm{i}\cdot 1\right)=\Im \left(0+\mathrm{i}\cdot 1\right)$$
7	1	mulridi	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
8	7	fveq2i	$$⊢\Im \left(\mathrm{i}\cdot 1\right)=\Im \left(\mathrm{i}\right)$$
9		0re	$$⊢0\in ℝ$$
10		1re	$$⊢1\in ℝ$$
11		crim	$$⊢\left(0\in ℝ\wedge 1\in ℝ\right)\to \Im \left(0+\mathrm{i}\cdot 1\right)=1$$
12	9 10 11	mp2an	$$⊢\Im \left(0+\mathrm{i}\cdot 1\right)=1$$
13	6 8 12	3eqtr3i	$$⊢\Im \left(\mathrm{i}\right)=1$$