Step |
Hyp |
Ref |
Expression |
1 |
|
iblitg.1 |
|- ( ph -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) |
2 |
|
iblitg.2 |
|- ( ( ph /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ K ) ) ) ) |
3 |
|
iblitg.3 |
|- ( ph -> ( x e. A |-> B ) e. L^1 ) |
4 |
|
iblitg.4 |
|- ( ( ph /\ x e. A ) -> B e. V ) |
5 |
1
|
adantr |
|- ( ( ph /\ K e. ZZ ) -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) ) |
6 |
2
|
adantlr |
|- ( ( ( ph /\ K e. ZZ ) /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ K ) ) ) ) |
7 |
|
iexpcyc |
|- ( K e. ZZ -> ( _i ^ ( K mod 4 ) ) = ( _i ^ K ) ) |
8 |
7
|
oveq2d |
|- ( K e. ZZ -> ( B / ( _i ^ ( K mod 4 ) ) ) = ( B / ( _i ^ K ) ) ) |
9 |
8
|
fveq2d |
|- ( K e. ZZ -> ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) = ( Re ` ( B / ( _i ^ K ) ) ) ) |
10 |
9
|
ad2antlr |
|- ( ( ( ph /\ K e. ZZ ) /\ x e. A ) -> ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) = ( Re ` ( B / ( _i ^ K ) ) ) ) |
11 |
6 10
|
eqtr4d |
|- ( ( ( ph /\ K e. ZZ ) /\ x e. A ) -> T = ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) |
12 |
11
|
ibllem |
|- ( ( ph /\ K e. ZZ ) -> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) |
13 |
12
|
mpteq2dv |
|- ( ( ph /\ K e. ZZ ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ T ) , T , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) |
14 |
5 13
|
eqtrd |
|- ( ( ph /\ K e. ZZ ) -> G = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) |
15 |
14
|
fveq2d |
|- ( ( ph /\ K e. ZZ ) -> ( S.2 ` G ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) ) |
16 |
|
oveq2 |
|- ( k = ( K mod 4 ) -> ( _i ^ k ) = ( _i ^ ( K mod 4 ) ) ) |
17 |
16
|
oveq2d |
|- ( k = ( K mod 4 ) -> ( B / ( _i ^ k ) ) = ( B / ( _i ^ ( K mod 4 ) ) ) ) |
18 |
17
|
fveq2d |
|- ( k = ( K mod 4 ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) |
19 |
18
|
breq2d |
|- ( k = ( K mod 4 ) -> ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) <-> 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) ) |
20 |
19
|
anbi2d |
|- ( k = ( K mod 4 ) -> ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) <-> ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) ) ) |
21 |
20 18
|
ifbieq1d |
|- ( k = ( K mod 4 ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) |
22 |
21
|
mpteq2dv |
|- ( k = ( K mod 4 ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) |
23 |
22
|
fveq2d |
|- ( k = ( K mod 4 ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) ) |
24 |
23
|
eleq1d |
|- ( k = ( K mod 4 ) -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) e. RR ) ) |
25 |
|
eqidd |
|- ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) |
26 |
|
eqidd |
|- ( ( ph /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) ) |
27 |
25 26 4
|
isibl2 |
|- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) ) |
28 |
3 27
|
mpbid |
|- ( ph -> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) |
29 |
28
|
simprd |
|- ( ph -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) |
30 |
29
|
adantr |
|- ( ( ph /\ K e. ZZ ) -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) |
31 |
|
4nn |
|- 4 e. NN |
32 |
|
zmodfz |
|- ( ( K e. ZZ /\ 4 e. NN ) -> ( K mod 4 ) e. ( 0 ... ( 4 - 1 ) ) ) |
33 |
31 32
|
mpan2 |
|- ( K e. ZZ -> ( K mod 4 ) e. ( 0 ... ( 4 - 1 ) ) ) |
34 |
|
4m1e3 |
|- ( 4 - 1 ) = 3 |
35 |
34
|
oveq2i |
|- ( 0 ... ( 4 - 1 ) ) = ( 0 ... 3 ) |
36 |
33 35
|
eleqtrdi |
|- ( K e. ZZ -> ( K mod 4 ) e. ( 0 ... 3 ) ) |
37 |
36
|
adantl |
|- ( ( ph /\ K e. ZZ ) -> ( K mod 4 ) e. ( 0 ... 3 ) ) |
38 |
24 30 37
|
rspcdva |
|- ( ( ph /\ K e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) ) , ( Re ` ( B / ( _i ^ ( K mod 4 ) ) ) ) , 0 ) ) ) e. RR ) |
39 |
15 38
|
eqeltrd |
|- ( ( ph /\ K e. ZZ ) -> ( S.2 ` G ) e. RR ) |