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

Theorem mbfi1flimlem 19604
Description: Lemma for mbfi1flim 19605. (Contributed by Mario Carneiro, 5-Sep-2014.)
Hypotheses
Ref Expression
mbfi1flim.1  |-  ( ph  ->  F  e. MblFn )
mbfi1flimlem.2  |-  ( ph  ->  F : RR --> RR )
Assertion
Ref Expression
mbfi1flimlem  |-  ( ph  ->  E. g ( g : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x ) ) )
Distinct variable groups:    g, n, x, F    ph, g, n, x

Proof of Theorem mbfi1flimlem
Dummy variables  y 
f  h  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mbfi1flimlem.2 . . . . 5  |-  ( ph  ->  F : RR --> RR )
21ffvelrnda 5862 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 y )  e.  RR )
31feqmptd 5771 . . . . 5  |-  ( ph  ->  F  =  ( y  e.  RR  |->  ( F `
 y ) ) )
4 mbfi1flim.1 . . . . 5  |-  ( ph  ->  F  e. MblFn )
53, 4eqeltrrd 2510 . . . 4  |-  ( ph  ->  ( y  e.  RR  |->  ( F `  y ) )  e. MblFn )
62, 5mbfpos 19533 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )  e. MblFn )
7 0re 9081 . . . . . 6  |-  0  e.  RR
8 ifcl 3767 . . . . . 6  |-  ( ( ( F `  y
)  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_ 
( F `  y
) ,  ( F `
 y ) ,  0 )  e.  RR )
92, 7, 8sylancl 644 . . . . 5  |-  ( (
ph  /\  y  e.  RR )  ->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 )  e.  RR )
10 max1 10763 . . . . . 6  |-  ( ( 0  e.  RR  /\  ( F `  y )  e.  RR )  -> 
0  <_  if (
0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )
117, 2, 10sylancr 645 . . . . 5  |-  ( (
ph  /\  y  e.  RR )  ->  0  <_  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )
12 elrege0 10997 . . . . 5  |-  ( if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 )  e.  ( 0 [,)  +oo )  <->  ( if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 )  e.  RR  /\  0  <_  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) )
139, 11, 12sylanbrc 646 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 )  e.  ( 0 [,)  +oo ) )
14 eqid 2435 . . . 4  |-  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )  =  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )
1513, 14fmptd 5885 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
166, 15mbfi1fseq 19603 . 2  |-  ( ph  ->  E. f ( f : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( f `  n )  /\  (
f `  n )  o R  <_  ( f `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) ) )
172renegcld 9454 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  -u ( F `  y )  e.  RR )
182, 5mbfneg 19532 . . . 4  |-  ( ph  ->  ( y  e.  RR  |->  -u ( F `  y
) )  e. MblFn )
1917, 18mbfpos 19533 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) )  e. MblFn )
20 ifcl 3767 . . . . . 6  |-  ( (
-u ( F `  y )  e.  RR  /\  0  e.  RR )  ->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 )  e.  RR )
2117, 7, 20sylancl 644 . . . . 5  |-  ( (
ph  /\  y  e.  RR )  ->  if ( 0  <_  -u ( F `
 y ) , 
-u ( F `  y ) ,  0 )  e.  RR )
22 max1 10763 . . . . . 6  |-  ( ( 0  e.  RR  /\  -u ( F `  y
)  e.  RR )  ->  0  <_  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) )
237, 17, 22sylancr 645 . . . . 5  |-  ( (
ph  /\  y  e.  RR )  ->  0  <_  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) )
24 elrege0 10997 . . . . 5  |-  ( if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 )  e.  ( 0 [,)  +oo )  <->  ( if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 )  e.  RR  /\  0  <_  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) )
2521, 23, 24sylanbrc 646 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  if ( 0  <_  -u ( F `
 y ) , 
-u ( F `  y ) ,  0 )  e.  ( 0 [,)  +oo ) )
26 eqid 2435 . . . 4  |-  ( y  e.  RR  |->  if ( 0  <_  -u ( F `
 y ) , 
-u ( F `  y ) ,  0 ) )  =  ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) )
2725, 26fmptd 5885 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
2819, 27mbfi1fseq 19603 . 2  |-  ( ph  ->  E. h ( h : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )
29 eeanv 1937 . . 3  |-  ( E. f E. h ( ( f : NN --> dom  S.1  /\  A. n  e.  NN  ( 0 p  o R  <_  (
f `  n )  /\  ( f `  n
)  o R  <_ 
( f `  (
n  +  1 ) ) )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x ) )  /\  ( h : NN --> dom  S.1  /\  A. n  e.  NN  (
0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  <->  ( E. f ( f : NN --> dom  S.1  /\  A. n  e.  NN  (
0 p  o R  <_  ( f `  n )  /\  (
f `  n )  o R  <_  ( f `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) )  /\  E. h ( h : NN --> dom  S.1  /\  A. n  e.  NN  (
0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) ) )
30 3simpb 955 . . . . . . 7  |-  ( ( f : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( f `  n )  /\  (
f `  n )  o R  <_  ( f `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) )  ->  (
f : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( f `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) ) )
31 3simpb 955 . . . . . . 7  |-  ( ( h : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  ->  (
h : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )
3230, 31anim12i 550 . . . . . 6  |-  ( ( ( f : NN --> dom  S.1  /\  A. n  e.  NN  ( 0 p  o R  <_  (
f `  n )  /\  ( f `  n
)  o R  <_ 
( f `  (
n  +  1 ) ) )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x ) )  /\  ( h : NN --> dom  S.1  /\  A. n  e.  NN  (
0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  -> 
( ( f : NN --> dom  S.1  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x ) )  /\  ( h : NN --> dom  S.1  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `
 y ) , 
-u ( F `  y ) ,  0 ) ) `  x
) ) ) )
33 an4 798 . . . . . 6  |-  ( ( ( f : NN --> dom  S.1  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) )  /\  (
h : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  <->  ( (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 )  /\  ( A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) ) )
3432, 33sylib 189 . . . . 5  |-  ( ( ( f : NN --> dom  S.1  /\  A. n  e.  NN  ( 0 p  o R  <_  (
f `  n )  /\  ( f `  n
)  o R  <_ 
( f `  (
n  +  1 ) ) )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x ) )  /\  ( h : NN --> dom  S.1  /\  A. n  e.  NN  (
0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  -> 
( ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 )  /\  ( A. x  e.  RR  ( n  e.  NN  |->  ( ( f `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) ) )
35 r19.26 2830 . . . . . . 7  |-  ( A. x  e.  RR  (
( n  e.  NN  |->  ( ( f `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  <->  ( A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `
 y ) , 
-u ( F `  y ) ,  0 ) ) `  x
) ) )
36 i1fsub 19590 . . . . . . . . . 10  |-  ( ( x  e.  dom  S.1  /\  y  e.  dom  S.1 )  ->  ( x  o F  -  y )  e.  dom  S.1 )
3736adantl 453 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  (
x  e.  dom  S.1  /\  y  e.  dom  S.1 ) )  ->  (
x  o F  -  y )  e.  dom  S.1 )
38 simprl 733 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  f : NN --> dom  S.1 )
39 simprr 734 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  h : NN --> dom  S.1 )
40 nnex 9996 . . . . . . . . . 10  |-  NN  e.  _V
4140a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  NN  e.  _V )
42 inidm 3542 . . . . . . . . 9  |-  ( NN 
i^i  NN )  =  NN
4337, 38, 39, 41, 41, 42off 6312 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  ( f  o F  o F  -  h ) : NN --> dom  S.1 )
44 fveq2 5720 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
4544breq2d 4216 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  (
0  <_  ( F `  y )  <->  0  <_  ( F `  x ) ) )
46 eqidd 2436 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  0  =  0 )
4745, 44, 46ifbieq12d 3753 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 )  =  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 ) )
48 fvex 5734 . . . . . . . . . . . . . . 15  |-  ( F `
 x )  e. 
_V
49 c0ex 9075 . . . . . . . . . . . . . . 15  |-  0  e.  _V
5048, 49ifex 3789 . . . . . . . . . . . . . 14  |-  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  e. 
_V
5147, 14, 50fvmpt 5798 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 ) )
5251breq2d 4216 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (
( n  e.  NN  |->  ( ( f `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  <->  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 ) ) )
5344negeqd 9290 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  -u ( F `  y )  =  -u ( F `  x ) )
5453breq2d 4216 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  (
0  <_  -u ( F `
 y )  <->  0  <_  -u ( F `  x ) ) )
5554, 53, 46ifbieq12d 3753 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 )  =  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )
56 negex 9294 . . . . . . . . . . . . . . 15  |-  -u ( F `  x )  e.  _V
5756, 49ifex 3789 . . . . . . . . . . . . . 14  |-  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 )  e.  _V
5855, 26, 57fvmpt 5798 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
)  =  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )
5958breq2d 4216 . . . . . . . . . . . 12  |-  ( x  e.  RR  ->  (
( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
)  <->  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) ) )
6052, 59anbi12d 692 . . . . . . . . . . 11  |-  ( x  e.  RR  ->  (
( ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  <->  ( (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  /\  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) ) ) )
6160adantl 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  (
( ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  <->  ( (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  /\  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) ) ) )
62 nnuz 10511 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
63 1z 10301 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  1  e.  ZZ )
65 simprl 733 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 ) )
6640mptex 5958 . . . . . . . . . . . . . 14  |-  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h
) `  n ) `  x ) )  e. 
_V
6766a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  e.  _V )
68 simprr 734 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )
6938ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  ->  (
f `  n )  e.  dom  S.1 )
70 i1ff 19558 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f `  n )  e.  dom  S.1  ->  ( f `  n ) : RR --> RR )
7169, 70syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  ->  (
f `  n ) : RR --> RR )
7271ffvelrnda 5862 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( ( f `
 n ) `  x )  e.  RR )
