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	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 𝐾 mod 4 ) ) = ( i ↑ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		zre	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
2		4re	⊢ 4 ∈ ℝ
3		4pos	⊢ 0 < 4
4	2 3	elrpii	⊢ 4 ∈ ℝ+
5		modval	⊢ ( ( 𝐾 ∈ ℝ ∧ 4 ∈ ℝ+ ) → ( 𝐾 mod 4 ) = ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) )
6	1 4 5	sylancl	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 mod 4 ) = ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) )
7	6	oveq2d	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 𝐾 mod 4 ) ) = ( i ↑ ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) )
8		4z	⊢ 4 ∈ ℤ
9		4nn	⊢ 4 ∈ ℕ
10		nndivre	⊢ ( ( 𝐾 ∈ ℝ ∧ 4 ∈ ℕ ) → ( 𝐾 / 4 ) ∈ ℝ )
11	1 9 10	sylancl	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 / 4 ) ∈ ℝ )
12	11	flcld	⊢ ( 𝐾 ∈ ℤ → ( ⌊ ‘ ( 𝐾 / 4 ) ) ∈ ℤ )
13		zmulcl	⊢ ( ( 4 ∈ ℤ ∧ ( ⌊ ‘ ( 𝐾 / 4 ) ) ∈ ℤ ) → ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ∈ ℤ )
14	8 12 13	sylancr	⊢ ( 𝐾 ∈ ℤ → ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ∈ ℤ )
15		ax-icn	⊢ i ∈ ℂ
16		ine0	⊢ i ≠ 0
17		expsub	⊢ ( ( ( i ∈ ℂ ∧ i ≠ 0 ) ∧ ( 𝐾 ∈ ℤ ∧ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ∈ ℤ ) ) → ( i ↑ ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) = ( ( i ↑ 𝐾 ) / ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) )
18	15 16 17	mpanl12	⊢ ( ( 𝐾 ∈ ℤ ∧ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ∈ ℤ ) → ( i ↑ ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) = ( ( i ↑ 𝐾 ) / ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) )
19	14 18	mpdan	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) = ( ( i ↑ 𝐾 ) / ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) )
20		expmulz	⊢ ( ( ( i ∈ ℂ ∧ i ≠ 0 ) ∧ ( 4 ∈ ℤ ∧ ( ⌊ ‘ ( 𝐾 / 4 ) ) ∈ ℤ ) ) → ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) = ( ( i ↑ 4 ) ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) )
21	15 16 20	mpanl12	⊢ ( ( 4 ∈ ℤ ∧ ( ⌊ ‘ ( 𝐾 / 4 ) ) ∈ ℤ ) → ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) = ( ( i ↑ 4 ) ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) )
22	8 12 21	sylancr	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) = ( ( i ↑ 4 ) ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) )
23		i4	⊢ ( i ↑ 4 ) = 1
24	23	oveq1i	⊢ ( ( i ↑ 4 ) ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) = ( 1 ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) )
25		1exp	⊢ ( ( ⌊ ‘ ( 𝐾 / 4 ) ) ∈ ℤ → ( 1 ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) = 1 )
26	12 25	syl	⊢ ( 𝐾 ∈ ℤ → ( 1 ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) = 1 )
27	24 26	eqtrid	⊢ ( 𝐾 ∈ ℤ → ( ( i ↑ 4 ) ↑ ( ⌊ ‘ ( 𝐾 / 4 ) ) ) = 1 )
28	22 27	eqtrd	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) = 1 )
29	28	oveq2d	⊢ ( 𝐾 ∈ ℤ → ( ( i ↑ 𝐾 ) / ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) = ( ( i ↑ 𝐾 ) / 1 ) )
30		expclz	⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( i ↑ 𝐾 ) ∈ ℂ )
31	15 16 30	mp3an12	⊢ ( 𝐾 ∈ ℤ → ( i ↑ 𝐾 ) ∈ ℂ )
32	31	div1d	⊢ ( 𝐾 ∈ ℤ → ( ( i ↑ 𝐾 ) / 1 ) = ( i ↑ 𝐾 ) )
33	29 32	eqtrd	⊢ ( 𝐾 ∈ ℤ → ( ( i ↑ 𝐾 ) / ( i ↑ ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) = ( i ↑ 𝐾 ) )
34	19 33	eqtrd	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 𝐾 − ( 4 · ( ⌊ ‘ ( 𝐾 / 4 ) ) ) ) ) = ( i ↑ 𝐾 ) )
35	7 34	eqtrd	⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 𝐾 mod 4 ) ) = ( i ↑ 𝐾 ) )