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

Theorem mbfi1flimlem 19483
Description: Lemma for mbfi1flim 19484. (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 5811 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  ( F `
 y )  e.  RR )
31feqmptd 5720 . . . . 5  |-  ( ph  ->  F  =  ( y  e.  RR  |->  ( F `
 y ) ) )
4 mbfi1flim.1 . . . . 5  |-  ( ph  ->  F  e. MblFn )
53, 4eqeltrrd 2464 . . . 4  |-  ( ph  ->  ( y  e.  RR  |->  ( F `  y ) )  e. MblFn )
62, 5mbfpos 19412 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )  e. MblFn )
7 0re 9026 . . . . . 6  |-  0  e.  RR
8 ifcl 3720 . . . . . 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 10707 . . . . . 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 10941 . . . . 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 2389 . . . 4  |-  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )  =  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) )
1513, 14fmptd 5834 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
166, 15mbfi1fseq 19482 . 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 9398 . . . 4  |-  ( (
ph  /\  y  e.  RR )  ->  -u ( F `  y )  e.  RR )
182, 5mbfneg 19411 . . . 4  |-  ( ph  ->  ( y  e.  RR  |->  -u ( F `  y
) )  e. MblFn )
1917, 18mbfpos 19412 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) )  e. MblFn )
20 ifcl 3720 . . . . . 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 10707 . . . . . 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 10941 . . . . 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 2389 . . . 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 5834 . . 3  |-  ( ph  ->  ( y  e.  RR  |->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 ) ) : RR --> ( 0 [,)  +oo ) )
2819, 27mbfi1fseq 19482 . 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 1926 . . 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 2783 . . . . . . 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 19469 . . . . . . . . . 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 9940 . . . . . . . . . 10  |-  NN  e.  _V
4140a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  NN  e.  _V )
42 inidm 3495 . . . . . . . . 9  |-  ( NN 
i^i  NN )  =  NN
4337, 38, 39, 41, 41, 42off 6261 . . . . . . . 8  |-  ( (
ph  /\  ( f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  ->  ( f  o F  o F  -  h ) : NN --> dom  S.1 )
44 fveq2 5670 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
4544breq2d 4167 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  (
0  <_  ( F `  y )  <->  0  <_  ( F `  x ) ) )
46 eqidd 2390 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  0  =  0 )
4745, 44, 46ifbieq12d 3706 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 )  =  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 ) )
48 fvex 5684 . . . . . . . . . . . . . . 15  |-  ( F `
 x )  e. 
_V
49 c0ex 9020 . . . . . . . . . . . . . . 15  |-  0  e.  _V
5048, 49ifex 3742 . . . . . . . . . . . . . 14  |-  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 )  e. 
_V
5147, 14, 50fvmpt 5747 . . . . . . . . . . . . 13  |-  ( x  e.  RR  ->  (
( y  e.  RR  |->  if ( 0  <_  ( F `  y ) ,  ( F `  y ) ,  0 ) ) `  x
)  =  if ( 0  <_  ( F `  x ) ,  ( F `  x ) ,  0 ) )
5251breq2d 4167 . . . . . . . . . . . 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 9234 . . . . . . . . . . . . . . . 16  |-  ( y  =  x  ->  -u ( F `  y )  =  -u ( F `  x ) )
5453breq2d 4167 . . . . . . . . . . . . . . 15  |-  ( y  =  x  ->  (
0  <_  -u ( F `
 y )  <->  0  <_  -u ( F `  x ) ) )
5554, 53, 46ifbieq12d 3706 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  if ( 0  <_  -u ( F `  y ) ,  -u ( F `  y ) ,  0 )  =  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 ) )
56 negex 9238 . . . . . . . . . . . . . . 15  |-  -u ( F `  x )  e.  _V
5756, 49ifex 3742 . . . . . . . . . . . . . 14  |-  if ( 0  <_  -u ( F `
 x ) , 
-u ( F `  x ) ,  0 )  e.  _V
5855, 26, 57fvmpt 5747 . . . . . . . . . . . . 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 4167 . . . . . . . . . . . 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 10455 . . . . . . . . . . . . 13  |-  NN  =  ( ZZ>= `  1 )
63 1z 10245 . . . . . . . . . . . . . 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 5907 . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  ->  (
f `  n )  e.  dom  S.1 )
70 i1ff 19437 . . . . . . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . 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 9049 . . . . . . . . . . . . . . . 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 2389 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  |->  ( ( f `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( f `
 n ) `  x ) )
7674, 75fmptd 5834 . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  n  e.  NN )  ->  (
h `  n )  e.  dom  S.1 )
80 i1ff 19437 . . . . . . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . 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 9049 . . . . . . . . . . . . . . . 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 2389 . . . . . . . . . . . . . . . 16  |-  ( n  e.  NN  |->  ( ( h `  n ) `
 x ) )  =  ( n  e.  NN  |->  ( ( h `
 n ) `  x ) )
8684, 85fmptd 5834 . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . . . . . . . . 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 5533 . . . . . . . . . . . . . . . . . . . . 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 2390 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
f `  k )  =  ( f `  k ) )
94 eqidd 2390 . . . . . . . . . . . . . . . . . . . 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 6255 . . . . . . . . . . . . . . . . . . 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 5672 . . . . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
f `  k )  e.  dom  S.1 )
99 i1ff 19437 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f `  k )  e.  dom  S.1  ->  ( f `  k ) : RR --> RR )
100 ffn 5533 . . . . . . . . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  k  e.  NN )  ->  (
h `  k )  e.  dom  S.1 )
103 i1ff 19437 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  k )  e.  dom  S.1  ->  ( h `  k ) : RR --> RR )
104 ffn 5533 . . . . . . . . . . . . . . . . . . 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 9016 . . . . . . . . . . . . . . . . . . 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 3495 . . . . . . . . . . . . . . . . . 18  |-  ( RR 
i^i  RR )  =  RR
109 eqidd 2390 . . . . . . . . . . . . . . . . . 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 2390 . . . . . . . . . . . . . . . . . 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 6255 . . . . . . . . . . . . . . . . 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 2421 . . . . . . . . . . . . . . . 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 5670 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( f  o F  o F  -  h
) `  n )  =  ( ( f  o F  o F  -  h ) `  k ) )
115114fveq1d 5672 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  (
( ( f  o F  o F  -  h ) `  n
) `  x )  =  ( ( ( f  o F  o F  -  h ) `  k ) `  x
) )
116 eqid 2389 . . . . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . . 17  |-  ( ( ( f  o F  o F  -  h
) `  k ) `  x )  e.  _V
118115, 116, 117fvmpt 5747 . . . . . . . . . . . . . . . 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 5670 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
f `  n )  =  ( f `  k ) )
121120fveq1d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( f `  n
) `  x )  =  ( ( f `
 k ) `  x ) )
122 fvex 5684 . . . . . . . . . . . . . . . . . 18  |-  ( ( f `  k ) `
 x )  e. 
_V
123121, 75, 122fvmpt 5747 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( f `  n ) `  x
) ) `  k
)  =  ( ( f `  k ) `
 x ) )
