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

Theorem mbfi1fseqlem4 19602
Description: Lemma for mbfi1fseq 19605. This lemma is not as interesting as it is long - it is simply checking that  G is in fact a sequence of simple functions, by verifying that its range is in  ( 0 ... n 2 ^ n
)  /  ( 2 ^ n ) (which is to say, the numbers from  0 to  n in increments of  1  / 
( 2 ^ n
)), and also that the preimage of each point  k is measurable, because it is equal to  ( -u n [,] n )  i^i  ( `' F " ( k [,) k  +  1  /  ( 2 ^ n ) ) ) for  k  <  n and  ( -u n [,] n
)  i^i  ( `' F " ( k [,) 
+oo ) ) for  k  =  n. (Contributed by Mario Carneiro, 16-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
mbfi1fseqlem4  |-  ( ph  ->  G : NN --> dom  S.1 )
Distinct variable groups:    x, m, y, F    x, G    m, J    ph, m, x, y
Allowed substitution hints:    G( y, m)    J( x, y)

Proof of Theorem mbfi1fseqlem4
Dummy variables  k  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 9073 . . . . 5  |-  RR  e.  _V
21mptex 5958 . . . 4  |-  ( x  e.  RR  |->  if ( x  e.  ( -u m [,] m ) ,  if ( ( m J x )  <_  m ,  ( m J x ) ,  m ) ,  0 ) )  e.  _V
3 mbfi1fseq.4 . . . 4  |-  G  =  ( m  e.  NN  |->  ( x  e.  RR  |->  if ( x  e.  (
-u m [,] m
) ,  if ( ( m J x )  <_  m , 
( m J x ) ,  m ) ,  0 ) ) )
42, 3fnmpti 5565 . . 3  |-  G  Fn  NN
54a1i 11 . 2  |-  ( ph  ->  G  Fn  NN )
6 mbfi1fseq.1 . . . . . 6  |-  ( ph  ->  F  e. MblFn )
7 mbfi1fseq.2 . . . . . 6  |-  ( ph  ->  F : RR --> ( 0 [,)  +oo ) )
8 mbfi1fseq.3 . . . . . 6  |-  J  =  ( m  e.  NN ,  y  e.  RR  |->  ( ( |_ `  ( ( F `  y )  x.  (
2 ^ m ) ) )  /  (
2 ^ m ) ) )
96, 7, 8, 3mbfi1fseqlem3 19601 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( G `
 n ) : RR --> ran  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) ) )
10 elfznn0 11075 . . . . . . . . 9  |-  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  ->  m  e.  NN0 )
1110nn0red 10267 . . . . . . . 8  |-  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  ->  m  e.  RR )
12 2nn 10125 . . . . . . . . . 10  |-  2  e.  NN
13 nnnn0 10220 . . . . . . . . . 10  |-  ( n  e.  NN  ->  n  e.  NN0 )
14 nnexpcl 11386 . . . . . . . . . 10  |-  ( ( 2  e.  NN  /\  n  e.  NN0 )  -> 
( 2 ^ n
)  e.  NN )
1512, 13, 14sylancr 645 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
2 ^ n )  e.  NN )
1615adantl 453 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2 ^ n )  e.  NN )
17 nndivre 10027 . . . . . . . 8  |-  ( ( m  e.  RR  /\  ( 2 ^ n
)  e.  NN )  ->  ( m  / 
( 2 ^ n
) )  e.  RR )
1811, 16, 17syl2anr 465 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
m  /  ( 2 ^ n ) )  e.  RR )
19 eqid 2435 . . . . . . 7  |-  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  |->  ( m  /  ( 2 ^ n ) ) )  =  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) )
2018, 19fmptd 5885 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  |->  ( m  /  ( 2 ^ n ) ) ) : ( 0 ... ( n  x.  (
2 ^ n ) ) ) --> RR )
21 frn 5589 . . . . . 6  |-  ( ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) ) : ( 0 ... ( n  x.  ( 2 ^ n
) ) ) --> RR 
->  ran  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) )  C_  RR )
2220, 21syl 16 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  C_  RR )
23 fss 5591 . . . . 5  |-  ( ( ( G `  n
) : RR --> ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  /\  ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  C_  RR )  ->  ( G `  n
) : RR --> RR )
249, 22, 23syl2anc 643 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ( G `
 n ) : RR --> RR )
25 fzfid 11304 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  e. 
Fin )
26 ffn 5583 . . . . . . . 8  |-  ( ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) ) : ( 0 ... ( n  x.  ( 2 ^ n
) ) ) --> RR 
->  ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n ) ) ) 
|->  ( m  /  (
2 ^ n ) ) )  Fn  (
0 ... ( n  x.  ( 2 ^ n
) ) ) )
2720, 26syl 16 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  |->  ( m  /  ( 2 ^ n ) ) )  Fn  ( 0 ... ( n  x.  (
2 ^ n ) ) ) )
28 dffn4 5651 . . . . . . 7  |-  ( ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  Fn  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  <->  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) ) : ( 0 ... (
n  x.  ( 2 ^ n ) ) ) -onto-> ran  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) ) )
2927, 28sylib 189 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  |->  ( m  /  ( 2 ^ n ) ) ) : ( 0 ... ( n  x.  (
2 ^ n ) ) ) -onto-> ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) ) )
30 fofi 7384 . . . . . 6  |-  ( ( ( 0 ... (
n  x.  ( 2 ^ n ) ) )  e.  Fin  /\  ( m  e.  (
0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) ) : ( 0 ... ( n  x.  ( 2 ^ n
) ) ) -onto-> ran  ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n ) ) ) 
|->  ( m  /  (
2 ^ n ) ) ) )  ->  ran  ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n ) ) ) 
|->  ( m  /  (
2 ^ n ) ) )  e.  Fin )
3125, 29, 30syl2anc 643 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  e.  Fin )
32 frn 5589 . . . . . 6  |-  ( ( G `  n ) : RR --> ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  ->  ran  ( G `
 n )  C_  ran  ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n ) ) ) 
