Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lvsovso Unicode version

Theorem lvsovso 25729
Description: If the limit values of two convergent numerical functions are strictly ordered, the values of the functions are strictly ordered for some element of the filter. Bourbaki TG IV.18 prop. 2. (Contributed by FL, 6-Dec-2010.) (Revised by Mario Carneiro, 8-Aug-2015.)
Hypotheses
Ref Expression
lvsovso.l1  |-  L1  =  U. ( ( J  fLimf  F ) `  F1 )
lvsovso.l2  |-  L 2  =  U. ( ( J 
fLimf  F ) `  F 2 )
lvsovso.j  |-  J  =  ( topGen `  ran  (,) )
Assertion
Ref Expression
lvsovso  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  E. a  e.  F  A. x  e.  a 
( F1 `  x )  <  ( F 2 `  x ) )
Distinct variable groups:    F, a, x    a, F1, x    a, F 2, x    x, J    x, L1    x, L 2    x, Y
Allowed substitution hints:    J( a)    Y( a)   
L1( a)    L 2(
a)

Proof of Theorem lvsovso
Dummy variables  r 
s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl1 958 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  F  e.  ( Fil `  Y ) )
2 simpl2 959 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  F1 : Y --> RR )
31, 2jca 518 . . 3  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR ) )
4 simpr1 961 . . 3  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( J  fLimf  F ) `  F1 )  =/=  (/) )
5 lvsovso.l2 . . . . . . . . . . . . . . 15  |-  L 2  =  U. ( ( J 
fLimf  F ) `  F 2 )
6 lvsovso.j . . . . . . . . . . . . . . 15  |-  J  =  ( topGen `  ran  (,) )
75, 6limnumrr 25725 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR  /\  ( ( J  fLimf  F ) `  F 2
)  =/=  (/) )  ->  L 2  e.  RR )
87recnd 8877 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR  /\  ( ( J  fLimf  F ) `  F 2
)  =/=  (/) )  ->  L 2  e.  CC )
983expia 1153 . . . . . . . . . . . 12  |-  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  ( ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  ->  L 2  e.  CC ) )
109com12 27 . . . . . . . . . . 11  |-  ( ( ( J  fLimf  F ) `
 F 2 )  =/=  (/)  ->  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  L 2  e.  CC ) )
11103ad2ant2 977 . . . . . . . . . 10  |-  ( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
)  ->  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  L 2  e.  CC ) )
1211com12 27 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  ( ( ( ( J  fLimf  F ) `
 F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 )  ->  L 2  e.  CC )
)
13123adant2 974 . . . . . . . 8  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 )  ->  L 2  e.  CC )
)
1413imp 418 . . . . . . 7  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  L 2  e.  CC )
15 lvsovso.l1 . . . . . . . . . . . . . . 15  |-  L1  =  U. ( ( J  fLimf  F ) `  F1 )
1615, 6limnumrr 25725 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  ( ( J  fLimf  F ) `  F1 )  =/=  (/) )  ->  L1  e.  RR )
1716recnd 8877 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  ( ( J  fLimf  F ) `  F1 )  =/=  (/) )  ->  L1  e.  CC )
18173expia 1153 . . . . . . . . . . . 12  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  ->  L1  e.  CC ) )
1918com12 27 . . . . . . . . . . 11  |-  ( ( ( J  fLimf  F ) `
 F1 )  =/=  (/)  ->  (
( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR )  ->  L1  e.  CC ) )
20193ad2ant1 976 . . . . . . . . . 10  |-  ( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
)  ->  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  L1  e.  CC ) )
2120com12 27 . . . . . . . . 9  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  (
( ( ( J 
fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
)  ->  L1  e.  CC ) )
22213adant3 975 . . . . . . . 8  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 )  ->  L1  e.  CC ) )
2322imp 418 . . . . . . 7  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  L1  e.  CC )
2414, 23subcld 9173 . . . . . 6  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( L 2  -  L1 )  e.  CC )
2524abscld 11934 . . . . 5  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( abs `  ( L 2  -  L1 )
)  e.  RR )
2625rehalfcld 9974 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR )
27 simpr3 963 . . . . . . . 8  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  L1 
<  L 2 )
28163expia 1153 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  ->  L1  e.  RR ) )
2928com12 27 . . . . . . . . . . . . 13  |-  ( ( ( J  fLimf  F ) `
 F1 )  =/=  (/)  ->  (
( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR )  ->  L1  e.  RR ) )
30293ad2ant1 976 . . . . . . . . . . . 12  |-  ( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
)  ->  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  L1  e.  RR ) )
3130com12 27 . . . . . . . . . . 11  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  (
( ( ( J 
fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
)  ->  L1  e.  RR ) )
32313adant3 975 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 )  ->  L1  e.  RR ) )
3332imp 418 . . . . . . . . 9  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  L1  e.  RR )
3473expia 1153 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  ( ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  ->  L 2  e.  RR ) )
3534com12 27 . . . . . . . . . . . . 13  |-  ( ( ( J  fLimf  F ) `
 F 2 )  =/=  (/)  ->  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  L 2  e.  RR ) )
