Theorem igz

Description: _i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014)

	Ref	Expression
Assertion	igz	$$⊢\mathrm{i}\in \mathbb{Z}\left[i\right]$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		rei	$$⊢\Re \left(\mathrm{i}\right)=0$$
3		0z	$$⊢0\in \mathbb{Z}$$
4	2 3	eqeltri	$$⊢\Re \left(\mathrm{i}\right)\in \mathbb{Z}$$
5		imi	$$⊢\Im \left(\mathrm{i}\right)=1$$
6		1z	$$⊢1\in \mathbb{Z}$$
7	5 6	eqeltri	$$⊢\Im \left(\mathrm{i}\right)\in \mathbb{Z}$$
8		elgz	$$⊢\mathrm{i}\in \mathbb{Z}\left[i\right]\leftrightarrow \left(\mathrm{i}\in ℂ\wedge \Re \left(\mathrm{i}\right)\in \mathbb{Z}\wedge \Im \left(\mathrm{i}\right)\in \mathbb{Z}\right)$$
9	1 4 7 8	mpbir3an	$$⊢\mathrm{i}\in \mathbb{Z}\left[i\right]$$