7372an32s 780 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  n  e.  NN )  ->  ( ( f `
 n ) `  x )  e.  RR )
7473recnd 9104 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  n  e.  NN )  ->  ( ( f `
 n ) `  x )  e.  CC )
75 eqid 2435 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )
7674, 75fmptd 5885 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  (
n  e.  NN  |->  ( ( f `  n
) `  x )
) : NN --> CC )
7776adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) ) : NN --> CC )
7877ffvelrnda 5862 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( f `  n ) `  x
) ) `  k
)  e.  CC )
7939ffvelrnda 5862 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  ->  (
h `  n )  e.  dom  S.1 )
80 i1ff 19558 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  n )  e.  dom  S.1  ->  ( h `  n ) : RR --> RR )
8179, 80syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  ->  (
h `  n ) : RR --> RR )
8281ffvelrnda 5862 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  /\  x  e.  RR )  ->  ( ( h `
 n ) `  x )  e.  RR )
8382an32s 780 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  n  e.  NN )  ->  ( ( h `
 n ) `  x )  e.  RR )
8483recnd 9104 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  n  e.  NN )  ->  ( ( h `
 n ) `  x )  e.  CC )
85 eqid 2435 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  |->  ( ( h `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )
8684, 85fmptd 5885 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  (
n  e.  NN  |->  ( ( h `  n
) `  x )
) : NN --> CC )
8786adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) ) : NN --> CC )
8887ffvelrnda 5862 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( h `  n ) `  x
) ) `  k
)  e.  CC )
89 ffn 5583 . . . . . . . . . . . . . . . . . . . . 21  |-  ( f : NN --> dom  S.1  ->  f  Fn  NN )
9038, 89syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  f  Fn  NN )
91 ffn 5583 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h : NN --> dom  S.1  ->  h  Fn  NN )
9239, 91syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  h  Fn  NN )
93 eqidd 2436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
f `  k )  =  ( f `  k ) )
94 eqidd 2436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
h `  k )  =  ( h `  k ) )
9590, 92, 41, 41, 42, 93, 94ofval 6306 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
( f  o F  o F  -  h
) `  k )  =  ( ( f `
 k )  o F  -  ( h `
 k ) ) )
9695fveq1d 5722 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
( ( f  o F  o F  -  h ) `  k
) `  x )  =  ( ( ( f `  k )  o F  -  (
h `  k )
) `  x )
)
9796adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  /\  x  e.  RR )  ->  ( ( ( f  o F  o F  -  h ) `  k ) `  x
)  =  ( ( ( f `  k
)  o F  -  ( h `  k
) ) `  x
) )
9838ffvelrnda 5862 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
f `  k )  e.  dom  S.1 )
99 i1ff 19558 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  k )  e.  dom  S.1  ->  ( f `  k ) : RR --> RR )
100 ffn 5583 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  k ) : RR --> RR  ->  ( f `  k )  Fn  RR )
10198, 99, 1003syl 19 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
f `  k )  Fn  RR )
10239ffvelrnda 5862 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
h `  k )  e.  dom  S.1 )
103 i1ff 19558 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  e.  dom  S.1  ->  ( h `  k ) : RR --> RR )
104 ffn 5583 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k ) : RR --> RR  ->  ( h `  k )  Fn  RR )
105102, 103, 1043syl 19 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
h `  k )  Fn  RR )
106 reex 9071 . . . . . . . . . . . . . . . . . . 19  |-  RR  e.  _V
107106a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  RR  e.  _V )
108 inidm 3542 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
i^i  RR )  =  RR
109 eqidd 2436 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  /\  x  e.  RR )  ->  ( ( f `
 k ) `  x )  =  ( ( f `  k
) `  x )
)
110 eqidd 2436 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  /\  x  e.  RR )  ->  ( ( h `
 k ) `  x )  =  ( ( h `  k
) `  x )
)
111101, 105, 107, 107, 108, 109, 110ofval 6306 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  /\  x  e.  RR )  ->  ( ( ( f `  k )  o F  -  (
h `  k )
) `  x )  =  ( ( ( f `  k ) `
 x )  -  ( ( h `  k ) `  x
) ) )
11297, 111eqtrd 2467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  /\  x  e.  RR )  ->  ( ( ( f  o F  o F  -  h ) `  k ) `  x
)  =  ( ( ( f `  k
) `  x )  -  ( ( h `
 k ) `  x ) ) )
113112an32s 780 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  k  e.  NN )  ->  ( ( ( f  o F  o F  -  h ) `  k ) `  x
)  =  ( ( ( f `  k
) `  x )  -  ( ( h `
 k ) `  x ) ) )
114 fveq2 5720 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( f  o F  o F  -  h
) `  n )  =  ( ( f  o F  o F  -  h ) `  k ) )
115114fveq1d 5722 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  (
( ( f  o F  o F  -  h ) `  n
) `  x )  =  ( ( ( f  o F  o F  -  h ) `  k ) `  x
) )
116 eqid 2435 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h
) `  n ) `  x ) )  =  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )
117 fvex 5734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  o F  o F  -  h
) `  k ) `  x )  e.  _V
118115, 116, 117fvmpt 5798 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) ) `  k
)  =  ( ( ( f  o F  o F  -  h
) `  k ) `  x ) )
119118adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h
) `  n ) `  x ) ) `  k )  =  ( ( ( f  o F  o F  -  h ) `  k
) `  x )
)
120 fveq2 5720 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
f `  n )  =  ( f `  k ) )
121120fveq1d 5722 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( f `  n
) `  x )  =  ( ( f `
 k ) `  x ) )