36353ad2ant2 977 . . . . . . . . . . . 12  |-  ( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
)  ->  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  L 2  e.  RR ) )
3736com12 27 . . . . . . . . . . 11  |-  ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y --> RR )  ->  ( ( ( ( J  fLimf  F ) `
 F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 )  ->  L 2  e.  RR )
)
38373adant2 974 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 )  ->  L 2  e.  RR )
)
3938imp 418 . . . . . . . . 9  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  L 2  e.  RR )
4033, 39posdifd 9375 . . . . . . . 8  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( L1  <  L 2  <->  0  <  ( L 2  -  L1 ) ) )
4127, 40mpbid 201 . . . . . . 7  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
0  <  ( L 2  -  L1 ) )
4241gt0ne0d 9353 . . . . . 6  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( L 2  -  L1 )  =/=  0 )
43 absgt0 11824 . . . . . . 7  |-  ( ( L 2  -  L1 )  e.  CC  ->  ( ( L 2  -  L1 )  =/=  0  <->  0  <  ( abs `  ( L 2  -  L1 )
) ) )
4424, 43syl 15 . . . . . 6  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( L 2  -  L1 )  =/=  0  <->  0  <  ( abs `  ( L 2  -  L1 )
) ) )
4542, 44mpbid 201 . . . . 5  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
0  <  ( abs `  ( L 2  -  L1 ) ) )
46 halfpos2 9957 . . . . . 6  |-  ( ( abs `  ( L 2  -  L1 )
)  e.  RR  ->  ( 0  <  ( abs `  ( L 2  -  L1 ) )  <->  0  <  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )
4725, 46syl 15 . . . . 5  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( 0  <  ( abs `  ( L 2  -  L1 ) )  <->  0  <  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )
4845, 47mpbid 201 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
0  <  ( ( abs `  ( L 2  -  L1 ) )  / 
2 ) )
4926, 48elrpd 10404 . . 3  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR+ )
50 simpl3 960 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  ->  F 2 : Y --> RR )
511, 50jca 518 . . 3  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( F  e.  ( Fil `  Y )  /\  F 2 : Y
--> RR ) )
52 simpr2 962 . . 3  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( J  fLimf  F ) `  F 2
)  =/=  (/) )
53 eqid 2296 . . . . 5  |-  ( (
L1  -  ( ( abs `  ( L 2  -  L1 ) )  / 
2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  =  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )
5415, 6, 53flfneicn 25728 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR )  /\  ( ( J 
fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR+ )  ->  E. r  e.  F  ( F1 " r )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) ) )
55 eqid 2296 . . . . 5  |-  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  =  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )
565, 6, 55flfneicn 25728 . . . 4  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F 2 : Y
--> RR )  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR+ )  ->  E. s  e.  F  ( F 2 " s )  C_  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L 2  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )
5754, 56anim12i 549 . . 3  |-  ( ( ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR )  /\  (
( J  fLimf  F ) `
 F1 )  =/=  (/)  /\  (
( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR+ )  /\  (
( F  e.  ( Fil `  Y )  /\  F 2 : Y
--> RR )  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR+ ) )  -> 
( E. r  e.  F  ( F1 " r
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  E. s  e.  F  ( F 2 " s
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) ) )
583, 4, 49, 51, 52, 49, 57syl33anc 1197 . 2  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( E. r  e.  F  ( F1 " r
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  E. s  e.  F  ( F 2 " s
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) ) )
59 filin 17565 . . . . . . . . . . . . . . 15  |-  ( ( F  e.  ( Fil `  Y )  /\  r  e.  F  /\  s  e.  F )  ->  (
r  i^i  s )  e.  F )
60 inss1 3402 . . . . . . . . . . . . . . . . . 18  |-  ( r  i^i  s )  C_  r
61 inss2 3403 . . . . . . . . . . . . . . . . . 18  |-  ( r  i^i  s )  C_  s
62 imass2 5065 . . . . . . . . . . . . . . . . . . 19  |-  ( ( r  i^i  s ) 
C_  r  ->  ( F1 " ( r  i^i  s ) )  C_  ( F1 " r ) )
63 imass2 5065 . . . . . . . . . . . . . . . . . . 19  |-  ( ( r  i^i  s ) 
C_  s  ->  ( F 2 " ( r  i^i  s ) ) 
C_  ( F 2 " s ) )
6462, 63anim12i 549 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( r  i^i  s
)  C_  r  /\  ( r  i^i  s
)  C_  s )  ->  ( ( F1 " (
r  i^i  s )
)  C_  ( F1 " r )  /\  ( F 2 " ( r  i^i  s ) ) 
C_  ( F 2 " s ) ) )
6560, 61, 64mp2an 653 . . . . . . . . . . . . . . . . 17  |-  ( (
F1 " ( r  i^i  s ) )  C_  ( F1 " r )  /\  ( F 2 " ( r  i^i  s ) )  C_  ( F 2 " s
) )
66 sstr2 3199 . . . . . . . . . . . . . . . . . 18  |-  ( (
F1 " ( r  i^i  s ) )  C_  ( F1 " r )  ->  ( ( F1 " r )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  -> 
( F1 " ( r  i^i  s ) ) 
C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) ) ) )
67 sstr2 3199 . . . . . . . . . . . . . . . . . 18  |-  ( ( F 2 " (
r  i^i  s )
)  C_  ( F 2 " s )  -> 
( ( F 2 " s )  C_  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L 2  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  ->  ( F 2 " ( r  i^i  s ) ) 
C_  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) ) )
6866, 67im2anan9 808 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F1 " (
r  i^i  s )
)  C_  ( F1 " r )  /\  ( F 2 " ( r  i^i  s ) ) 
C_  ( F 2 " s ) )  ->  ( ( (
F1 " r )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " s
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  -> 
( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) ) ) )
6965, 68ax-mp 8 . . . . . . . . . . . . . . . 16  |-  ( ( ( F1 " r
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " s
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  -> 
( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) ) )
702ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  ->  F1 : Y --> RR )
71 simprl1 1000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  ->  F  e.  ( Fil `  Y ) )
72 simplr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( r  i^i  s
)  e.  F )
73 filelss 17563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F  e.  ( Fil `  Y )  /\  (
r  i^i  s )  e.  F )  ->  (
r  i^i  s )  C_  Y )
7471, 72, 73syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( r  i^i  s
)  C_  Y )
7574sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  ->  x  e.  Y )
76 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
F1 : Y --> RR  /\  x  e.  Y )  ->  ( F1 `  x
)  e.  RR )
7770, 75, 76syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( F1 `  x )  e.  RR )
7839adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  ->  L 2  e.  RR )
7926adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR )
8078, 79resubcld 9227 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR )
8180adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR )
8250ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  ->  F 2 : Y --> RR )
83 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F 2 : Y --> RR  /\  x  e.  Y
)  ->  ( F 2 `  x )  e.  RR )
8482, 75, 83syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( F 2 `  x )  e.  RR )
8577, 81, 843jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( ( F1 `  x
)  e.  RR  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR  /\  ( F 2 `  x
)  e.  RR ) )
86 ffun 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( F1 : Y --> RR  ->  Fun  F1 )
87863ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
F1 : Y --> RR  /\  F  e.  ( Fil `  Y )  /\  (
r  i^i  s )  e.  F )  ->  Fun  F1 )
88733adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
F1 : Y --> RR  /\  F  e.  ( Fil `  Y )  /\  (
r  i^i  s )  e.  F )  ->  (
r  i^i  s )  C_  Y )
89 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( F1 : Y --> RR  ->  dom  F1  =  Y )
90893ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
F1 : Y --> RR  /\  F  e.  ( Fil `  Y )  /\  (
r  i^i  s )  e.  F )  ->  dom  F1  =  Y )
9188, 90sseqtr4d 3228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
F1 : Y --> RR  /\  F  e.  ( Fil `  Y )  /\  (
r  i^i  s )  e.  F )  ->  (
r  i^i  s )  C_ 
dom  F1 )
9287, 91jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
F1 : Y --> RR  /\  F  e.  ( Fil `  Y )  /\  (
r  i^i  s )  e.  F )  ->  ( Fun  F1  /\  ( r  i^i  s )  C_  dom  F1 ) )
93923exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( F1 : Y --> RR  ->  ( F  e.  ( Fil `  Y )  ->  (
( r  i^i  s
)  e.  F  -> 
( Fun  F1  /\  (
r  i^i  s )  C_ 
dom  F1 ) ) ) )
9493impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR )  ->  (
( r  i^i  s
)  e.  F  -> 
( Fun  F1  /\  (
r  i^i  s )  C_ 
dom  F1 ) ) )
95943adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( r  i^i  s )  e.  F  ->  ( Fun  F1  /\  (
r  i^i  s )  C_ 
dom  F1 ) ) )
96 funfvima2 5770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( Fun  F1  /\  (
r  i^i  s )  C_ 
dom  F1 )  ->  (
x  e.  ( r  i^i  s )  -> 
( F1 `  x )  e.  ( F1 " (
r  i^i  s )
) ) )
9795, 96syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( r  i^i  s )  e.  F  ->  ( x  e.  ( r  i^i  s )  ->  ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) ) ) ) )
98973imp 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F  /\  x  e.  (
r  i^i  s )
)  ->  ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) ) )
99 ffun 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( F 2 : Y --> RR  ->  Fun 
F 2 )
100993ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  ->  Fun  F 2 )
101100adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F
)  ->  Fun  F 2
)
102733ad2antl1 1117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F
)  ->  ( r  i^i  s )  C_  Y
)
103 simpl3 960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F
)  ->  F 2 : Y --> RR )
104 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( F 2 : Y --> RR  ->  dom 
F 2  =  Y )
105103, 104syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F
)  ->  dom  F 2  =  Y )
106102, 105sseqtr4d 3228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F
)  ->  ( r  i^i  s )  C_  dom  F 2 )
107 funfvima2 5770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( Fun  F 2  /\  ( r  i^i  s
)  C_  dom  F 2
)  ->  ( x  e.  ( r  i^i  s
)  ->  ( F 2 `  x )  e.  ( F 2 "
( r  i^i  s
) ) ) )
108101, 106, 107syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F
)  ->  ( x  e.  ( r  i^i  s
)  ->  ( F 2 `  x )  e.  ( F 2 "
( r  i^i  s
) ) ) )
1091083impia 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F  /\  x  e.  (
r  i^i  s )
)  ->  ( F 2 `  x )  e.  ( F 2 "
( r  i^i  s
) ) )
11098, 109jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( r  i^i  s )  e.  F  /\  x  e.  (
r  i^i  s )
)  ->  ( ( F1 `  x )  e.  ( F1 " (
r  i^i  s )
)  /\  ( F 2 `  x )  e.  ( F 2 "
( r  i^i  s
) ) ) )
1111103exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  -> 
( ( r  i^i  s )  e.  F  ->  ( x  e.  ( r  i^i  s )  ->  ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) ) ) ) )
112111adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( r  i^i  s )  e.  F  ->  ( x  e.  ( r  i^i  s )  ->  ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) ) ) ) )
113112com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( r  i^i  s )  e.  F  ->  (
( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) )  ->  (
x  e.  ( r  i^i  s )  -> 
( ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) ) ) ) )
114113adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  ->  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J 
fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) )  ->  (
x  e.  ( r  i^i  s )  -> 
( ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) ) ) ) )
115114imp31 421 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) ) )
116 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( L 2  e.  RR  ->  L 2  e.  CC )
117 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( L1  e.  RR  ->  L1  e.  CC )
118 subcl 9067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( L 2  e.  CC  /\  L1  e.  CC )  -> 
( L 2  -  L1 )  e.  CC )
119116, 117, 118syl2anr 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L 2  -  L1 )  e.  CC )
120119abscld 11934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( abs `  ( L 2  -  L1 )
)  e.  RR )
121120recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( abs `  ( L 2  -  L1 )
)  e.  CC )
122121halfcld 9972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( ( abs `  ( L 2  -  L1 ) )  /  2
)  e.  CC )
1231223adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC )
1241173ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  -> 
L1  e.  CC )
125123, 124, 123add12d 9049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( ( ( abs `  ( L 2  -  L1 ) )  /  2
)  +  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  =  ( L1  +  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) ) )
1261213adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( abs `  ( L 2  -  L1 )
)  e.  CC )
1271262halvesd 9973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( ( ( abs `  ( L 2  -  L1 ) )  /  2
)  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( abs `  ( L 2  -  L1 ) ) )
128 resubcl 9127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( L 2  e.  RR  /\  L1  e.  RR )  -> 
( L 2  -  L1 )  e.  RR )
129128ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L 2  -  L1 )  e.  RR )
1301293adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( L 2  -  L1 )  e.  RR )
131 0re 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  0  e.  RR
132129, 131jctil 523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( 0  e.  RR  /\  ( L 2  -  L1 )  e.  RR ) )
1331323adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( 0  e.  RR  /\  ( L 2  -  L1 )  e.  RR ) )
134 posdif 9283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L1  <  L 2  <->  0  <  ( L 2  -  L1 )
) )
135134biimp3a 1281 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  0  <  ( L 2  -  L1 )
)
136 ltle 8926 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 0  e.  RR  /\  ( L 2  -  L1 )  e.  RR )  ->  ( 0  <  ( L 2  -  L1 )  ->  0  <_  ( L 2  -  L1 ) ) )
137133, 135, 136sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  0  <_  ( L 2  -  L1 ) )
138130, 137absidd 11921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( abs `  ( L 2  -  L1 )
)  =  ( L 2  -  L1 )
)
139127, 138eqtr2d 2329 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( L 2  -  L1 )  =  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )
140116adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  L 2  e.  CC )
141117adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  L1  e.  CC )
142120rehalfcld 9974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( ( abs `  ( L 2  -  L1 ) )  /  2
)  e.  RR )
143 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR  ->  (
( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC )
144143, 143jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR  ->  (
( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC  /\  (
( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC ) )
145 addcl 8835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC  /\  (
( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC )  -> 
( ( ( abs `  ( L 2  -  L1 ) )  /  2
)  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  CC )
146142, 144, 1453syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  e.  CC )
147140, 141, 1463jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L 2  e.  CC  /\  L1  e.  CC  /\  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  e.  CC ) )
1481473adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( L 2  e.  CC  /\  L1  e.  CC  /\  ( ( ( abs `  ( L 2  -  L1 ) )  /  2
)  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  CC ) )
149 subadd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( L 2  e.  CC  /\  L1  e.  CC  /\  (
( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  e.  CC )  ->  ( ( L 2  -  L1 )  =  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  <->  ( L1  +  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  =  L 2 ) )
150148, 149syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( ( L 2  -  L1 )  =  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  <->  ( L1  +  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  =  L 2 ) )
151139, 150mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( L1  +  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  =  L 2 )
152125, 151eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( ( ( abs `  ( L 2  -  L1 ) )  /  2
)  +  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  =  L 2 )
153129recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L 2  -  L1 )  e.  CC )
154153abscld 11934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( abs `  ( L 2  -  L1 )
)  e.  RR )
155154recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( abs `  ( L 2  -  L1 )
)  e.  CC )
156155halfcld 9972 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( ( abs `  ( L 2  -  L1 ) )  /  2
)  e.  CC )
157117, 143anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
L1  e.  RR  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  RR )  -> 
( L1  e.  CC  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC ) )
158142, 157syldan 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L1  e.  CC  /\  ( ( abs `  ( L 2  -  L1 ) )  /  2
)  e.  CC ) )
159 addcl 8835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
L1  e.  CC  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC )  -> 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  CC )
160158, 159syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L1  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  CC )
161140, 156, 1603jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
L1  e.  RR  /\  L 2  e.  RR )  ->  ( L 2  e.  CC  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC  /\  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  e.  CC ) )
1621613adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( L 2  e.  CC  /\  ( ( abs `  ( L 2  -  L1 ) )  /  2
)  e.  CC  /\  ( L1  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  CC ) )
163 subadd 9070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( L 2  e.  CC  /\  ( ( abs `  ( L 2  -  L1 )
)  /  2 )  e.  CC  /\  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  e.  CC )  ->  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  <->  ( (
( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( L1  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  =  L 2 ) )
164162, 163syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  =  (
L1  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <->  ( ( ( abs `  ( L 2  -  L1 )
)  /  2 )  +  ( L1  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  =  L 2 ) )
165152, 164mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
L1  e.  RR  /\  L 2  e.  RR  /\  L1  <  L 2 )  ->  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )
16633, 39, 27, 165syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )
167 ssel2 3188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F1 `  x )  e.  ( F1 " (
r  i^i  s )
) )  ->  ( F1 `  x )  e.  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) ) )
168 eliooord 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
F1 `  x )  e.  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  -> 
( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F1 `  x )  /\  ( F1 `  x )  < 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )
169167, 168syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F1 `  x )  e.  ( F1 " (
r  i^i  s )
) )  ->  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F1 `  x )  /\  ( F1 `  x )  < 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )
170169simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F1 `  x )  e.  ( F1 " (
r  i^i  s )
) )  ->  ( F1 `  x )  < 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) )
171 ssel2 3188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( F 2 "
( r  i^i  s
) )  C_  (
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( F 2 `  x )  e.  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )
172 eliooord 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( F 2 `  x
)  e.  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  ->  (
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x )  /\  ( F 2 `  x )  <  ( L 2  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )
173171, 172syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( F 2 "
( r  i^i  s
) )  C_  (
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x )  /\  ( F 2 `  x )  <  ( L 2  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )
174173simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( F 2 "
( r  i^i  s
) )  C_  (
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  <  ( F 2 `  x ) )
175170, 174anim12i 549 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F1 `  x )  e.  ( F1 " (
r  i^i  s )
) )  /\  (
( F 2 "
( r  i^i  s
) )  C_  (
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) ) )  ->  ( ( F1 `  x )  < 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) )
176175an4s 799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) ) )  ->  ( ( F1 `  x )  < 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) )
177176ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  -> 
( ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  < 
( L1  +  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) )
178 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  ->  (
( F1 `  x )  <  ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  <->  ( F1 `  x )  <  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) ) )
179178anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  ->  (
( ( F1 `  x
)  <  ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  / 
2 ) )  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) )  <->  ( ( F1 `  x )  <  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) )
180179imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  ->  (
( ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  < 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) )  <->  ( (
( F1 `  x )  e.  ( F1 " (
r  i^i  s )
)  /\  ( F 2 `  x )  e.  ( F 2 "
( r  i^i  s
) ) )  -> 
( ( F1 `  x
)  <  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) ) )
181177, 180syl5ibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  =  ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) )  ->  (
( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  -> 
( ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  < 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) ) )
182166, 181syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y --> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  (
( J  fLimf  F ) `
 F 2 )  =/=  (/)  /\  L1  <  L 2 ) )  -> 
( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  -> 
( ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  < 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) ) )
183182com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  -> 
( ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) )  ->  (
( ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  <  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) ) )
184183adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  ->  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J 
fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) )  ->  (
( ( F1 `  x
)  e.  ( F1 " ( r  i^i  s
) )  /\  ( F 2 `  x )  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  <  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) ) )
185184imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  < 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) )
186185adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( ( ( F1 `  x )  e.  (
F1 " ( r  i^i  s ) )  /\  ( F 2 `  x
)  e.  ( F 2 " ( r  i^i  s ) ) )  ->  ( ( F1 `  x )  < 
( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) )
187115, 186mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( ( F1 `  x
)  <  ( L 2  -  ( ( abs `  ( L 2  -  L1 ) )  / 
2 ) )  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) )
18885, 187jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
F1 " ( r  i^i  s ) )  C_  ( ( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  /\  x  e.  ( r  i^i  s ) )  -> 
( ( ( F1 `  x )  e.  RR  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR  /\  ( F 2 `  x
)  e.  RR )  /\  ( ( F1 `  x )  <  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) )
189188ex 423 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( x  e.  ( r  i^i  s )  ->  ( ( (
F1 `  x )  e.  RR  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR  /\  ( F 2 `  x
)  e.  RR )  /\  ( ( F1 `  x )  <  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) ) ) )
190 lttr 8915 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( F1 `  x
)  e.  RR  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR  /\  ( F 2 `  x
)  e.  RR )  ->  ( ( (
F1 `  x )  <  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) )  ->  ( F1 `  x )  <  ( F 2 `  x ) ) )
191190imp 418 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( F1 `  x
)  e.  RR  /\  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  e.  RR  /\  ( F 2 `  x
)  e.  RR )  /\  ( ( F1 `  x )  <  ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) )  /\  ( L 2  -  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) )  <  ( F 2 `  x ) ) )  ->  ( F1 `  x )  < 
( F 2 `  x ) )
192189, 191syl6 29 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  -> 
( x  e.  ( r  i^i  s )  ->  ( F1 `  x
)  <  ( F 2 `  x )
) )
193192ralrimiv 2638 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( F1 " ( r  i^i  s
) )  C_  (
( L1  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  /\  ( ( F  e.  ( Fil `  Y
)  /\  F1 : Y --> RR  /\  F 2 : Y
--> RR )  /\  (
( ( J  fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) ) )  ->  A. x  e.  (
r  i^i  s )
( F1 `  x )  <  ( F 2 `  x ) )
194193ex 423 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( F1 " (
r  i^i  s )
)  C_  ( ( L1  -  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) (,) ( L1  +  ( ( abs `  ( L 2  -  L1 ) )  /  2
) ) )  /\  ( F 2 " (
r  i^i  s )
)  C_  ( ( L 2  -  (
( abs `  ( L 2  -  L1 )
)  /  2 ) ) (,) ( L 2  +  ( ( abs `  ( L 2  -  L1 )
)  /  2 ) ) ) )  /\  ( r  i^i  s
)  e.  F )  ->  ( ( ( F  e.  ( Fil `  Y )  /\  F1 : Y
--> RR  /\  F 2 : Y --> RR )  /\  ( ( ( J 
fLimf  F ) `  F1 )  =/=  (/)  /\  ( ( J  fLimf  F ) `  F 2 )  =/=  (/)  /\  L1  <  L 2
) )  ->  A. x  e.  ( r  i^i  s
) ( F1 `  x
)  <  ( F 2 `  x )
) )
195 raleq 2749 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  ( r  i^i  s )  ->  ( A. x  e.  a 
( F1 `  x )  <  ( F 2 `  x )  <->  A. x  e.  ( r  i^i  s
) ( F1 `  x
)  <  ( F 2 `  x )
) )
196195rspcev 2897 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( r  i^i  s
)  e.  F  /\  A. x  e.  ( r  i^i  s ) (
F1 `  x )  <  ( F 2 `  x ) )  ->  E. a  e.  F  A. x  e.  a 
( F1 `  x )  <  ( F 2 `  x ) )
197196expcom 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( A. x  e.  ( r  i^i  s ) ( F1 `  x )  <  ( F 2 `  x )  ->  ( ( r  i^i  s )  e.  F  ->  E. a  e.  F  A. x  e.  a  ( F1 `  x )  <  ( F 2 `  x ) ) )
198194, 197syl6 29 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( F1 "