MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfi1fseqlem6 Structured version   Visualization version   Unicode version

Theorem mbfi1fseqlem6 22757
Description: Lemma for mbfi1fseq 22758. Verify that  G converges pointwise to  F, and wrap up the existence quantifier. (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
mbfi1fseq.1  |-  ( ph  ->  F  e. MblFn )
mbfi1fseq.2  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
mbfi1fseq.3  |-  J  =  ( m  e.  NN ,  y  e.  RR  |->  ( ( |_ `  ( ( F `  y )  x.  (
2 ^ m ) ) )  /  (
2 ^ m ) ) )
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 ) ) )
Assertion
Ref Expression
mbfi1fseqlem6  |-  ( ph  ->  E. g ( g : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0p  oR  <_  ( g `  n )  /\  (
g `  n )  oR  <_  ( g `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( g `
 n ) `  x ) )  ~~>  ( F `
 x ) ) )
Distinct variable groups:    g, m, n, x, y, F    g, G, n, x    m, J    ph, m, n, x, y
Allowed substitution hints:    ph( g)    G( y, m)    J( x, y, g, n)

Proof of Theorem mbfi1fseqlem6
Dummy variables  j 
k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfi1fseq.1 . . 3  |-  ( ph  ->  F  e. MblFn )
2 mbfi1fseq.2 . . 3  |-  ( ph  ->  F : RR --> ( 0 [,) +oo ) )
3 mbfi1fseq.3 . . 3  |-  J  =  ( m  e.  NN ,  y  e.  RR  |->  ( ( |_ `  ( ( F `  y )  x.  (
2 ^ m ) ) )  /  (
2 ^ m ) ) )
4 mbfi1fseq.4 . . 3  |-  G  =  ( m  e.  NN  |->  ( x  e.  RR  |->  if ( x  e.  (
-u m [,] m
) ,  if ( ( m J x )  <_  m , 
( m J x ) ,  m ) ,  0 ) ) )
51, 2, 3, 4mbfi1fseqlem4 22755 . 2  |-  ( ph  ->  G : NN --> dom  S.1 )
61, 2, 3, 4mbfi1fseqlem5 22756 . . 3  |-  ( (
ph  /\  n  e.  NN )  ->  ( 0p  oR  <_ 
( G `  n
)  /\  ( G `  n )  oR  <_  ( G `  ( n  +  1
) ) ) )
76ralrimiva 2809 . 2  |-  ( ph  ->  A. n  e.  NN  ( 0p  oR  <_  ( G `  n )  /\  ( G `  n )  oR  <_  ( G `
 ( n  + 
1 ) ) ) )
8 simpr 468 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  RR )
98recnd 9687 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  x  e.  CC )
109abscld 13575 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  x )  e.  RR )
112ffvelrnda 6037 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  ( 0 [,) +oo ) )
12 elrege0 11764 . . . . . . . 8  |-  ( ( F `  x )  e.  ( 0 [,) +oo )  <->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
1311, 12sylib 201 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( F `  x )  e.  RR  /\  0  <_  ( F `  x
) ) )
1413simpld 466 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  RR )
1510, 14readdcld 9688 . . . . 5  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( abs `  x )  +  ( F `  x ) )  e.  RR )
16 arch 10890 . . . . 5  |-  ( ( ( abs `  x
)  +  ( F `
 x ) )  e.  RR  ->  E. k  e.  NN  ( ( abs `  x )  +  ( F `  x ) )  <  k )
1715, 16syl 17 . . . 4  |-  ( (
ph  /\  x  e.  RR )  ->  E. k  e.  NN  ( ( abs `  x )  +  ( F `  x ) )  <  k )
18 eqid 2471 . . . . 5  |-  ( ZZ>= `  k )  =  (
ZZ>= `  k )
19 nnz 10983 . . . . . 6  |-  ( k  e.  NN  ->  k  e.  ZZ )
2019ad2antrl 742 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  ->  k  e.  ZZ )
21 nnuz 11218 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
22 1zzd 10992 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  1  e.  ZZ )
23 halfcn 10852 . . . . . . . . . 10  |-  ( 1  /  2 )  e.  CC
2423a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( 1  /  2 )  e.  CC )
25 halfre 10851 . . . . . . . . . . . 12  |-  ( 1  /  2 )  e.  RR
26 0re 9661 . . . . . . . . . . . . 13  |-  0  e.  RR
27 halfgt0 10853 . . . . . . . . . . . . 13  |-  0  <  ( 1  /  2
)
2826, 25, 27ltleii 9775 . . . . . . . . . . . 12  |-  0  <_  ( 1  /  2
)
29 absid 13436 . . . . . . . . . . . 12  |-  ( ( ( 1  /  2
)  e.  RR  /\  0  <_  ( 1  / 
2 ) )  -> 
( abs `  (
1  /  2 ) )  =  ( 1  /  2 ) )
3025, 28, 29mp2an 686 . . . . . . . . . . 11  |-  ( abs `  ( 1  /  2
) )  =  ( 1  /  2 )
31 halflt1 10854 . . . . . . . . . . 11  |-  ( 1  /  2 )  <  1
3230, 31eqbrtri 4415 . . . . . . . . . 10  |-  ( abs `  ( 1  /  2
) )  <  1
3332a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  RR )  ->  ( abs `  ( 1  /  2
) )  <  1
)
3424, 33expcnv 13999 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN0  |->  ( ( 1  /  2 ) ^ n ) )  ~~>  0 )
3514recnd 9687 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ( F `
 x )  e.  CC )