122 fvex 5734 . . . . . . . . . . . . . . . . . 18  |-  ( ( f `  k ) `
 x )  e. 
_V
123121, 75, 122fvmpt 5798 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( f `  n ) `  x
) ) `  k
)  =  ( ( f `  k ) `
 x ) )
124 fveq2 5720 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
h `  n )  =  ( h `  k ) )
125124fveq1d 5722 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( h `  n
) `  x )  =  ( ( h `
 k ) `  x ) )
126 fvex 5734 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k ) `
 x )  e. 
_V
127125, 85, 126fvmpt 5798 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( h `  n ) `  x
) ) `  k
)  =  ( ( h `  k ) `
 x ) )
128123, 127oveq12d 6091 . . . . . . . . . . . . . . . 16  |-  ( k  e.  NN  ->  (
( ( n  e.  NN  |->  ( ( f `
 n ) `  x ) ) `  k )  -  (
( n  e.  NN  |->  ( ( h `  n ) `  x
) ) `  k
) )  =  ( ( ( f `  k ) `  x
)  -  ( ( h `  k ) `
 x ) ) )
129128adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  k  e.  NN )  ->  ( ( ( n  e.  NN  |->  ( ( f `  n
) `  x )
) `  k )  -  ( ( n  e.  NN  |->  ( ( h `  n ) `
 x ) ) `
 k ) )  =  ( ( ( f `  k ) `
 x )  -  ( ( h `  k ) `  x
) ) )
130113, 119, 1293eqtr4d 2477 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  k  e.  NN )  ->  ( ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h
) `  n ) `  x ) ) `  k )  =  ( ( ( n  e.  NN  |->  ( ( f `
 n ) `  x ) ) `  k )  -  (
( n  e.  NN  |->  ( ( h `  n ) `  x
) ) `  k
) ) )
131130adantlr 696 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  /\  k  e.  NN )  ->  (
( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) ) `  k
)  =  ( ( ( n  e.  NN  |->  ( ( f `  n ) `  x
) ) `  k
)  -  ( ( n  e.  NN  |->  ( ( h `  n
) `  x )
) `  k )
) )
13262, 64, 65, 67, 68, 78, 88, 131climsub 12417 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  -  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) ) )
1331adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  F : RR --> RR )
134133ffvelrnda 5862 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
135 max0sub 10772 . . . . . . . . . . . . . 14  |-  ( ( F `  x )  e.  RR  ->  ( if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  -  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )  =  ( F `  x ) )
136134, 135syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  ( if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  -  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )  =  ( F `  x ) )
137136adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  -  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )  =  ( F `  x ) )
138132, 137breqtrd 4228 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  /\  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  if ( 0  <_ 
( F `  x
) ,  ( F `
 x ) ,  0 )  /\  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  if ( 0  <_  -u ( F `  x ) ,  -u ( F `  x ) ,  0 ) ) )  ->  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( F `
 x ) )
