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