|->  ( m  /  (
2 ^ n ) ) ) )
339, 32syl 16 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ran  ( G `  n )  C_ 
ran  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) ) )
34 ssfi 7321 . . . . 5  |-  ( ( ran  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) )  e. 
Fin  /\  ran  ( G `
 n )  C_  ran  ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n ) ) ) 
|->  ( m  /  (
2 ^ n ) ) ) )  ->  ran  ( G `  n
)  e.  Fin )
3531, 33, 34syl2anc 643 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ran  ( G `  n )  e.  Fin )
366, 7, 8, 3mbfi1fseqlem2 19600 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  ->  ( G `  n )  =  ( x  e.  RR  |->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 ) ) )
3736fveq1d 5722 . . . . . . . . . . . . 13  |-  ( n  e.  NN  ->  (
( G `  n
) `  x )  =  ( ( x  e.  RR  |->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 ) ) `  x
) )
3837ad2antlr 708 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( G `  n
) `  x )  =  ( ( x  e.  RR  |->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 ) ) `  x
) )
39 simpr 448 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  x  e.  RR )
40 ovex 6098 . . . . . . . . . . . . . . 15  |-  ( n J x )  e. 
_V
41 vex 2951 . . . . . . . . . . . . . . 15  |-  n  e. 
_V
4240, 41ifex 3789 . . . . . . . . . . . . . 14  |-  if ( ( n J x )  <_  n , 
( n J x ) ,  n )  e.  _V
43 c0ex 9077 . . . . . . . . . . . . . 14  |-  0  e.  _V
4442, 43ifex 3789 . . . . . . . . . . . . 13  |-  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  e.  _V
45 eqid 2435 . . . . . . . . . . . . . 14  |-  ( x  e.  RR  |->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 ) )  =  ( x  e.  RR  |->  if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 ) )
4645fvmpt2 5804 . . . . . . . . . . . . 13  |-  ( ( x  e.  RR  /\  if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 )  e. 
_V )  ->  (
( x  e.  RR  |->  if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 ) ) `
 x )  =  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 ) )
