Theorem im1

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

	Ref	Expression
Assertion	im1	$$⊢\Im \left(1\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		reim0	$$⊢1\in ℝ\to \Im \left(1\right)=0$$
3	1 2	ax-mp	$$⊢\Im \left(1\right)=0$$