i4

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

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3		expadd	$⊢ (i \in ℂ \land 2 \in ℕ_{0} \land 2 \in ℕ_{0}) \to i^{2 + 2} = i^{2} i^{2}$
4	1 2 2 3	mp3an	$⊢ i^{2 + 2} = i^{2} i^{2}$
5		2p2e4	$⊢ 2 + 2 = 4$
6	5	oveq2i	$⊢ i^{2 + 2} = i^{4}$
7		i2	$⊢ i^{2} = - 1$
8	7 7	oveq12i	$⊢ i^{2} 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	$⊢ i^{2} i^{2} = 1$
13	4 6 12	3eqtr3i	$⊢ i^{4} = 1$

Metamath Proof Explorer