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 syl5eq 
 |-  ( 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 ) )