| Step |
Hyp |
Ref |
Expression |
| 1 |
|
mbfi1fseq.1 |
|- ( ph -> F e. MblFn ) |
| 2 |
|
mbfi1fseq.2 |
|- ( ph -> F : RR --> ( 0 [,) +oo ) ) |
| 3 |
|
mbfi1fseq.3 |
|- J = ( m e. NN , y e. RR |-> ( ( |_ ` ( ( F ` y ) x. ( 2 ^ m ) ) ) / ( 2 ^ m ) ) ) |
| 4 |
|
mbfi1fseq.4 |
|- G = ( m e. NN |-> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) ) |
| 5 |
|
negeq |
|- ( m = A -> -u m = -u A ) |
| 6 |
|
id |
|- ( m = A -> m = A ) |
| 7 |
5 6
|
oveq12d |
|- ( m = A -> ( -u m [,] m ) = ( -u A [,] A ) ) |
| 8 |
7
|
eleq2d |
|- ( m = A -> ( x e. ( -u m [,] m ) <-> x e. ( -u A [,] A ) ) ) |
| 9 |
|
oveq1 |
|- ( m = A -> ( m J x ) = ( A J x ) ) |
| 10 |
9 6
|
breq12d |
|- ( m = A -> ( ( m J x ) <_ m <-> ( A J x ) <_ A ) ) |
| 11 |
10 9 6
|
ifbieq12d |
|- ( m = A -> if ( ( m J x ) <_ m , ( m J x ) , m ) = if ( ( A J x ) <_ A , ( A J x ) , A ) ) |
| 12 |
8 11
|
ifbieq1d |
|- ( m = A -> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) = if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) |
| 13 |
12
|
mpteq2dv |
|- ( m = A -> ( x e. RR |-> if ( x e. ( -u m [,] m ) , if ( ( m J x ) <_ m , ( m J x ) , m ) , 0 ) ) = ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) ) |
| 14 |
|
reex |
|- RR e. _V |
| 15 |
14
|
mptex |
|- ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) e. _V |
| 16 |
13 4 15
|
fvmpt |
|- ( A e. NN -> ( G ` A ) = ( x e. RR |-> if ( x e. ( -u A [,] A ) , if ( ( A J x ) <_ A , ( A J x ) , A ) , 0 ) ) ) |