Theorem i4

Description: _i to the fourth power. (Contributed by NM, 31-Jan-2007)

	Ref	Expression
Assertion	i4	$$⊢{\mathrm{i}}^4=1$$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$$⊢\mathrm{i}\in ℂ$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3		expadd	$$⊢\left(\mathrm{i}\in ℂ\wedge 2\in {\mathbb{N}}_0\wedge 2\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^{2+2}={\mathrm{i}}^2{\mathrm{i}}^2$$
4	1 2 2 3	mp3an	$$⊢{\mathrm{i}}^{2+2}={\mathrm{i}}^2{\mathrm{i}}^2$$
5		2p2e4	$$⊢2+2=4$$
6	5	oveq2i	$$⊢{\mathrm{i}}^{2+2}={\mathrm{i}}^4$$
7		i2	$$⊢{\mathrm{i}}^2=-1$$
8	7 7	oveq12i	$$⊢{\mathrm{i}}^2{\mathrm{i}}^2=-1-1$$
9		ax-1cn	$$⊢1\in ℂ$$
10	9 9	mul2negi	$$⊢-1-1=1\cdot 1$$
11		1t1e1	$$⊢1\cdot 1=1$$
12	8 10 11	3eqtri	$$⊢{\mathrm{i}}^2{\mathrm{i}}^2=1$$
13	4 6 12	3eqtr3i	$$⊢{\mathrm{i}}^4=1$$