139138ex 424 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  (
( ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  /\  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )  ->  (
n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n
) `  x )
)  ~~>  ( F `  x ) ) )
14061, 139sylbid 207 . . . . . . . . 9  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  (
( ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  ->  (
n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n
) `  x )
)  ~~>  ( F `  x ) ) )
141140ralimdva 2776 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  ( A. x  e.  RR  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x )  /\  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  ->  A. x  e.  RR  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( F `
 x ) ) )
142 ovex 6098 . . . . . . . . 9  |-  ( f  o F  o F  -  h )  e. 
_V
143 feq1 5568 . . . . . . . . . 10  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
g : NN --> dom  S.1  <->  (
f  o F  o F  -  h ) : NN --> dom  S.1 ) )
144 fveq1 5719 . . . . . . . . . . . . . 14  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
g `  n )  =  ( ( f  o F  o F  -  h ) `  n ) )
145144fveq1d 5722 . . . . . . . . . . . . 13  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
( g `  n
) `  x )  =  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )
146145mpteq2dv 4288 . . . . . . . . . . . 12  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  =  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h
) `  n ) `  x ) ) )
147146breq1d 4214 . . . . . . . . . . 11  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x )  <->  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( F `
 x ) ) )
148147ralbidv 2717 . . . . . . . . . 10  |-  ( g  =  ( f  o F  o F  -  h )  ->  ( A. x  e.  RR  ( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x )  <->  A. x  e.  RR  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( F `
 x ) ) )
149143, 148anbi12d 692 . . . . . . . . 9  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
( g : NN --> dom  S.1  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( g `
 n ) `  x ) )  ~~>  ( F `
 x ) )  <-> 