36 nnex 10637 . . . . . . . . . 10  |-  NN  e.  _V
3736mptex 6152 . . . . . . . . 9  |-  ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) )  e.  _V
3837a1i 11 . . . . . . . 8  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) )  e.  _V )
39 nnnn0 10900 . . . . . . . . . . 11  |-  ( j  e.  NN  ->  j  e.  NN0 )
4039adantl 473 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  j  e.  NN0 )
41 oveq2 6316 . . . . . . . . . . 11  |-  ( n  =  j  ->  (
( 1  /  2
) ^ n )  =  ( ( 1  /  2 ) ^
j ) )
42 eqid 2471 . . . . . . . . . . 11  |-  ( n  e.  NN0  |->  ( ( 1  /  2 ) ^ n ) )  =  ( n  e. 
NN0  |->  ( ( 1  /  2 ) ^
n ) )
43 ovex 6336 . . . . . . . . . . 11  |-  ( ( 1  /  2 ) ^ j )  e. 
_V
4441, 42, 43fvmpt 5963 . . . . . . . . . 10  |-  ( j  e.  NN0  ->  ( ( n  e.  NN0  |->  ( ( 1  /  2 ) ^ n ) ) `
 j )  =  ( ( 1  / 
2 ) ^ j
) )
4540, 44syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( n  e.  NN0  |->  ( ( 1  / 
2 ) ^ n
) ) `  j
)  =  ( ( 1  /  2 ) ^ j ) )
46 expcl 12328 . . . . . . . . . 10  |-  ( ( ( 1  /  2
)  e.  CC  /\  j  e.  NN0 )  -> 
( ( 1  / 
2 ) ^ j
)  e.  CC )
4723, 40, 46sylancr 676 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( 1  /  2
) ^ j )  e.  CC )
4845, 47eqeltrd 2549 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( n  e.  NN0  |->  ( ( 1  / 
2 ) ^ n
) ) `  j
)  e.  CC )
4941oveq2d 6324 . . . . . . . . . . 11  |-  ( n  =  j  ->  (
( F `  x
)  -  ( ( 1  /  2 ) ^ n ) )  =  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ j
) ) )
50 eqid 2471 . . . . . . . . . . 11  |-  ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) )  =  ( n  e.  NN  |->  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ n
) ) )
51 ovex 6336 . . . . . . . . . . 11  |-  ( ( F `  x )  -  ( ( 1  /  2 ) ^
j ) )  e. 
_V
5249, 50, 51fvmpt 5963 . . . . . . . . . 10  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( ( F `  x )  -  (
( 1  /  2
) ^ n ) ) ) `  j
)  =  ( ( F `  x )  -  ( ( 1  /  2 ) ^
j ) ) )
5352adantl 473 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( ( F `  x )  -  (
( 1  /  2
) ^ n ) ) ) `  j
)  =  ( ( F `  x )  -  ( ( 1  /  2 ) ^
j ) ) )
5445oveq2d 6324 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( F `  x
)  -  ( ( n  e.  NN0  |->  ( ( 1  /  2 ) ^ n ) ) `
 j ) )  =  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ j
) ) )
5553, 54eqtr4d 2508 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  j  e.  NN )  ->  (
( n  e.  NN  |->  ( ( F `  x )  -  (
( 1  /  2
) ^ n ) ) ) `  j
)  =  ( ( F `  x )  -  ( ( n  e.  NN0  |->  ( ( 1  /  2 ) ^ n ) ) `
 j ) ) )
5621, 22, 34, 35, 38, 48, 55climsubc2 13779 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) )  ~~>  ( ( F `  x )  -  0 ) )
5735subid1d 9994 . . . . . . 7  |-  ( (
ph  /\  x  e.  RR )  ->  ( ( F `  x )  -  0 )  =  ( F `  x
) )
5856, 57breqtrd 4420 . . . . . 6  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) )  ~~>  ( F `  x
) )
5958adantr 472 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  ->  ( n  e.  NN  |->  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ n
) ) )  ~~>  ( F `
 x ) )
