Theorem iexpcyc

Description: Taking _i to the K -th power is the same as using the K mod 4 -th power instead, by i4 . (Contributed by Mario Carneiro, 7-Jul-2014)

	Ref	Expression
Assertion	iexpcyc	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{K\mathrm{mod}4}={\mathrm{i}}^K$$

Proof

Step	Hyp	Ref	Expression
1		zre	$$⊢K\in \mathbb{Z}\to K\in ℝ$$
2		4re	$$⊢4\in ℝ$$
3		4pos	$$⊢0<4$$
4	2 3	elrpii	$$⊢4\in {ℝ}^{+}$$
5		modval	$$⊢\left(K\in ℝ\wedge 4\in {ℝ}^{+}\right)\to K\mathrm{mod}4=K-4⌊\frac{K}{4}⌋$$
6	1 4 5	sylancl	$$⊢K\in \mathbb{Z}\to K\mathrm{mod}4=K-4⌊\frac{K}{4}⌋$$
7	6	oveq2d	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{K\mathrm{mod}4}={\mathrm{i}}^{K-4⌊\frac{K}{4}⌋}$$
8		4z	$$⊢4\in \mathbb{Z}$$
9		4nn	$$⊢4\in \mathbb{N}$$
10		nndivre	$$⊢\left(K\in ℝ\wedge 4\in \mathbb{N}\right)\to \frac{K}{4}\in ℝ$$
11	1 9 10	sylancl	$$⊢K\in \mathbb{Z}\to \frac{K}{4}\in ℝ$$
12	11	flcld	$$⊢K\in \mathbb{Z}\to ⌊\frac{K}{4}⌋\in \mathbb{Z}$$
13		zmulcl	$$⊢\left(4\in \mathbb{Z}\wedge ⌊\frac{K}{4}⌋\in \mathbb{Z}\right)\to 4⌊\frac{K}{4}⌋\in \mathbb{Z}$$
14	8 12 13	sylancr	$$⊢K\in \mathbb{Z}\to 4⌊\frac{K}{4}⌋\in \mathbb{Z}$$
15		ax-icn	$$⊢\mathrm{i}\in ℂ$$
16		ine0	$$⊢\mathrm{i}\ne 0$$
17		expsub	$$⊢\left(\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\wedge \left(K\in \mathbb{Z}\wedge 4⌊\frac{K}{4}⌋\in \mathbb{Z}\right)\right)\to {\mathrm{i}}^{K-4⌊\frac{K}{4}⌋}=\frac{{\mathrm{i}}^K}{{\mathrm{i}}^{4⌊\frac{K}{4}⌋}}$$
18	15 16 17	mpanl12	$$⊢\left(K\in \mathbb{Z}\wedge 4⌊\frac{K}{4}⌋\in \mathbb{Z}\right)\to {\mathrm{i}}^{K-4⌊\frac{K}{4}⌋}=\frac{{\mathrm{i}}^K}{{\mathrm{i}}^{4⌊\frac{K}{4}⌋}}$$
19	14 18	mpdan	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{K-4⌊\frac{K}{4}⌋}=\frac{{\mathrm{i}}^K}{{\mathrm{i}}^{4⌊\frac{K}{4}⌋}}$$
20		expmulz	$$⊢\left(\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\right)\wedge \left(4\in \mathbb{Z}\wedge ⌊\frac{K}{4}⌋\in \mathbb{Z}\right)\right)\to {\mathrm{i}}^{4⌊\frac{K}{4}⌋}={\left({\mathrm{i}}^4\right)}^{⌊\frac{K}{4}⌋}$$
21	15 16 20	mpanl12	$$⊢\left(4\in \mathbb{Z}\wedge ⌊\frac{K}{4}⌋\in \mathbb{Z}\right)\to {\mathrm{i}}^{4⌊\frac{K}{4}⌋}={\left({\mathrm{i}}^4\right)}^{⌊\frac{K}{4}⌋}$$
22	8 12 21	sylancr	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{4⌊\frac{K}{4}⌋}={\left({\mathrm{i}}^4\right)}^{⌊\frac{K}{4}⌋}$$
23		i4	$$⊢{\mathrm{i}}^4=1$$
24	23	oveq1i	$$⊢{\left({\mathrm{i}}^4\right)}^{⌊\frac{K}{4}⌋}=1^{⌊\frac{K}{4}⌋}$$
25		1exp	$$⊢⌊\frac{K}{4}⌋\in \mathbb{Z}\to 1^{⌊\frac{K}{4}⌋}=1$$
26	12 25	syl	$$⊢K\in \mathbb{Z}\to 1^{⌊\frac{K}{4}⌋}=1$$
27	24 26	syl5eq	$$⊢K\in \mathbb{Z}\to {\left({\mathrm{i}}^4\right)}^{⌊\frac{K}{4}⌋}=1$$
28	22 27	eqtrd	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{4⌊\frac{K}{4}⌋}=1$$
29	28	oveq2d	$$⊢K\in \mathbb{Z}\to \frac{{\mathrm{i}}^K}{{\mathrm{i}}^{4⌊\frac{K}{4}⌋}}=\frac{{\mathrm{i}}^K}{1}$$
30		expclz	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge K\in \mathbb{Z}\right)\to {\mathrm{i}}^K\in ℂ$$
31	15 16 30	mp3an12	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^K\in ℂ$$
32	31	div1d	$$⊢K\in \mathbb{Z}\to \frac{{\mathrm{i}}^K}{1}={\mathrm{i}}^K$$
33	29 32	eqtrd	$$⊢K\in \mathbb{Z}\to \frac{{\mathrm{i}}^K}{{\mathrm{i}}^{4⌊\frac{K}{4}⌋}}={\mathrm{i}}^K$$
34	19 33	eqtrd	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{K-4⌊\frac{K}{4}⌋}={\mathrm{i}}^K$$
35	7 34	eqtrd	$$⊢K\in \mathbb{Z}\to {\mathrm{i}}^{K\mathrm{mod}4}={\mathrm{i}}^K$$