4739, 44, 46sylancl 644 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( x  e.  RR  |->  if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 ) ) `
 x )  =  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 ) )
4838, 47eqtrd 2467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( G `  n
) `  x )  =  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 ) )
4948adantlr 696 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( G `  n ) `  x
)  =  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 ) )
5049eqeq1d 2443 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( ( G `
 n ) `  x )  =  k  <-> 
if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  =  k ) )
51 eldifsni 3920 . . . . . . . . . . . . 13  |-  ( k  e.  ( ran  ( G `  n )  \  { 0 } )  ->  k  =/=  0
)
5251ad2antlr 708 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  k  =/=  0 )
53 neeq1 2606 . . . . . . . . . . . 12  |-  ( if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 )  =  k  ->  ( if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  =/=  0  <->  k  =/=  0 ) )
5452, 53syl5ibrcom 214 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  =  k  ->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  =/=  0
) )
55 iffalse 3738 . . . . . . . . . . . 12  |-  ( -.  x  e.  ( -u n [,] n )  ->  if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 )  =  0 )
5655necon1ai 2640 . . . . . . . . . . 11  |-  ( if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 )  =/=  0  ->  x  e.  ( -u n [,] n
) )
5754, 56syl6 31 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  =  k  ->  x  e.  ( -u n [,] n ) ) )
5857pm4.71rd 617 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  =  k  <->  ( x  e.  ( -u n [,] n )  /\  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  =  k ) ) )
59 iftrue 3737 . . . . . . . . . . . 12  |-  ( x  e.  ( -u n [,] n )  ->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  =  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) )
6059eqeq1d 2443 . . . . . . . . . . 11  |-  ( x  e.  ( -u n [,] n )  ->  ( if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 )  =  k  <->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  k ) )
61 simpllr 736 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  n  e.  NN )
6261nnred 10007 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  n  e.  RR )
6362adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  n  e.  RR )
64 0re 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  0  e.  RR
65 pnfxr 10705 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  +oo  e.  RR*
66 icossre 10983 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 0  e.  RR  /\  +oo 
e.  RR* )  ->  (
0 [,)  +oo )  C_  RR )
6764, 65, 66mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0 [,)  +oo )  C_  RR
68 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( m  e.  NN  /\  y  e.  RR )  ->  y  e.  RR )
69 ffvelrn 5860 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  y  e.  RR )  ->  ( F `  y )  e.  ( 0 [,)  +oo ) )
707, 68, 69syl2an 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( F `  y
)  e.  ( 0 [,)  +oo ) )
7167, 70sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( F `  y
)  e.  RR )
72 nnnn0 10220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( m  e.  NN  ->  m  e.  NN0 )
73 nnexpcl 11386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2  e.  NN  /\  m  e.  NN0 )  -> 
( 2 ^ m
)  e.  NN )
7412, 72, 73sylancr 645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( m  e.  NN  ->  (
2 ^ m )  e.  NN )
7574ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( 2 ^ m
)  e.  NN )
7675nnred 10007 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( 2 ^ m
)  e.  RR )
7771, 76remulcld 9108 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( ( F `  y )  x.  (
2 ^ m ) )  e.  RR )
78 reflcl 11197 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F `  y
)  x.  ( 2 ^ m ) )  e.  RR  ->  ( |_ `  ( ( F `
 y )  x.  ( 2 ^ m
) ) )  e.  RR )
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( |_ `  (
( F `  y
)  x.  ( 2 ^ m ) ) )  e.  RR )
8079, 75nndivred 10040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( m  e.  NN  /\  y  e.  RR ) )  -> 
( ( |_ `  ( ( F `  y )  x.  (
2 ^ m ) ) )  /  (
2 ^ m ) )  e.  RR )
8180ralrimivva 2790 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  A. m  e.  NN  A. y  e.  RR  (
( |_ `  (
( F `  y
)  x.  ( 2 ^ m ) ) )  /  ( 2 ^ m ) )  e.  RR )
828fmpt2 6410 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. m  e.  NN  A. y  e.  RR  ( ( |_
`  ( ( F `
 y )  x.  ( 2 ^ m
) ) )  / 
( 2 ^ m
) )  e.  RR  <->  J : ( NN  X.  RR ) --> RR )
8381, 82sylib 189 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  J : ( NN 
X.  RR ) --> RR )
84 fovrn 6208 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( J : ( NN 
X.  RR ) --> RR 
/\  n  e.  NN  /\  x  e.  RR )  ->  ( n J x )  e.  RR )
8583, 84syl3an1 1217 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN  /\  x  e.  RR )  ->  ( n J x )  e.  RR )
86853expa 1153 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
n J x )  e.  RR )
8786adantlr 696 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n J x )  e.  RR )
8887adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( n J x )  e.  RR )
89 lemin 10771 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  RR  /\  ( n J x )  e.  RR  /\  n  e.  RR )  ->  ( n  <_  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  <->  ( n  <_ 
( n J x )  /\  n  <_  n ) ) )
9063, 88, 63, 89syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( n  <_  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  <->  ( n  <_  ( n J x )  /\  n  <_  n ) ) )
91 ifcl 3767 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n J x )  e.  RR  /\  n  e.  RR )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  e.  RR )
9288, 63, 91syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  if (
( n J x )  <_  n , 
( n J x ) ,  n )  e.  RR )
9392, 63letri3d 9207 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  n  <->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  <_  n  /\  n  <_  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ) ) )
94 simpr 448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  k  =  n )
9594eqeq2d 2446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  if (
( n J x )  <_  n , 
( n J x ) ,  n )  =  n ) )
96 min2 10769 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n J x )  e.  RR  /\  n  e.  RR )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  <_  n
)
9788, 63, 96syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  if (
( n J x )  <_  n , 
( n J x ) ,  n )  <_  n )
9897biantrurd 495 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( n  <_  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  <->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  <_  n  /\  n  <_  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ) ) )
9993, 95, 983bitr4d 277 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  n  <_  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ) )
10063leidd 9585 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  n  <_  n )
101100biantrud 494 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( n  <_  ( n J x )  <->  ( n  <_ 
( n J x )  /\  n  <_  n ) ) )
10290, 99, 1013bitr4d 277 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  n  <_  ( n J x ) ) )
103 breq1 4207 . . . . . . . . . . . . . . 15  |-  ( k  =  n  ->  (
k  <_  ( F `  x )  <->  n  <_  ( F `  x ) ) )
1047adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  n  e.  NN )  ->  F : RR
--> ( 0 [,)  +oo ) )
105104ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  x )  e.  ( 0 [,)  +oo ) )
106 elrege0 10999 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( F `  x )  e.  RR  /\  0  <_ 
( F `  x
) ) )
107105, 106sylib 189 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( F `  x
)  e.  RR  /\  0  <_  ( F `  x ) ) )
108107simpld 446 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
109108adantlr 696 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( F `  x
)  e.  RR )
11061, 15syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( 2 ^ n
)  e.  NN )
111110nnred 10007 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( 2 ^ n
)  e.  RR )
112109, 111remulcld 9108 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  x.  (
2 ^ n ) )  e.  RR )
113 reflcl 11197 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  x
)  x.  ( 2 ^ n ) )  e.  RR  ->  ( |_ `  ( ( F `
 x )  x.  ( 2 ^ n
) ) )  e.  RR )
114112, 113syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( |_ `  (
( F `  x
)  x.  ( 2 ^ n ) ) )  e.  RR )
115110nngt0d 10035 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  0  <  ( 2 ^ n ) )
116 lemuldiv 9881 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  RR  /\  ( |_ `  ( ( F `  x )  x.  ( 2 ^ n ) ) )  e.  RR  /\  (
( 2 ^ n
)  e.  RR  /\  0  <  ( 2 ^ n ) ) )  ->  ( ( n  x.  ( 2 ^ n ) )  <_ 
( |_ `  (
( F `  x
)  x.  ( 2 ^ n ) ) )  <->  n  <_  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) ) )
11762, 114, 111, 115, 116syl112anc 1188 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( n  x.  ( 2 ^ n
) )  <_  ( |_ `  ( ( F `
 x )  x.  ( 2 ^ n
) ) )  <->  n  <_  ( ( |_ `  (
( F `  x
)  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) ) )
118 lemul1 9854 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  RR  /\  ( F `  x )  e.  RR  /\  (
( 2 ^ n
)  e.  RR  /\  0  <  ( 2 ^ n ) ) )  ->  ( n  <_ 
( F `  x
)  <->  ( n  x.  ( 2 ^ n
) )  <_  (
( F `  x
)  x.  ( 2 ^ n ) ) ) )
11962, 109, 111, 115, 118syl112anc 1188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n  <_  ( F `  x )  <->  ( n  x.  ( 2 ^ n ) )  <_  ( ( F `
 x )  x.  ( 2 ^ n
) ) ) )
120 nnmulcl 10015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  NN  /\  ( 2 ^ n
)  e.  NN )  ->  ( n  x.  ( 2 ^ n
) )  e.  NN )
12115, 120mpdan 650 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  NN  ->  (
n  x.  ( 2 ^ n ) )  e.  NN )
12261, 121syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n  x.  (
2 ^ n ) )  e.  NN )
123122nnzd 10366 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n  x.  (
2 ^ n ) )  e.  ZZ )
124 flge 11206 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( F `  x )  x.  (
2 ^ n ) )  e.  RR  /\  ( n  x.  (
2 ^ n ) )  e.  ZZ )  ->  ( ( n  x.  ( 2 ^ n ) )  <_ 
( ( F `  x )  x.  (
2 ^ n ) )  <->  ( n  x.  ( 2 ^ n
) )  <_  ( |_ `  ( ( F `
 x )  x.  ( 2 ^ n
) ) ) ) )
125112, 123, 124syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( n  x.  ( 2 ^ n
) )  <_  (
( F `  x
)  x.  ( 2 ^ n ) )  <-> 
( n  x.  (
2 ^ n ) )  <_  ( |_ `  ( ( F `  x )  x.  (
2 ^ n ) ) ) ) )
126119, 125bitrd 245 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n  <_  ( F `  x )  <->  ( n  x.  ( 2 ^ n ) )  <_  ( |_ `  ( ( F `  x )  x.  (
2 ^ n ) ) ) ) )
127 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  x  e.  RR )
128 simpr 448 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  =  n  /\  y  =  x )  ->  y  =  x )
129128fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  =  n  /\  y  =  x )  ->  ( F `  y
)  =  ( F `
 x ) )
130 simpl 444 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  =  n  /\  y  =  x )  ->  m  =  n )
131130oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  =  n  /\  y  =  x )  ->  ( 2 ^ m
)  =  ( 2 ^ n ) )
132129, 131oveq12d 6091 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( m  =  n  /\  y  =  x )  ->  ( ( F `  y )  x.  (
2 ^ m ) )  =  ( ( F `  x )  x.  ( 2 ^ n ) ) )
133132fveq2d 5724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  =  n  /\  y  =  x )  ->  ( |_ `  (
( F `  y
)  x.  ( 2 ^ m ) ) )  =  ( |_
`  ( ( F `
 x )  x.  ( 2 ^ n
) ) ) )
134133, 131oveq12d 6091 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  =  n  /\  y  =  x )  ->  ( ( |_ `  ( ( F `  y )  x.  (
2 ^ m ) ) )  /  (
2 ^ m ) )  =  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) )
135 ovex 6098 . . . . . . . . . . . . . . . . . . 19  |-  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) )  e. 
_V
136134, 8, 135ovmpt2a 6196 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  NN  /\  x  e.  RR )  ->  ( n J x )  =  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) )
13761, 127, 136syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n J x )  =  ( ( |_ `  ( ( F `  x )  x.  ( 2 ^ n ) ) )  /  ( 2 ^ n ) ) )
138137breq2d 4216 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n  <_  (
n J x )  <-> 
n  <_  ( ( |_ `  ( ( F `
 x )  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) ) ) )
139117, 126, 1383bitr4d 277 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( n  <_  ( F `  x )  <->  n  <_  ( n J x ) ) )
140103, 139sylan9bbr 682 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( k  <_  ( F `  x
)  <->  n  <_  ( n J x ) ) )
141127adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  x  e.  RR )
142 iftrue 3737 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  =  RR )
143142adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  if (
k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  =  RR )
144141, 143eleqtrrd 2512 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  x  e.  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) )
145144biantrurd 495 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( k  <_  ( F `  x
)  <->  ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  /\  k  <_  ( F `  x
) ) ) )
146102, 140, 1453bitr2d 273 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =  n )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  /\  k  <_  ( F `  x
) ) ) )
14733ssdifssd 3477 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( ran  ( G `  n
)  \  { 0 } )  C_  ran  ( m  e.  (
0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) ) )
148147sselda 3340 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  k  e.  ran  ( m  e.  ( 0 ... ( n  x.  ( 2 ^ n ) ) ) 
|->  ( m  /  (
2 ^ n ) ) ) )
14919rnmpt 5108 . . . . . . . . . . . . . . . . . . . . 21  |-  ran  (
m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) )  |->  ( m  /  ( 2 ^ n ) ) )  =  { k  |  E. m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) k  =  ( m  /  ( 2 ^ n ) ) }
150149abeq2i 2542 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ran  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  |->  ( m  /  ( 2 ^ n ) ) )  <->  E. m  e.  (
0 ... ( n  x.  ( 2 ^ n
) ) ) k  =  ( m  / 
( 2 ^ n
) ) )
151 elfzelz 11051 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  ->  m  e.  ZZ )
152151adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  m  e.  ZZ )
153152zcnd 10368 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  m  e.  CC )
15415ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
2 ^ n )  e.  NN )
155154nncnd 10008 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
2 ^ n )  e.  CC )
156154nnne0d 10036 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
2 ^ n )  =/=  0 )
157153, 155, 156divcan1d 9783 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
( m  /  (
2 ^ n ) )  x.  ( 2 ^ n ) )  =  m )
158157, 152eqeltrd 2509 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
( m  /  (
2 ^ n ) )  x.  ( 2 ^ n ) )  e.  ZZ )
159 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( m  / 
( 2 ^ n
) )  ->  (
k  x.  ( 2 ^ n ) )  =  ( ( m  /  ( 2 ^ n ) )  x.  ( 2 ^ n
) ) )
160159eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( m  / 
( 2 ^ n
) )  ->  (
( k  x.  (
2 ^ n ) )  e.  ZZ  <->  ( (
m  /  ( 2 ^ n ) )  x.  ( 2 ^ n ) )  e.  ZZ ) )
161158, 160syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) ) )  ->  (
k  =  ( m  /  ( 2 ^ n ) )  -> 
( k  x.  (
2 ^ n ) )  e.  ZZ ) )
162161rexlimdva 2822 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  ( E. m  e.  ( 0 ... ( n  x.  ( 2 ^ n
) ) ) k  =  ( m  / 
( 2 ^ n
) )  ->  (
k  x.  ( 2 ^ n ) )  e.  ZZ ) )
163150, 162syl5bi 209 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( k  e.  ran  ( m  e.  ( 0 ... ( n  x.  (
2 ^ n ) ) )  |->  ( m  /  ( 2 ^ n ) ) )  ->  ( k  x.  ( 2 ^ n
) )  e.  ZZ ) )
164163imp 419 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ran  ( m  e.  ( 0 ... (
n  x.  ( 2 ^ n ) ) )  |->  ( m  / 
( 2 ^ n
) ) ) )  ->  ( k  x.  ( 2 ^ n
) )  e.  ZZ )
165148, 164syldan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( k  x.  ( 2 ^ n
) )  e.  ZZ )
166165adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( k  x.  (
2 ^ n ) )  e.  ZZ )
167 flbi 11215 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( F `  x )  x.  (
2 ^ n ) )  e.  RR  /\  ( k  x.  (
2 ^ n ) )  e.  ZZ )  ->  ( ( |_
`  ( ( F `
 x )  x.  ( 2 ^ n
) ) )  =  ( k  x.  (
2 ^ n ) )  <->  ( ( k  x.  ( 2 ^ n ) )  <_ 
( ( F `  x )  x.  (
2 ^ n ) )  /\  ( ( F `  x )  x.  ( 2 ^ n ) )  < 
( ( k  x.  ( 2 ^ n
) )  +  1 ) ) ) )
168112, 166, 167syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( |_ `  ( ( F `  x )  x.  (
2 ^ n ) ) )  =  ( k  x.  ( 2 ^ n ) )  <-> 
( ( k  x.  ( 2 ^ n
) )  <_  (
( F `  x
)  x.  ( 2 ^ n ) )  /\  ( ( F `
 x )  x.  ( 2 ^ n
) )  <  (
( k  x.  (
2 ^ n ) )  +  1 ) ) ) )
169168adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( ( |_ `  ( ( F `
 x )  x.  ( 2 ^ n
) ) )  =  ( k  x.  (
2 ^ n ) )  <->  ( ( k  x.  ( 2 ^ n ) )  <_ 
( ( F `  x )  x.  (
2 ^ n ) )  /\  ( ( F `  x )  x.  ( 2 ^ n ) )  < 
( ( k  x.  ( 2 ^ n
) )  +  1 ) ) ) )
170 neeq1 2606 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  -> 
( if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =/=  n  <->  k  =/=  n
) )
171170biimparc 474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =/=  n )
172 iffalse 3738 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  ( n J x )  <_  n  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  n )
173172necon1ai 2640 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =/=  n  -> 
( n J x )  <_  n )
174171, 173syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  ( n J x )  <_  n
)
175 iftrue 3737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( n J x )  <_  n  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  ( n J x ) )
176174, 175syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  ( n J x ) )
177 simpr 448 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  k )
178176, 177eqtr3d 2469 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  ( n J x )  =  k )
179178, 174eqbrtrrd 4226 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  k  <_  n
)
180179, 178jca 519 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  =/=  n  /\  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k )  ->  ( k  <_  n  /\  ( n J x )  =  k ) )
181180ex 424 . . . . . . . . . . . . . . . . 17  |-  ( k  =/=  n  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  -> 
( k  <_  n  /\  ( n J x )  =  k ) ) )
182 breq1 4207 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n J x )  =  k  ->  (
( n J x )  <_  n  <->  k  <_  n ) )
183182biimparc 474 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  <_  n  /\  ( n J x )  =  k )  ->  ( n J x )  <_  n
)
184183, 175syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  <_  n  /\  ( n J x )  =  k )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  ( n J x ) )
185 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  <_  n  /\  ( n J x )  =  k )  ->  ( n J x )  =  k )
186184, 185eqtrd 2467 . . . . . . . . . . . . . . . . 17  |-  ( ( k  <_  n  /\  ( n J x )  =  k )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  k )
187181, 186impbid1 195 . . . . . . . . . . . . . . . 16  |-  ( k  =/=  n  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  ( k  <_  n  /\  ( n J x )  =  k ) ) )
188187adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  ( k  <_  n  /\  ( n J x )  =  k ) ) )
189 eldifi 3461 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ran  ( G `  n )  \  { 0 } )  ->  k  e.  ran  ( G `  n ) )
190 nnre 9999 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  NN  ->  n  e.  RR )
191190ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  n  e.  RR )
19286, 191, 96syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  <_  n )
19313ad2antlr 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  n  e.  NN0 )
194193nn0ge0d 10269 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  0  <_  n )
195 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  <_  n  <->  if (
x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  <_  n )
)
196 breq1 4207 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0  =  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  ->  ( 0  <_  n 
<->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  <_  n ) )
197195, 196ifboth 3762 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  <_  n  /\  0  <_  n )  ->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n
) ,  0 )  <_  n )
198192, 194, 197syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  <_  n
)
19948, 198eqbrtrd 4224 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  x  e.  RR )  ->  (
( G `  n
) `  x )  <_  n )
200199ralrimiva 2781 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  A. x  e.  RR  ( ( G `
 n ) `  x )  <_  n
)
201 ffn 5583 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( G `  n ) : RR --> RR  ->  ( G `  n )  Fn  RR )
20224, 201syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( G `
 n )  Fn  RR )
203 breq1 4207 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( ( G `
 n ) `  x )  ->  (
k  <_  n  <->  ( ( G `  n ) `  x )  <_  n
) )
204203ralrn 5865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( G `  n )  Fn  RR  ->  ( A. k  e.  ran  ( G `  n ) k  <_  n  <->  A. x  e.  RR  ( ( G `
 n ) `  x )  <_  n
) )
205202, 204syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  ( A. k  e.  ran  ( G `
 n ) k  <_  n  <->  A. x  e.  RR  ( ( G `
 n ) `  x )  <_  n
) )
206200, 205mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  A. k  e.  ran  ( G `  n ) k  <_  n )
207206r19.21bi 2796 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ran  ( G `  n ) )  -> 
k  <_  n )
208189, 207sylan2 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  k  <_  n )
209208ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  k  <_  n )
210209biantrurd 495 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( (
n J x )  =  k  <->  ( k  <_  n  /\  ( n J x )  =  k ) ) )
211137eqeq1d 2443 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( n J x )  =  k  <-> 
( ( |_ `  ( ( F `  x )  x.  (
2 ^ n ) ) )  /  (
2 ^ n ) )  =  k ) )
212114recnd 9106 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( |_ `  (
( F `  x
)  x.  ( 2 ^ n ) ) )  e.  CC )
21333, 22sstrd 3350 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  n  e.  NN )  ->  ran  ( G `  n )  C_  RR )
214213ssdifssd 3477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( ran  ( G `  n
)  \  { 0 } )  C_  RR )
215214sselda 3340 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  k  e.  RR )
216215adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  k  e.  RR )
217216recnd 9106 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  k  e.  CC )
218110nncnd 10008 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( 2 ^ n
)  e.  CC )
219110nnne0d 10036 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( 2 ^ n
)  =/=  0 )
220212, 217, 218, 219divmul3d 9816 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( ( |_
`  ( ( F `
 x )  x.  ( 2 ^ n
) ) )  / 
( 2 ^ n
) )  =  k  <-> 
( |_ `  (
( F `  x
)  x.  ( 2 ^ n ) ) )  =  ( k  x.  ( 2 ^ n ) ) ) )
221211, 220bitrd 245 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( n J x )  =  k  <-> 
( |_ `  (
( F `  x
)  x.  ( 2 ^ n ) ) )  =  ( k  x.  ( 2 ^ n ) ) ) )
222221adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( (
n J x )  =  k  <->  ( |_ `  ( ( F `  x )  x.  (
2 ^ n ) ) )  =  ( k  x.  ( 2 ^ n ) ) ) )
223188, 210, 2223bitr2d 273 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  ( |_ `  ( ( F `  x )  x.  (
2 ^ n ) ) )  =  ( k  x.  ( 2 ^ n ) ) ) )
224 ifnefalse 3739 . . . . . . . . . . . . . . . . . 18  |-  ( k  =/=  n  ->  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  =  ( `' F " (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )
225224eleq2d 2502 . . . . . . . . . . . . . . . . 17  |-  ( k  =/=  n  ->  (
x  e.  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  <-> 
x  e.  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) )
226110nnrecred 10037 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( 1  /  (
2 ^ n ) )  e.  RR )
227216, 226readdcld 9107 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( k  +  ( 1  /  ( 2 ^ n ) ) )  e.  RR )
228227rexrd 9126 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( k  +  ( 1  /  ( 2 ^ n ) ) )  e.  RR* )
229 elioomnf 10991 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  +  ( 1  /  ( 2 ^ n ) ) )  e.  RR*  ->  ( ( F `  x )  e.  (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) )  <->  ( ( F `  x )  e.  RR  /\  ( F `
 x )  < 
( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )
230228, 229syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  e.  ( 
-oo (,) ( k  +  ( 1  /  (
2 ^ n ) ) ) )  <->  ( ( F `  x )  e.  RR  /\  ( F `
 x )  < 
( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )
231104ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  F : RR --> ( 0 [,)  +oo ) )
232 ffn 5583 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( F : RR --> ( 0 [,)  +oo )  ->  F  Fn  RR )
233231, 232syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  F  Fn  RR )
234 elpreima 5842 . . . . . . . . . . . . . . . . . . . . 21  |-  ( F  Fn  RR  ->  (
x  e.  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) )
235233, 234syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) )
236127biantrurd 495 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  e.  ( 
-oo (,) ( k  +  ( 1  /  (
2 ^ n ) ) ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) )
237235, 236bitr4d 248 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) )  <->  ( F `  x )  e.  ( 
-oo (,) ( k  +  ( 1  /  (
2 ^ n ) ) ) ) ) )
238109biantrurd 495 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  <  (
k  +  ( 1  /  ( 2 ^ n ) ) )  <-> 
( ( F `  x )  e.  RR  /\  ( F `  x
)  <  ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )
239230, 237, 2383bitr4d 277 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) )  <->  ( F `  x )  <  (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) )
240 ltmul1 9852 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  x
)  e.  RR  /\  ( k  +  ( 1  /  ( 2 ^ n ) ) )  e.  RR  /\  ( ( 2 ^ n )  e.  RR  /\  0  <  ( 2 ^ n ) ) )  ->  ( ( F `  x )  <  ( k  +  ( 1  /  ( 2 ^ n ) ) )  <->  ( ( F `
 x )  x.  ( 2 ^ n
) )  <  (
( k  +  ( 1  /  ( 2 ^ n ) ) )  x.  ( 2 ^ n ) ) ) )
241109, 227, 111, 115, 240syl112anc 1188 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  <  (
k  +  ( 1  /  ( 2 ^ n ) ) )  <-> 
( ( F `  x )  x.  (
2 ^ n ) )  <  ( ( k  +  ( 1  /  ( 2 ^ n ) ) )  x.  ( 2 ^ n ) ) ) )
242226recnd 9106 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( 1  /  (
2 ^ n ) )  e.  CC )
243217, 242, 218adddird 9105 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( k  +  ( 1  /  (
2 ^ n ) ) )  x.  (
2 ^ n ) )  =  ( ( k  x.  ( 2 ^ n ) )  +  ( ( 1  /  ( 2 ^ n ) )  x.  ( 2 ^ n
) ) ) )
244218, 219recid2d 9778 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( 1  / 
( 2 ^ n
) )  x.  (
2 ^ n ) )  =  1 )
245244oveq2d 6089 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( k  x.  ( 2 ^ n
) )  +  ( ( 1  /  (
2 ^ n ) )  x.  ( 2 ^ n ) ) )  =  ( ( k  x.  ( 2 ^ n ) )  +  1 ) )
246243, 245eqtrd 2467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( k  +  ( 1  /  (
2 ^ n ) ) )  x.  (
2 ^ n ) )  =  ( ( k  x.  ( 2 ^ n ) )  +  1 ) )
247246breq2d 4216 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( ( F `
 x )  x.  ( 2 ^ n
) )  <  (
( k  +  ( 1  /  ( 2 ^ n ) ) )  x.  ( 2 ^ n ) )  <-> 
( ( F `  x )  x.  (
2 ^ n ) )  <  ( ( k  x.  ( 2 ^ n ) )  +  1 ) ) )
248239, 241, 2473bitrd 271 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) )  <->  ( ( F `  x )  x.  ( 2 ^ n
) )  <  (
( k  x.  (
2 ^ n ) )  +  1 ) ) )
249225, 248sylan9bbr 682 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  <->  ( ( F `  x )  x.  ( 2 ^ n
) )  <  (
( k  x.  (
2 ^ n ) )  +  1 ) ) )
250 lemul1 9854 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  RR  /\  ( F `  x )  e.  RR  /\  (
( 2 ^ n
)  e.  RR  /\  0  <  ( 2 ^ n ) ) )  ->  ( k  <_ 
( F `  x
)  <->  ( k  x.  ( 2 ^ n
) )  <_  (
( F `  x
)  x.  ( 2 ^ n ) ) ) )
251216, 109, 111, 115, 250syl112anc 1188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( k  <_  ( F `  x )  <->  ( k  x.  ( 2 ^ n ) )  <_  ( ( F `
 x )  x.  ( 2 ^ n
) ) ) )
252251adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( k  <_  ( F `  x
)  <->  ( k  x.  ( 2 ^ n
) )  <_  (
( F `  x
)  x.  ( 2 ^ n ) ) ) )
253249, 252anbi12d 692 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( (
x  e.  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  /\  k  <_  ( F `  x )
)  <->  ( ( ( F `  x )  x.  ( 2 ^ n ) )  < 
( ( k  x.  ( 2 ^ n
) )  +  1 )  /\  ( k  x.  ( 2 ^ n ) )  <_ 
( ( F `  x )  x.  (
2 ^ n ) ) ) ) )
254 ancom 438 . . . . . . . . . . . . . . 15  |-  ( ( ( ( F `  x )  x.  (
2 ^ n ) )  <  ( ( k  x.  ( 2 ^ n ) )  +  1 )  /\  ( k  x.  (
2 ^ n ) )  <_  ( ( F `  x )  x.  ( 2 ^ n
) ) )  <->  ( (
k  x.  ( 2 ^ n ) )  <_  ( ( F `
 x )  x.  ( 2 ^ n
) )  /\  (
( F `  x
)  x.  ( 2 ^ n ) )  <  ( ( k  x.  ( 2 ^ n ) )  +  1 ) ) )
255253, 254syl6bb 253 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( (
x  e.  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  /\  k  <_  ( F `  x )
)  <->  ( ( k  x.  ( 2 ^ n ) )  <_ 
( ( F `  x )  x.  (
2 ^ n ) )  /\  ( ( F `  x )  x.  ( 2 ^ n ) )  < 
( ( k  x.  ( 2 ^ n
) )  +  1 ) ) ) )
256169, 223, 2553bitr4d 277 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  k  =/=  n
)  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n
)  =  k  <->  ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  /\  k  <_  ( F `  x
) ) ) )
257146, 256pm2.61dane 2676 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  k  <->  ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  /\  k  <_  ( F `  x
) ) ) )
258 eldif 3322 . . . . . . . . . . . . 13  |-  ( x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) )  <->  ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  /\  -.  x  e.  ( `' F " (  -oo (,) k ) ) ) )
259216rexrd 9126 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  k  e.  RR* )
260 elioomnf 10991 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  RR*  ->  ( ( F `  x )  e.  (  -oo (,) k )  <->  ( ( F `  x )  e.  RR  /\  ( F `
 x )  < 
k ) ) )
261259, 260syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  e.  ( 
-oo (,) k )  <->  ( ( F `  x )  e.  RR  /\  ( F `
 x )  < 
k ) ) )
262 elpreima 5842 . . . . . . . . . . . . . . . . . . 19  |-  ( F  Fn  RR  ->  (
x  e.  ( `' F " (  -oo (,) k ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  (  -oo (,) k
) ) ) )
263233, 262syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) k ) )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  (  -oo (,) k
) ) ) )
264127biantrurd 495 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  e.  ( 
-oo (,) k )  <->  ( x  e.  RR  /\  ( F `
 x )  e.  (  -oo (,) k
) ) ) )
265263, 264bitr4d 248 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) k ) )  <->  ( F `  x )  e.  ( 
-oo (,) k ) ) )
266109biantrurd 495 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( F `  x )  <  k  <->  ( ( F `  x
)  e.  RR  /\  ( F `  x )  <  k ) ) )
267261, 265, 2663bitr4d 277 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( `' F " (  -oo (,) k ) )  <->  ( F `  x )  <  k
) )
268267notbid 286 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( -.  x  e.  ( `' F "
(  -oo (,) k ) )  <->  -.  ( F `  x )  <  k
) )
269216, 109lenltd 9211 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( k  <_  ( F `  x )  <->  -.  ( F `  x
)  <  k )
)
270268, 269bitr4d 248 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( -.  x  e.  ( `' F "
(  -oo (,) k ) )  <->  k  <_  ( F `  x )
) )
271270anbi2d 685 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( x  e.  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  /\  -.  x  e.  ( `' F " (  -oo (,) k ) ) )  <-> 
( x  e.  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  /\  k  <_  ( F `  x )
) ) )
272258, 271syl5bb 249 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( x  e.  ( if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  \  ( `' F " (  -oo (,) k ) ) )  <-> 
( x  e.  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  /\  k  <_  ( F `  x )
) ) )
273257, 272bitr4d 248 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( if ( ( n J x )  <_  n ,  ( n J x ) ,  n )  =  k  <->  x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) ) )
27460, 273sylan9bbr 682 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n )  \  {
0 } ) )  /\  x  e.  RR )  /\  x  e.  (
-u n [,] n
) )  ->  ( if ( x  e.  (
-u n [,] n
) ,  if ( ( n J x )  <_  n , 
( n J x ) ,  n ) ,  0 )  =  k  <->  x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) ) )
275274pm5.32da 623 . . . . . . . . 9  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( x  e.  ( -u n [,] n )  /\  if ( x  e.  ( -u n [,] n ) ,  if ( ( n J x )  <_  n ,  ( n J x ) ,  n ) ,  0 )  =  k )  <->  ( x  e.  ( -u n [,] n )  /\  x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  \ 
( `' F "
(  -oo (,) k ) ) ) ) ) )
27650, 58, 2753bitrd 271 . . . . . . . 8  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `  n
)  \  { 0 } ) )  /\  x  e.  RR )  ->  ( ( ( G `
 n ) `  x )  =  k  <-> 
( x  e.  (
-u n [,] n
)  /\  x  e.  ( if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  \  ( `' F " (  -oo (,) k ) ) ) ) ) )
277276pm5.32da 623 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( (
x  e.  RR  /\  ( ( G `  n ) `  x
)  =  k )  <-> 
( x  e.  RR  /\  ( x  e.  (
-u n [,] n
)  /\  x  e.  ( if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  \  ( `' F " (  -oo (,) k ) ) ) ) ) ) )
27824adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( G `  n ) : RR --> RR )
279278, 201syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( G `  n )  Fn  RR )
280 fniniseg 5843 . . . . . . . 8  |-  ( ( G `  n )  Fn  RR  ->  (
x  e.  ( `' ( G `  n
) " { k } )  <->  ( x  e.  RR  /\  ( ( G `  n ) `
 x )  =  k ) ) )