6036mptex 6152 . . . . . 6  |-  ( n  e.  NN  |->  ( ( G `  n ) `
 x ) )  e.  _V
6160a1i 11 . . . . 5  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  ->  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )  e. 
_V )
62 simprl 772 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  ->  k  e.  NN )
63 eluznn 11252 . . . . . . . 8  |-  ( ( k  e.  NN  /\  j  e.  ( ZZ>= `  k ) )  -> 
j  e.  NN )
6462, 63sylan 479 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  j  e.  NN )
6564, 52syl 17 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) ) `
 j )  =  ( ( F `  x )  -  (
( 1  /  2
) ^ j ) ) )
6614ad2antrr 740 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( F `  x )  e.  RR )
6764, 39syl 17 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  j  e.  NN0 )
68 reexpcl 12327 . . . . . . . 8  |-  ( ( ( 1  /  2
)  e.  RR  /\  j  e.  NN0 )  -> 
( ( 1  / 
2 ) ^ j
)  e.  RR )
6925, 67, 68sylancr 676 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( 1  /  2 ) ^
j )  e.  RR )
7066, 69resubcld 10068 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ j
) )  e.  RR )
7165, 70eqeltrd 2549 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) ) `
 j )  e.  RR )
72 fveq2 5879 . . . . . . . . 9  |-  ( n  =  j  ->  ( G `  n )  =  ( G `  j ) )
7372fveq1d 5881 . . . . . . . 8  |-  ( n  =  j  ->  (
( G `  n
) `  x )  =  ( ( G `
 j ) `  x ) )
74 eqid 2471 . . . . . . . 8  |-  ( n  e.  NN  |->  ( ( G `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )
75 fvex 5889 . . . . . . . 8  |-  ( ( G `  j ) `
 x )  e. 
_V
7673, 74, 75fvmpt 5963 . . . . . . 7  |-  ( j  e.  NN  ->  (
( n  e.  NN  |->  ( ( G `  n ) `  x
) ) `  j
)  =  ( ( G `  j ) `
 x ) )
7764, 76syl 17 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( G `  n ) `
 x ) ) `
 j )  =  ( ( G `  j ) `  x
) )
785ad3antrrr 744 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  G : NN --> dom  S.1 )
7978, 64ffvelrnd 6038 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( G `  j )  e.  dom  S.1 )
80 i1ff 22713 . . . . . . . 8  |-  ( ( G `  j )  e.  dom  S.1  ->  ( G `  j ) : RR --> RR )
8179, 80syl 17 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( G `  j ) : RR --> RR )
828ad2antrr 740 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  x  e.  RR )
8381, 82ffvelrnd 6038 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( G `
 j ) `  x )  e.  RR )
