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
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )

Proof

Step Hyp Ref Expression
1 zre
 |-  ( K e. ZZ -> K e. RR )
2 4re
 |-  4 e. RR
3 4pos
 |-  0 < 4
4 2 3 elrpii
 |-  4 e. RR+
5 modval
 |-  ( ( K e. RR /\ 4 e. RR+ ) -> ( K mod 4 ) = ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) )
6 1 4 5 sylancl
 |-  ( K e. ZZ -> ( K mod 4 ) = ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) )
7 6 oveq2d
 |-  ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) )
8 4z
 |-  4 e. ZZ
9 4nn
 |-  4 e. NN
10 nndivre
 |-  ( ( K e. RR /\ 4 e. NN ) -> ( K / 4 ) e. RR )
11 1 9 10 sylancl
 |-  ( K e. ZZ -> ( K / 4 ) e. RR )
12 11 flcld
 |-  ( K e. ZZ -> ( |_ ` ( K / 4 ) ) e. ZZ )
13 zmulcl
 |-  ( ( 4 e. ZZ /\ ( |_ ` ( K / 4 ) ) e. ZZ ) -> ( 4 x. ( |_ ` ( K / 4 ) ) ) e. ZZ )
14 8 12 13 sylancr
 |-  ( K e. ZZ -> ( 4 x. ( |_ ` ( K / 4 ) ) ) e. ZZ )
15 ax-icn
 |-  _i e. CC
16 ine0
 |-  _i =/= 0
17 expsub
 |-  ( ( ( _i e. CC /\ _i =/= 0 ) /\ ( K e. ZZ /\ ( 4 x. ( |_ ` ( K / 4 ) ) ) e. ZZ ) ) -> ( _i ^ ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) = ( ( _i ^ K ) / ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) )
18 15 16 17 mpanl12
 |-  ( ( K e. ZZ /\ ( 4 x. ( |_ ` ( K / 4 ) ) ) e. ZZ ) -> ( _i ^ ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) = ( ( _i ^ K ) / ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) )
19 14 18 mpdan
 |-  ( K e. ZZ -> ( _i ^ ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) = ( ( _i ^ K ) / ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) )
20 expmulz
 |-  ( ( ( _i e. CC /\ _i =/= 0 ) /\ ( 4 e. ZZ /\ ( |_ ` ( K / 4 ) ) e. ZZ ) ) -> ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) = ( ( _i ^ 4 ) ^ ( |_ ` ( K / 4 ) ) ) )
21 15 16 20 mpanl12
 |-  ( ( 4 e. ZZ /\ ( |_ ` ( K / 4 ) ) e. ZZ ) -> ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) = ( ( _i ^ 4 ) ^ ( |_ ` ( K / 4 ) ) ) )
22 8 12 21 sylancr
 |-  ( K e. ZZ -> ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) = ( ( _i ^ 4 ) ^ ( |_ ` ( K / 4 ) ) ) )
23 i4
 |-  ( _i ^ 4 ) = 1
24 23 oveq1i
 |-  ( ( _i ^ 4 ) ^ ( |_ ` ( K / 4 ) ) ) = ( 1 ^ ( |_ ` ( K / 4 ) ) )
25 1exp
 |-  ( ( |_ ` ( K / 4 ) ) e. ZZ -> ( 1 ^ ( |_ ` ( K / 4 ) ) ) = 1 )
26 12 25 syl
 |-  ( K e. ZZ -> ( 1 ^ ( |_ ` ( K / 4 ) ) ) = 1 )
27 24 26 eqtrid
 |-  ( K e. ZZ -> ( ( _i ^ 4 ) ^ ( |_ ` ( K / 4 ) ) ) = 1 )
28 22 27 eqtrd
 |-  ( K e. ZZ -> ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) = 1 )
29 28 oveq2d
 |-  ( K e. ZZ -> ( ( _i ^ K ) / ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) = ( ( _i ^ K ) / 1 ) )
30 expclz
 |-  ( ( _i e. CC /\ _i =/= 0 /\ K e. ZZ ) -> ( _i ^ K ) e. CC )
31 15 16 30 mp3an12
 |-  ( K e. ZZ -> ( _i ^ K ) e. CC )
32 31 div1d
 |-  ( K e. ZZ -> ( ( _i ^ K ) / 1 ) = ( _i ^ K ) )
33 29 32 eqtrd
 |-  ( K e. ZZ -> ( ( _i ^ K ) / ( _i ^ ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) = ( _i ^ K ) )
34 19 33 eqtrd
 |-  ( K e. ZZ -> ( _i ^ ( K - ( 4 x. ( |_ ` ( K / 4 ) ) ) ) ) = ( _i ^ K ) )
35 7 34 eqtrd
 |-  ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) )