124 fveq2 5670 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  k  ->  (
h `  n )  =  ( h `  k ) )
125124fveq1d 5672 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  k  ->  (
( h `  n
) `  x )  =  ( ( h `
 k ) `  x ) )
126 fvex 5684 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  k ) `
 x )  e. 
_V
127125, 85, 126fvmpt 5747 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  NN  ->  (
( n  e.  NN  |->  ( ( h `  n ) `  x
) ) `  k
)  =  ( ( h `  k ) `
 x ) )
128123, 127oveq12d 6040 . . . . . . . . . . . . . . . 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 2431 . . . . . . . . . . . . . 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 12356 . . . . . . . . . . . 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 5811 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
f : NN --> dom  S.1  /\  h : NN --> dom  S.1 ) )  /\  x  e.  RR )  ->  ( F `  x )  e.  RR )
135 max0sub 10716 . . . . . . . . . . . . . 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 4179 . . . . . . . . . . 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 2729 . . . . . . . 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 6047 . . . . . . . . 9  |-  ( f  o F  o F  -  h )  e. 
_V
143 feq1 5518 . . . . . . . . . 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 5669 . . . . . . . . . . . . . 14  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
g `  n )  =  ( ( f  o F  o F  -  h ) `  n ) )
145144fveq1d 5672 . . . . . . . . . . . . 13  |-  ( g  =  ( f  o F  o F  -  h )  ->  (
( g `  n
) `  x )  =  ( ( ( f  o F  o F  -  h ) `  n ) `  x
) )
146145mpteq2dv 4239 . . . . . . . . . . . 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 4165 . . . . . . . . . . 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 2671 . . . . . . . . . 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 2988 . . . . . . . 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 1369 . . . . . . 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 1644 . . 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 1547    = wceq 1649    e. wcel 1717   A.wral 2651   _Vcvv 2901   ifcif 3684   class class class wbr 4155    e. cmpt 4209   dom cdm 4820    Fn wfn 5391   -->wf 5392   ` cfv 5396  (class class class)co 6022    o Fcof 6244    o Rcofr 6245   CCcc 8923   RRcr 8924   0cc0 8925   1c1 8926    + caddc 8928    +oocpnf 9052    <_ cle 9056    - cmin 9225   -ucneg 9226   NNcn 9934   ZZcz 10216   [,)cico 10852    ~~> cli 12207  MblFncmbf 19375   S.1citg1 19376   0 pc0p 19430
This theorem is referenced by:  mbfi1flim  19484
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370  ax-rep 4263  ax-sep 4273  ax-nul 4281  ax-pow 4320  ax-pr 4346  ax-un 4643  ax-inf2 7531  ax-cnex 8981  ax-resscn 8982  ax-1cn 8983  ax-icn 8984  ax-addcl 8985  ax-addrcl 8986  ax-mulcl 8987  ax-mulrcl 8988  ax-mulcom 8989  ax-addass 8990  ax-mulass 8991  ax-distr 8992  ax-i2m1 8993  ax-1ne0 8994  ax-1rid 8995  ax-rnegex 8996  ax-rrecex 8997  ax-cnre 8998  ax-pre-lttri 8999  ax-pre-lttrn 9000  ax-pre-ltadd 9001  ax-pre-mulgt0 9002  ax-pre-sup 9003
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2244  df-mo 2245  df-clab 2376  df-cleq 2382  df-clel 2385  df-nfc 2514  df-ne 2554  df-nel 2555  df-ral 2656  df-rex 2657  df-reu 2658  df-rmo 2659  df-rab 2660  df-v 2903  df-sbc 3107  df-csb 3197  df-dif 3268  df-un 3270  df-in 3272  df-ss 3279  df-pss 3281  df-nul 3574  df-if 3685  df-pw 3746  df-sn 3765  df-pr 3766  df-tp 3767  df-op 3768  df-uni 3960  df-int 3995  df-iun 4039  df-br 4156  df-opab 4210  df-mpt 4211  df-tr 4246  df-eprel 4437  df-id 4441  df-po 4446  df-so 4447  df-fr 4484  df-se 4485  df-we 4486  df-ord 4527  df-on 4528  df-lim 4529  df-suc 4530  df-om 4788  df-xp 4826  df-rel 4827  df-cnv 4828  df-co 4829  df-dm 4830  df-rn 4831  df-res 4832  df-ima 4833  df-iota 5360  df-fun 5398  df-fn 5399  df-f 5400  df-f1 5401  df-fo 5402  df-f1o 5403  df-fv 5404  df-isom 5405  df-ov 6025  df-oprab 6026  df-mpt2 6027  df-of 6246  df-ofr 6247  df-1st 6290  df-2nd 6291  df-riota 6487  df-recs 6571  df-rdg 6606  df-1o 6662  df-2o 6663  df-oadd 6666  df-er 6843  df-map 6958  df-pm 6959  df-en 7048  df-dom 7049  df-sdom 7050  df-fin 7051  df-fi 7353  df-sup 7383  df-oi 7414  df-card 7761  df-cda 7983  df-pnf 9057  df-mnf 9058  df-xr 9059  df-ltxr 9060  df-le 9061  df-sub 9227  df-neg 9228  df-div 9612  df-nn 9935  df-2 9992  df-3 9993  df-n0 10156  df-z 10217  df-uz 10423  df-q 10509  df-rp 10547  df-xneg 10644  df-xadd 10645  df-xmul 10646  df-ioo 10854  df-ico 10856  df-icc 10857  df-fz 10978  df-fzo 11068  df-fl 11131  df-seq 11253  df-exp 11312  df-hash 11548  df-cj 11833  df-re 11834  df-im 11835  df-sqr 11969  df-abs 11970  df-clim 12211  df-rlim 12212  df-sum 12409  df-rest 13579  df-topgen 13596  df-xmet 16621  df-met 16622  df-bl 16623  df-mopn 16624  df-top 16888  df-bases 16890  df-topon 16891  df-cmp 17374  df-ovol 19230  df-vol 19231  df-mbf 19381  df-itg1 19382  df-0p 19431
  Copyright terms: Public domain W3C validator