Step |
Hyp |
Ref |
Expression |
0 |
|
cibl |
|- L^1 |
1 |
|
vf |
|- f |
2 |
|
cmbf |
|- MblFn |
3 |
|
vk |
|- k |
4 |
|
cc0 |
|- 0 |
5 |
|
cfz |
|- ... |
6 |
|
c3 |
|- 3 |
7 |
4 6 5
|
co |
|- ( 0 ... 3 ) |
8 |
|
citg2 |
|- S.2 |
9 |
|
vx |
|- x |
10 |
|
cr |
|- RR |
11 |
|
cre |
|- Re |
12 |
1
|
cv |
|- f |
13 |
9
|
cv |
|- x |
14 |
13 12
|
cfv |
|- ( f ` x ) |
15 |
|
cdiv |
|- / |
16 |
|
ci |
|- _i |
17 |
|
cexp |
|- ^ |
18 |
3
|
cv |
|- k |
19 |
16 18 17
|
co |
|- ( _i ^ k ) |
20 |
14 19 15
|
co |
|- ( ( f ` x ) / ( _i ^ k ) ) |
21 |
20 11
|
cfv |
|- ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) |
22 |
|
vy |
|- y |
23 |
12
|
cdm |
|- dom f |
24 |
13 23
|
wcel |
|- x e. dom f |
25 |
|
cle |
|- <_ |
26 |
22
|
cv |
|- y |
27 |
4 26 25
|
wbr |
|- 0 <_ y |
28 |
24 27
|
wa |
|- ( x e. dom f /\ 0 <_ y ) |
29 |
28 26 4
|
cif |
|- if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) |
30 |
22 21 29
|
csb |
|- [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) |
31 |
9 10 30
|
cmpt |
|- ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) |
32 |
31 8
|
cfv |
|- ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) |
33 |
32 10
|
wcel |
|- ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR |
34 |
33 3 7
|
wral |
|- A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR |
35 |
34 1 2
|
crab |
|- { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR } |
36 |
0 35
|
wceq |
|- L^1 = { f e. MblFn | A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> [_ ( Re ` ( ( f ` x ) / ( _i ^ k ) ) ) / y ]_ if ( ( x e. dom f /\ 0 <_ y ) , y , 0 ) ) ) e. RR } |