8477, 83eqeltrd 2549 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( G `  n ) `
 x ) ) `
 j )  e.  RR )
8535ad2antrr 740 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( F `  x )  e.  CC )
86 2nn 10790 . . . . . . . . . . . . . 14  |-  2  e.  NN
87 nnexpcl 12323 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  NN  /\  j  e.  NN0 )  -> 
( 2 ^ j
)  e.  NN )
8886, 67, 87sylancr 676 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( 2 ^ j )  e.  NN )
8988nnred 10646 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( 2 ^ j )  e.  RR )
9089recnd 9687 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( 2 ^ j )  e.  CC )
9188nnne0d 10676 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( 2 ^ j )  =/=  0
)
9285, 90, 91divcan4d 10411 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( F `  x )  x.  ( 2 ^ j ) )  / 
( 2 ^ j
) )  =  ( F `  x ) )
9392eqcomd 2477 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( F `  x )  =  ( ( ( F `  x )  x.  (
2 ^ j ) )  /  ( 2 ^ j ) ) )
94 2cnd 10704 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  2  e.  CC )
95 2ne0 10724 . . . . . . . . . . 11  |-  2  =/=  0
9695a1i 11 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  2  =/=  0
)
97 eluzelz 11192 . . . . . . . . . . 11  |-  ( j  e.  ( ZZ>= `  k
)  ->  j  e.  ZZ )
9897adantl 473 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  j  e.  ZZ )
9994, 96, 98exprecd 12462 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( 1  /  2 ) ^
j )  =  ( 1  /  ( 2 ^ j ) ) )
10093, 99oveq12d 6326 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ j
) )  =  ( ( ( ( F `
 x )  x.  ( 2 ^ j
) )  /  (
2 ^ j ) )  -  ( 1  /  ( 2 ^ j ) ) ) )
10166, 89remulcld 9689 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  x.  ( 2 ^ j
) )  e.  RR )
102101recnd 9687 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  x.  ( 2 ^ j
) )  e.  CC )
103 1cnd 9677 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  1  e.  CC )
104102, 103, 90, 91divsubdird 10444 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  / 
( 2 ^ j
) )  =  ( ( ( ( F `
 x )  x.  ( 2 ^ j
) )  /  (
2 ^ j ) )  -  ( 1  /  ( 2 ^ j ) ) ) )
105100, 104eqtr4d 2508 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ j
) )  =  ( ( ( ( F `
 x )  x.  ( 2 ^ j
) )  -  1 )  /  ( 2 ^ j ) ) )
106 fllep1 12070 . . . . . . . . . 10  |-  ( ( ( F `  x
)  x.  ( 2 ^ j ) )  e.  RR  ->  (
( F `  x
)  x.  ( 2 ^ j ) )  <_  ( ( |_
`  ( ( F `
 x )  x.  ( 2 ^ j
) ) )  +  1 ) )
107101, 106syl 17 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  x.  ( 2 ^ j
) )  <_  (
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  +  1 ) )
108 1red 9676 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  1  e.  RR )
109 reflcl 12065 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  x.  ( 2 ^ j ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  x.  ( 2 ^ j
) ) )  e.  RR )
110101, 109syl 17 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( |_ `  ( ( F `  x )  x.  (
2 ^ j ) ) )  e.  RR )
111101, 108, 110lesubaddd 10231 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  <_ 
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  <->  ( ( F `
 x )  x.  ( 2 ^ j
) )  <_  (
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  +  1 ) ) )
112107, 111mpbird 240 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( F `  x )  x.  ( 2 ^ j ) )  - 
1 )  <_  ( |_ `  ( ( F `
 x )  x.  ( 2 ^ j
) ) ) )
113 peano2rem 9961 . . . . . . . . . 10  |-  ( ( ( F `  x
)  x.  ( 2 ^ j ) )  e.  RR  ->  (
( ( F `  x )  x.  (
2 ^ j ) )  -  1 )  e.  RR )
114101, 113syl 17 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( F `  x )  x.  ( 2 ^ j ) )  - 
1 )  e.  RR )
11588nngt0d 10675 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  0  <  (
2 ^ j ) )
116 lediv1 10492 . . . . . . . . 9  |-  ( ( ( ( ( F `
 x )  x.  ( 2 ^ j
) )  -  1 )  e.  RR  /\  ( |_ `  ( ( F `  x )  x.  ( 2 ^ j ) ) )  e.  RR  /\  (
( 2 ^ j
)  e.  RR  /\  0  <  ( 2 ^ j ) ) )  ->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  <_ 
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  <->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  / 
( 2 ^ j
) )  <_  (
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) ) )
117114, 110, 89, 115, 116syl112anc 1296 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  <_ 
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  <->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  / 
( 2 ^ j
) )  <_  (
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) ) )
118112, 117mpbid 215 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( ( F `  x
)  x.  ( 2 ^ j ) )  -  1 )  / 
( 2 ^ j
) )  <_  (
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) )
119105, 118eqbrtrd 4416 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  -  ( ( 1  / 
2 ) ^ j
) )  <_  (
( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) )
1201, 2, 3, 4mbfi1fseqlem2 22753 . . . . . . . . . 10  |-  ( j  e.  NN  ->  ( G `  j )  =  ( x  e.  RR  |->  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_  j ,  ( j J x ) ,  j ) ,  0 ) ) )
12164, 120syl 17 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( G `  j )  =  ( x  e.  RR  |->  if ( x  e.  (
-u j [,] j
) ,  if ( ( j J x )  <_  j , 
( j J x ) ,  j ) ,  0 ) ) )
122121fveq1d 5881 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( G `
 j ) `  x )  =  ( ( x  e.  RR  |->  if ( x  e.  (
-u j [,] j
) ,  if ( ( j J x )  <_  j , 
( j J x ) ,  j ) ,  0 ) ) `
 x ) )
