Metamath Proof Explorer

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 syl5eq ⊢ ( 𝐾 ∈ ℤ → ( ( 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 ↑ 𝐾 ) )