| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mbf0 |
|- (/) e. MblFn |
| 2 |
|
fconstmpt |
|- ( RR X. { 0 } ) = ( x e. RR |-> 0 ) |
| 3 |
2
|
eqcomi |
|- ( x e. RR |-> 0 ) = ( RR X. { 0 } ) |
| 4 |
3
|
fveq2i |
|- ( S.2 ` ( x e. RR |-> 0 ) ) = ( S.2 ` ( RR X. { 0 } ) ) |
| 5 |
|
itg20 |
|- ( S.2 ` ( RR X. { 0 } ) ) = 0 |
| 6 |
4 5
|
eqtri |
|- ( S.2 ` ( x e. RR |-> 0 ) ) = 0 |
| 7 |
|
0re |
|- 0 e. RR |
| 8 |
6 7
|
eqeltri |
|- ( S.2 ` ( x e. RR |-> 0 ) ) e. RR |
| 9 |
8
|
rgenw |
|- A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> 0 ) ) e. RR |
| 10 |
|
noel |
|- -. x e. (/) |
| 11 |
10
|
intnanr |
|- -. ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) |
| 12 |
11
|
iffalsei |
|- if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) = 0 |
| 13 |
12
|
eqcomi |
|- 0 = if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) |
| 14 |
13
|
a1i |
|- ( ( T. /\ x e. RR ) -> 0 = if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) |
| 15 |
14
|
mpteq2dva |
|- ( T. -> ( x e. RR |-> 0 ) = ( x e. RR |-> if ( ( x e. (/) /\ 0 <_ ( Re ` ( 0 / ( _i ^ k ) ) ) ) , ( Re ` ( 0 / ( _i ^ k ) ) ) , 0 ) ) ) |
| 16 |
|
eqidd |
|- ( ( T. /\ x e. (/) ) -> ( Re ` ( 0 / ( _i ^ k ) ) ) = ( Re ` ( 0 / ( _i ^ k ) ) ) ) |
| 17 |
|
dm0 |
|- dom (/) = (/) |
| 18 |
17
|
a1i |
|- ( T. -> dom (/) = (/) ) |
| 19 |
10
|
intnan |
|- -. ( T. /\ x e. (/) ) |
| 20 |
19
|
pm2.21i |
|- ( ( T. /\ x e. (/) ) -> ( (/) ` x ) = 0 ) |
| 21 |
15 16 18 20
|
isibl |
|- ( T. -> ( (/) e. L^1 <-> ( (/) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> 0 ) ) e. RR ) ) ) |
| 22 |
21
|
mptru |
|- ( (/) e. L^1 <-> ( (/) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> 0 ) ) e. RR ) ) |
| 23 |
1 9 22
|
mpbir2an |
|- (/) e. L^1 |