123 ovex 6336 . . . . . . . . . . 11  |-  ( j J x )  e. 
_V
124 vex 3034 . . . . . . . . . . 11  |-  j  e. 
_V
125123, 124ifex 3940 . . . . . . . . . 10  |-  if ( ( j J x )  <_  j , 
( j J x ) ,  j )  e.  _V
126 c0ex 9655 . . . . . . . . . 10  |-  0  e.  _V
127125, 126ifex 3940 . . . . . . . . 9  |-  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_ 
j ,  ( j J x ) ,  j ) ,  0 )  e.  _V
128 eqid 2471 . . . . . . . . . 10  |-  ( x  e.  RR  |->  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_ 
j ,  ( j J x ) ,  j ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  (
-u j [,] j
) ,  if ( ( j J x )  <_  j , 
( j J x ) ,  j ) ,  0 ) )
129128fvmpt2 5972 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  if ( x  e.  (
-u j [,] j
) ,  if ( ( j J x )  <_  j , 
( j J x ) ,  j ) ,  0 )  e. 
_V )  ->  (
( x  e.  RR  |->  if ( x  e.  (
-u j [,] j
) ,  if ( ( j J x )  <_  j , 
( j J x ) ,  j ) ,  0 ) ) `
 x )  =  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_  j ,  ( j J x ) ,  j ) ,  0 ) )
13082, 127, 129sylancl 675 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( x  e.  RR  |->  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_ 
j ,  ( j J x ) ,  j ) ,  0 ) ) `  x
)  =  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_ 
j ,  ( j J x ) ,  j ) ,  0 ) )
13177, 122, 1303eqtrd 2509 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( G `  n ) `
 x ) ) `
 j )  =  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_  j ,  ( j J x ) ,  j ) ,  0 ) )
13210ad2antrr 740 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( abs `  x
)  e.  RR )
13315ad2antrr 740 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( abs `  x )  +  ( F `  x ) )  e.  RR )
13464nnred 10646 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  j  e.  RR )
13511ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( F `  x )  e.  ( 0 [,) +oo )
)
136135, 12sylib 201 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( F `
 x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
137136simprd 470 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  0  <_  ( F `  x )
)
138132, 66addge01d 10222 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( 0  <_ 
( F `  x
)  <->  ( abs `  x
)  <_  ( ( abs `  x )  +  ( F `  x
) ) ) )
139137, 138mpbid 215 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( abs `  x
)  <_  ( ( abs `  x )  +  ( F `  x
) ) )
14062adantr 472 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  k  e.  NN )
141140nnred 10646 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  k  e.  RR )
142 simplrr 779 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( abs `  x )  +  ( F `  x ) )  <  k )
143133, 141, 142ltled 9800 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( abs `  x )  +  ( F `  x ) )  <_  k )
144 eluzle 11195 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ZZ>= `  k
)  ->  k  <_  j )
145144adantl 473 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  k  <_  j
)
146133, 141, 134, 143, 145letrd 9809 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( abs `  x )  +  ( F `  x ) )  <_  j )
147132, 133, 134, 139, 146letrd 9809 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( abs `  x
)  <_  j )
14882, 134absled 13569 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( abs `  x )  <_  j  <->  (
-u j  <_  x  /\  x  <_  j ) ) )
149147, 148mpbid 215 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( -u j  <_  x  /\  x  <_ 
j ) )
150149simpld 466 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  -u j  <_  x
)
151149simprd 470 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  x  <_  j
)
152134renegcld 10067 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  -u j  e.  RR )
153 elicc2 11724 . . . . . . . . . 10  |-  ( (
-u j  e.  RR  /\  j  e.  RR )  ->  ( x  e.  ( -u j [,] j )  <->  ( x  e.  RR  /\  -u j  <_  x  /\  x  <_ 
j ) ) )
154152, 134, 153syl2anc 673 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( x  e.  ( -u j [,] j )  <->  ( x  e.  RR  /\  -u j  <_  x  /\  x  <_ 
j ) ) )
15582, 150, 151, 154mpbir3and 1213 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  x  e.  (
-u j [,] j
) )
156155iftrued 3880 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  if ( x  e.  ( -u j [,] j ) ,  if ( ( j J x )  <_  j ,  ( j J x ) ,  j ) ,  0 )  =  if ( ( j J x )  <_  j ,  ( j J x ) ,  j ) )
157 simpr 468 . . . . . . . . . . . . . . . 16  |-  ( ( m  =  j  /\  y  =  x )  ->  y  =  x )
158157fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( ( m  =  j  /\  y  =  x )  ->  ( F `  y
)  =  ( F `
 x ) )
159 simpl 464 . . . . . . . . . . . . . . . 16  |-  ( ( m  =  j  /\  y  =  x )  ->  m  =  j )
160159oveq2d 6324 . . . . . . . . . . . . . . 15  |-  ( ( m  =  j  /\  y  =  x )  ->  ( 2 ^ m
)  =  ( 2 ^ j ) )
161158, 160oveq12d 6326 . . . . . . . . . . . . . 14  |-  ( ( m  =  j  /\  y  =  x )  ->  ( ( F `  y )  x.  (
2 ^ m ) )  =  ( ( F `  x )  x.  ( 2 ^ j ) ) )
162161fveq2d 5883 . . . . . . . . . . . . 13  |-  ( ( m  =  j  /\  y  =  x )  ->  ( |_ `  (
( F `  y
)  x.  ( 2 ^ m ) ) )  =  ( |_
`  ( ( F `
 x )  x.  ( 2 ^ j
) ) ) )
163162, 160oveq12d 6326 . . . . . . . . . . . 12  |-  ( ( m  =  j  /\  y  =  x )  ->  ( ( |_ `  ( ( F `  y )  x.  (
2 ^ m ) ) )  /  (
2 ^ m ) )  =  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) )
164 ovex 6336 . . . . . . . . . . . 12  |-  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) )  e. 
_V
165163, 3, 164ovmpt2a 6446 . . . . . . . . . . 11  |-  ( ( j  e.  NN  /\  x  e.  RR )  ->  ( j J x )  =  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) )
16664, 82, 165syl2anc 673 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( j J x )  =  ( ( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) ) )
167110, 88nndivred 10680 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( |_
`  ( ( F `
 x )  x.  ( 2 ^ j
) ) )  / 
( 2 ^ j
) )  e.  RR )
168 flle 12068 . . . . . . . . . . . . 13  |-  ( ( ( F `  x
)  x.  ( 2 ^ j ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  x.  ( 2 ^ j
) ) )  <_ 
( ( F `  x )  x.  (
2 ^ j ) ) )
169101, 168syl 17 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( |_ `  ( ( F `  x )  x.  (
2 ^ j ) ) )  <_  (
( F `  x
)  x.  ( 2 ^ j ) ) )
170 ledivmul2 10506 . . . . . . . . . . . . 13  |-  ( ( ( |_ `  (
( F `  x
)  x.  ( 2 ^ j ) ) )  e.  RR  /\  ( F `  x )  e.  RR  /\  (
( 2 ^ j
)  e.  RR  /\  0  <  ( 2 ^ j ) ) )  ->  ( ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) )  <_ 
( F `  x
)  <->  ( |_ `  ( ( F `  x )  x.  (
2 ^ j ) ) )  <_  (
( F `  x
)  x.  ( 2 ^ j ) ) ) )
171110, 66, 89, 115, 170syl112anc 1296 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ j ) ) )  /  ( 2 ^ j ) )  <_ 
( F `  x
)  <->  ( |_ `  ( ( F `  x )  x.  (
2 ^ j ) ) )  <_  (
( F `  x
)  x.  ( 2 ^ j ) ) ) )
172169, 171mpbird 240 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( |_
`  ( ( F `
 x )  x.  ( 2 ^ j
) ) )  / 
( 2 ^ j
) )  <_  ( F `  x )
)
1739ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  x  e.  CC )
174173absge0d 13583 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  0  <_  ( abs `  x ) )
17566, 132addge02d 10223 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( 0  <_ 
( abs `  x
)  <->  ( F `  x )  <_  (
( abs `  x
)  +  ( F `
 x ) ) ) )
176174, 175mpbid 215 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( F `  x )  <_  (
( abs `  x
)  +  ( F `
 x ) ) )
17766, 133, 134, 176, 146letrd 9809 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( F `  x )  <_  j
)
178167, 66, 134, 172, 177letrd 9809 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( |_
`  ( ( F `
 x )  x.  ( 2 ^ j
) ) )  / 
( 2 ^ j
) )  <_  j
)
179166, 178eqbrtrd 4416 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( j J x )  <_  j
)
180179iftrued 3880 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  if ( ( j J x )  <_  j ,  ( j J x ) ,  j )  =  ( j J x ) )
181180, 166eqtrd 2505 . . . . . . 7  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  if ( ( j J x )  <_  j ,  ( j J x ) ,  j )  =  ( ( |_ `  ( ( F `  x )  x.  (
2 ^ j ) ) )  /  (
2 ^ j ) ) )
182131, 156, 1813eqtrd 2509 . . . . . 6  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( G `  n ) `
 x ) ) `
 j )  =  ( ( |_ `  ( ( F `  x )  x.  (
2 ^ j ) ) )  /  (
2 ^ j ) ) )
183119, 65, 1823brtr4d 4426 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( F `  x )  -  ( ( 1  /  2 ) ^
n ) ) ) `
 j )  <_ 
( ( n  e.  NN  |->  ( ( G `
 n ) `  x ) ) `  j ) )
184182, 172eqbrtrd 4416 . . . . 5  |-  ( ( ( ( ph  /\  x  e.  RR )  /\  ( k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  /\  j  e.  (
ZZ>= `  k ) )  ->  ( ( n  e.  NN  |->  ( ( G `  n ) `
 x ) ) `
 j )  <_ 
( F `  x
) )
18518, 20, 59, 61, 71, 84, 183, 184climsqz 13781 . . . 4  |-  ( ( ( ph  /\  x  e.  RR )  /\  (
k  e.  NN  /\  ( ( abs `  x
)  +  ( F `
 x ) )  <  k ) )  ->  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )  ~~>  ( F `
 x ) )
18617, 185rexlimddv 2875 . . 3  |-  ( (
ph  /\  x  e.  RR )  ->  ( n  e.  NN  |->  ( ( G `  n ) `
 x ) )  ~~>  ( F `  x
) )
187186ralrimiva 2809 . 2  |-  ( ph  ->  A. x  e.  RR  ( n  e.  NN  |->  ( ( G `  n ) `  x
) )  ~~>  ( F `
 x ) )
18836mptex 6152 . . . 4  |-  ( m  e.  NN  |->  ( x  e.  RR  |->  if ( x  e.  ( -u m [,] m ) ,  if ( ( m J x )  <_  m ,  ( m J x ) ,  m ) ,  0 ) ) )  e. 
_V
1894, 188eqeltri 2545 . . 3  |-  G  e. 
_V
190 feq1 5720 . . . 4  |-  ( g  =  G  ->  (
g : NN --> dom  S.1  <->  G : NN --> dom  S.1 ) )
191 fveq1 5878 . . . . . . 7  |-  ( g  =  G  ->  (
g `  n )  =  ( G `  n ) )
192191breq2d 4407 . . . . . 6  |-  ( g  =  G  ->  (
0p  oR  <_  ( g `  n )  <->  0p  oR  <_  ( G `
 n ) ) )
193 fveq1 5878 . . . . . . 7  |-  ( g  =  G  ->  (
g `  ( n  +  1 ) )  =  ( G `  ( n  +  1
) ) )
194191, 193breq12d 4408 . . . . . 6  |-  ( g  =  G  ->  (
( g `  n
)  oR  <_ 
( g `  (
n  +  1 ) )  <->  ( G `  n )  oR  <_  ( G `  ( n  +  1
) ) ) )
195192, 194anbi12d 725 . . . . 5  |-  ( g  =  G  ->  (
( 0p  oR  <_  ( g `  n )  /\  (
g `  n )  oR  <_  ( g `
 ( n  + 
1 ) ) )  <-> 
( 0p  oR  <_  ( G `  n )  /\  ( G `  n )  oR  <_  ( G `
 ( n  + 
1 ) ) ) ) )
196195ralbidv 2829 . . . 4  |-  ( g  =  G  ->  ( A. n  e.  NN  ( 0p  oR  <_  ( g `  n )  /\  (
g `  n )  oR  <_  ( g `
 ( n  + 
1 ) ) )  <->  A. n  e.  NN  ( 0p  oR  <_  ( G `  n )  /\  ( G `  n )  oR  <_  ( G `
 ( n  + 
1 ) ) ) ) )
197191fveq1d 5881 . . . . . . 7  |-  ( g  =  G  ->  (
( g `  n
) `  x )  =  ( ( G `
 n ) `  x ) )
198197mpteq2dv 4483 . . . . . 6  |-  ( g  =  G  ->  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  =  ( n  e.  NN  |->  ( ( G `  n ) `
 x ) ) )
199198breq1d 4405 . . . . 5  |-  ( g  =  G  ->  (
( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x )  <->  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )  ~~>  ( F `
 x ) ) )
200199ralbidv 2829 . . . 4  |-  ( g  =  G  ->  ( A. x  e.  RR  ( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x )  <->  A. x  e.  RR  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )  ~~>  ( F `
 x ) ) )
201190, 196, 2003anbi123d 1365 . . 3  |-  ( g  =  G  ->  (
( g : NN --> dom  S.1  /\  A. n  e.  NN  ( 0p  oR  <_  (
g `  n )  /\  ( g `  n
)  oR  <_ 
( g `  (
n  +  1 ) ) )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  ~~>  ( F `  x ) )  <->  ( G : NN --> dom  S.1  /\  A. n  e.  NN  (
0p  oR  <_  ( G `  n )  /\  ( G `  n )  oR  <_  ( G `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )  ~~>  ( F `
 x ) ) ) )
202189, 201spcev 3127 . 2  |-  ( ( G : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0p  oR  <_  ( G `  n )  /\  ( G `  n )  oR  <_  ( G `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( G `
 n ) `  x ) )  ~~>  ( F `
 x ) )  ->  E. g ( g : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0p  oR  <_  ( g `  n )  /\  (
g `  n )  oR  <_  ( g `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( g `
 n ) `  x ) )  ~~>  ( F `
 x ) ) )
2035, 7, 187, 202syl3anc 1292 1  |-  ( ph  ->  E. g ( g : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0p  oR  <_  ( g `  n )  /\  (
g `  n )  oR  <_  ( g `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( g `
 n ) `  x ) )  ~~>  ( F `
 x ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 376    /\ w3a 1007    = wceq 1452   E.wex 1671    e. wcel 1904    =/= wne 2641   A.wral 2756   E.wrex 2757   _Vcvv 3031   ifcif 3872   class class class wbr 4395    |-> cmpt 4454   dom cdm 4839   -->wf 5585   ` cfv 5589  (class class class)co 6308    |-> cmpt2 6310    oRcofr 6549   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558    + caddc 9560    x. cmul 9562   +oocpnf 9690    < clt 9693    <_ cle 9694    - cmin 9880   -ucneg 9881    / cdiv 10291   NNcn 10631   2c2 10681   NN0cn0 10893   ZZcz 10961   ZZ>=cuz 11182   [,)cico 11662   [,]cicc 11663   |_cfl 12059   ^cexp 12310   abscabs 13374    ~~> cli 13625  MblFncmbf 22651   S.1citg1 22652   0pc0p 22706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-ofr 6551  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-ioo 11664  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-rlim 13630  df-sum 13830  df-rest 15399  df-topgen 15420  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-top 19998  df-bases 19999  df-topon 20000  df-cmp 20479  df-ovol 22494  df-vol 22496  df-mbf 22656  df-itg1 22657  df-0p 22707
This theorem is referenced by:  mbfi1fseq  22758
  Copyright terms: Public domain W3C validator