281279, 280syl 16 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( x  e.  ( `' ( G `
 n ) " { k } )  <-> 
( x  e.  RR  /\  ( ( G `  n ) `  x
)  =  k ) ) )
282 elin 3522 . . . . . . . 8  |-  ( x  e.  ( ( -u n [,] n )  i^i  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  \ 
( `' F "
(  -oo (,) k ) ) ) )  <->  ( x  e.  ( -u n [,] n )  /\  x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  \ 
( `' F "
(  -oo (,) k ) ) ) ) )
283190ad2antlr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  n  e.  RR )
284283renegcld 9456 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  -u n  e.  RR )
285 iccmbl 19452 . . . . . . . . . . . . 13  |-  ( (
-u n  e.  RR  /\  n  e.  RR )  ->  ( -u n [,] n )  e.  dom  vol )
286284, 283, 285syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( -u n [,] n )  e.  dom  vol )
287 mblss 19419 . . . . . . . . . . . 12  |-  ( (
-u n [,] n
)  e.  dom  vol  ->  ( -u n [,] n )  C_  RR )
288286, 287syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( -u n [,] n )  C_  RR )
289288sseld 3339 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( x  e.  ( -u n [,] n )  ->  x  e.  RR ) )
290289adantrd 455 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( (
x  e.  ( -u n [,] n )  /\  x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) )  ->  x  e.  RR ) )
291290pm4.71rd 617 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( (
x  e.  ( -u n [,] n )  /\  x  e.  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) )  <-> 
( x  e.  RR  /\  ( x  e.  (
-u n [,] n
)  /\  x  e.  ( if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  \  ( `' F " (  -oo (,) k ) ) ) ) ) ) )
292282, 291syl5bb 249 . . . . . . 7  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( x  e.  ( ( -u n [,] n )  i^i  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) )  <-> 
( x  e.  RR  /\  ( x  e.  (
-u n [,] n
)  /\  x  e.  ( if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  \  ( `' F " (  -oo (,) k ) ) ) ) ) ) )
293277, 281, 2923bitr4d 277 . . . . . 6  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( x  e.  ( `' ( G `
 n ) " { k } )  <-> 
x  e.  ( (
-u n [,] n
)  i^i  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) ) ) )
294293eqrdv 2433 . . . . 5  |-  ( ( ( ph  /\  n  e.  NN )  /\  k  e.  ( ran  ( G `
 n )  \  { 0 } ) )  ->  ( `' ( G `  n )
" { k } )  =  ( (
-u n [,] n
)  i^i  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) ) ) )
295 rembl 19427 . . . . . . . . 9  |-  RR  e.  dom  vol
296 fss 5591 . . . . . . . . . . 11  |-  ( ( F : RR --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  F : RR
--> RR )
2977, 67, 296sylancl 644 . . . . . . . . . 10  |-  ( ph  ->  F : RR --> RR )
298 mbfima 19516 . . . . . . . . . 10  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) )  e. 
dom  vol )
2996, 297, 298syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) )  e.  dom  vol )
300 ifcl 3767 . . . . . . . . 9  |-  ( ( RR  e.  dom  vol  /\  ( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) )  e.  dom  vol )  ->  if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  e. 
dom  vol )
301295, 299, 300sylancr 645 . . . . . . . 8  |-  ( ph  ->  if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  e.  dom  vol )
302 mbfima 19516 . . . . . . . . 9  |-  ( ( F  e. MblFn  /\  F : RR
--> RR )  ->  ( `' F " (  -oo (,) k ) )  e. 
dom  vol )
3036, 297, 302syl2anc 643 . . . . . . . 8  |-  ( ph  ->  ( `' F "
(  -oo (,) k ) )  e.  dom  vol )
304 difmbl 19429 . . . . . . . 8  |-  ( ( if ( k  =  n ,  RR , 
( `' F "
(  -oo (,) ( k  +  ( 1  / 
( 2 ^ n
) ) ) ) ) )  e.  dom  vol 
/\  ( `' F " (  -oo (,) k
) )  e.  dom  vol )  ->  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) ( k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) ) 
\  ( `' F " (  -oo (,) k
) ) )  e. 
dom  vol )
305301, 303, 304syl2anc 643 . . . . . . 7  |-  ( ph  ->  ( if ( k  =  n ,  RR ,  ( `' F " (  -oo (,) (
k  +  ( 1  /  ( 2 ^ n ) ) ) ) ) )  \ 
( `' F "
(  -oo (,) k ) ) )  e.  dom  vol )
306305ad2antrr 707 . . . . . 6  |-  ( ( ( ph