( ( f  o F  o F  -  h ) : NN --> dom  S.1  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( F `
 x ) ) ) )
150142, 149spcev 3035 . . . . . . . 8  |-  ( ( ( f  o F  o F  -  h
) : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )  ~~>  ( F `
 x ) )  ->  E. g ( g : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x ) ) )
15143, 141, 150ee12an 1372 . . . . . . 7  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  ( A. x  e.  RR  ( ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x )  /\  ( n  e.  NN  |->  ( ( h `  n ) `  x
) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) )  ->  E. g
( g : NN --> dom  S.1  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( g `
 n ) `  x ) )  ~~>  ( F `
 x ) ) ) )
15235, 151syl5bir 210 . . . . . 6  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  ( ( A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( h `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `
 y ) , 
-u ( F `  y ) ,  0 ) ) `  x
) )  ->  E. g
( g : NN --> dom  S.1  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( g `
 n ) `  x ) )  ~~>  ( F `
 x ) ) ) )
153152expimpd 587 . . . . 5  |-  ( ph  ->  ( ( ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 )  /\  ( A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  ->  E. g ( g : NN --> dom  S.1  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  ~~>  ( F `  x ) ) ) )
15434, 153syl5 30 . . . 4  |-  ( ph  ->  ( ( ( f : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( f `  n )  /\  (
f `  n )  o R  <_  ( f `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) )  /\  (
h : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  ->  E. g ( g : NN --> dom  S.1  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  ~~>  ( F `  x ) ) ) )
155154exlimdvv 1647 . . 3  |-  ( ph  ->  ( E. f E. h ( ( f : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( f `  n )  /\  (
f `  n )  o R  <_  ( f `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
) )  /\  (
h : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  ->  E. g ( g : NN --> dom  S.1  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  ~~>  ( F `  x ) ) ) )
15629, 155syl5bir 210 . 2  |-  ( ph  ->  ( ( E. f
( f : NN --> dom  S.1  /\  A. n  e.  NN  ( 0 p  o R  <_  (
f `  n )  /\  ( f `  n
)  o R  <_ 
( f `  (
n  +  1 ) ) )  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( f `  n
) `  x )
)  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `
 x ) )  /\  E. h ( h : NN --> dom  S.1  /\ 
A. n  e.  NN  ( 0 p  o R  <_  ( h `  n )  /\  (
h `  n )  o R  <_  ( h `
 ( n  + 
1 ) ) )  /\  A. x  e.  RR  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )  ~~>  ( ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) `  x
) ) )  ->  E. g ( g : NN --> dom  S.1  /\  A. x  e.  RR  (
n  e.  NN  |->  ( ( g `  n
) `  x )
)  ~~>  ( F `  x ) ) ) )
15716, 28, 156mp2and 661 1  |-  ( ph  ->  E. g ( g : NN --> dom  S.1  /\ 
A. x  e.  RR  ( n  e.  NN  |->  ( ( g `  n ) `  x
) )  ~~>  ( F `
 x ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   E.wex 1550    = wceq 1652    e. wcel 1725   A.wral 2697   _Vcvv 2948   ifcif 3731   class class class wbr 4204    e. cmpt 4258   dom cdm 4870    Fn wfn 5441   -->wf 5442   ` cfv 5446  (class class class)co 6073    o Fcof 6295    o Rcofr 6296   CCcc 8978   RRcr 8979   0cc0 8980   1c1 8981    + caddc 8983    +oocpnf 9107    <_ cle 9111    - cmin 9281   -ucneg 9282   NNcn 9990   ZZcz 10272   [,)cico 10908    ~~> cli 12268  MblFncmbf 19496   S.1citg1 19497   0 pc0p 19551
This theorem is referenced by:  mbfi1flim  19605
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7586  ax-cnex 9036  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056  ax-pre-mulgt0 9057  ax-pre-sup 9058
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297  df-ofr 6298  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-er 6897  df-map 7012  df-pm 7013  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-fi 7408  df-sup 7438  df-oi 7469  df-card 7816  df-cda 8038  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116  df-sub 9283  df-neg 9284  df-div 9668  df-nn 9991  df-2 10048  df-3 10049  df-n0 10212  df-z 10273  df-uz 10479  df-q 10565  df-rp 10603  df-xneg 10700  df-xadd 10701  df-xmul 10702  df-ioo 10910  df-ico 10912  df-icc 10913  df-fz 11034  df-fzo 11126  df-fl 11192  df-seq 11314  df-exp 11373  df-hash 11609  df-cj 11894  df-re 11895  df-im 11896  df-sqr 12030  df-abs 12031  df-clim 12272  df-rlim 12273  df-sum 12470  df-rest 13640  df-topgen 13657  df-psmet 16684  df-xmet 16685  df-met 16686  df-bl 16687  df-mopn 16688  df-top 16953  df-bases 16955  df-topon 16956  df-cmp 17440  df-ovol 19351  df-vol 19352  df-mbf 19502  df-itg1 19503  df-0p 19552
  Copyright terms: Public domain W3C validator