let T be RealNormSpace; :: thesis: for f being PartFunc of REAL,T
for g being PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being Real st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) holds
||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
let f be PartFunc of REAL,T; :: thesis: for g being PartFunc of REAL,REAL st dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being Real st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) holds
||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
let g be PartFunc of REAL,REAL; :: thesis: ( dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being Real st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) implies ||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0) )
assume A1: ( dom f = [.0,1.] & dom g = [.0,1.] & f | [.0,1.] is continuous & g | [.0,1.] is continuous & f is_differentiable_on ].0,1.[ & g is_differentiable_on ].0,1.[ & ( for x being Real st x in ].0,1.[ holds
||.(diff (f,x)).|| <= diff (g,x) ) ) ; :: thesis: ||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0)
now :: thesis: for e being Real st 0 < e holds
||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e
let e be Real; :: thesis: ( 0 < e implies ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e )
assume A2: 0 < e ; :: thesis: ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e
set e1 = e / 2;
set B = { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } ;
now :: thesis: for z being object st z in { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } holds
z in REAL
let z be object ; :: thesis: ( z in { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } implies z in REAL )
assume z in { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } ; :: thesis: z in REAL
then ex x being Real st
( z = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
hence z in REAL ; :: thesis: verum
end;
then reconsider B = { x where x is Real : ( x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) } as Subset of REAL by TARSKI:def 3;
now :: thesis: for r being Real st r in B holds
|.r.| < 2
let r be Real; :: thesis: ( r in B implies |.r.| < 2 )
assume r in B ; :: thesis: |.r.| < 2
then ex x being Real st
( r = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
then A3: ex t being Real st
( r = t & 0 <= t & t <= 1 ) ;
then |.r.| = r by ABSVALUE:def 1;
hence |.r.| < 2 by A3, XXREAL_0:2; :: thesis: verum
end;
then A4: B is real-bounded by SEQ_4:4;
set s = upper_bound B;
A5: ex d being Real st
( 0 < d & d in B )
proof
0 in [.0,1.] ;
then consider d1 being Real such that
A6: ( 0 < d1 & ( for x1 being Real st x1 in [.0,1.] & |.(x1 - 0).| < d1 holds
||.((f /. x1) - (f /. 0)).|| < e / 2 ) ) by A2, A1, NFCONT_3:17;
set d2 = d1 / 2;
A7: d1 / 2 < d1 by A6, XREAL_1:216;
take d = min ((d1 / 2),1); :: thesis: ( 0 < d & d in B )
thus A8: 0 < d by A6, XXREAL_0:21; :: thesis: d in B
A9: d <= 1 by XXREAL_0:17;
then A10: d in [.0,1.] by A8;
A11: d <= d1 / 2 by XXREAL_0:17;
|.(d - 0).| = d by A8, ABSVALUE:def 1;
then |.(d - 0).| < d1 by A11, A7, XXREAL_0:2;
then A12: ||.((f /. d) - (f /. 0)).|| < e / 2 by A6, A10;
A13: [.0,d.] c= dom g by A1, A9, XXREAL_1:34;
A14: g | [.0,d.] is continuous by A1, A9, FCONT_1:16, XXREAL_1:34;
A15: ].0,d.[ c= ].0,1.[ by A9, XXREAL_1:46;
then consider x0 being Real such that
A16: ( x0 in ].0,d.[ & diff (g,x0) = ((g . d) - (g . 0)) / (d - 0) ) by A1, A8, A13, A14, FDIFF_1:26, ROLLE:3;
||.(diff (f,x0)).|| <= diff (g,x0) by A1, A16, A15;
then 0 <= (g . d) - (g . 0) by A8, A16;
then 0 + ||.((f /. d) - (f /. 0)).|| <= ((g . d) - (g . 0)) + (e / 2) by A12, XREAL_1:7;
then 0 + ||.((f /. d) - (f /. 0)).|| <= (((g . d) - (g . 0)) + (e / 2)) + ((e / 2) * d) by A8, A2, XREAL_1:7;
then ||.((f /. d) - (f /. 0)).|| - ((((g . d) - (g . 0)) + (e / 2)) + ((e / 2) * d)) <= 0 by XREAL_1:47;
then ((||.((f /. d) - (f /. 0)).|| - ((g . d) - (g . 0))) - ((e / 2) * d)) - (e / 2) <= 0 ;
hence d in B by A10; :: thesis: verum
end;
then A17: 0 < upper_bound B by A4, SEQ_4:def 1;
now :: thesis: for r being Real st r in B holds
r <= 1
let r be Real; :: thesis: ( r in B implies r <= 1 )
assume r in B ; :: thesis: r <= 1
then ex x being Real st
( r = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
then ex t being Real st
( r = t & 0 <= t & t <= 1 ) ;
hence r <= 1 ; :: thesis: verum
end;
then A18: upper_bound B <= 1 by A5, SEQ_4:45;
defpred S1[ Nat, Element of REAL ] means ( $2 in B & |.((upper_bound B) - $2).| <= 1 / ($1 + 1) );
A19: now :: thesis: for x being Element of NAT ex r being Element of REAL st S1[x,r]
let x be Element of NAT ; :: thesis: ex r being Element of REAL st S1[x,r]
reconsider t = 1 / (1 + x) as Real ;
consider r being Real such that
A20: ( r in B & (upper_bound B) - t < r ) by A4, A5, SEQ_4:def 1;
reconsider r = r as Element of REAL by XREAL_0:def 1;
take r = r; :: thesis: S1[x,r]
((upper_bound B) - t) + t < r + t by A20, XREAL_1:8;
then A21: (upper_bound B) - r < (t + r) - r by XREAL_1:14;
r <= upper_bound B by A4, A20, SEQ_4:def 1;
then 0 <= (upper_bound B) - r by XREAL_1:48;
hence S1[x,r] by A20, A21, SEQ_2:1; :: thesis: verum
end;
consider sq being sequence of REAL such that
A22: for x being Element of NAT holds S1[x,sq . x] from FUNCT_2:sch 3(A19);
A23: for x being Nat holds S1[x,sq . x]
proof
let x be Nat; :: thesis: S1[x,sq . x]
x in NAT by ORDINAL1:def 12;
hence S1[x,sq . x] by A22; :: thesis: verum
end;
reconsider sq = sq as Real_Sequence ;
A24: now :: thesis: for p1 being Real st 0 < p1 holds
ex n being Nat st
for m being Nat st n <= m holds
|.((sq . m) - (upper_bound B)).| < p1
let p1 be Real; :: thesis: ( 0 < p1 implies ex n being Nat st
for m being Nat st n <= m holds
|.((sq . m) - (upper_bound B)).| < p1 )
assume A25: 0 < p1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((sq . m) - (upper_bound B)).| < p1
set p = p1 / 2;
consider n being Nat such that
A26: 1 / (p1 / 2) < n by SEQ_4:3;
(1 / (p1 / 2)) + 0 < n + 1 by A26, XREAL_1:8;
then A27: 1 / (n + 1) <= 1 / (1 / (p1 / 2)) by A25, XREAL_1:118;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((sq . m) - (upper_bound B)).| < p1
thus for m being Nat st n <= m holds
|.((sq . m) - (upper_bound B)).| < p1 :: thesis: verum
proof
let m be Nat; :: thesis: ( n <= m implies |.((sq . m) - (upper_bound B)).| < p1 )
assume n <= m ; :: thesis: |.((sq . m) - (upper_bound B)).| < p1
then ( 0 < n + 1 & n + 1 <= m + 1 ) by XREAL_1:6;
then 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
then A28: 1 / (m + 1) <= p1 / 2 by A27, XXREAL_0:2;
( sq . m in B & |.((upper_bound B) - (sq . m)).| <= 1 / (m + 1) ) by A23;
then |.((sq . m) - (upper_bound B)).| <= 1 / (1 + m) by COMPLEX1:60;
then A29: |.((sq . m) - (upper_bound B)).| <= p1 / 2 by A28, XXREAL_0:2;
p1 / 2 < p1 by A25, XREAL_1:216;
hence |.((sq . m) - (upper_bound B)).| < p1 by A29, XXREAL_0:2; :: thesis: verum
end;
end;
then A30: sq is convergent by SEQ_2:def 6;
then A31: lim sq = upper_bound B by A24, SEQ_2:def 7;
deffunc H1( Real) -> set = ((||.((f /. $1) - (f /. 0)).|| - ((g . $1) - (g . 0))) - ((e / 2) * $1)) - (e / 2);
A32: for x being Element of REAL holds H1(x) in REAL by XREAL_0:def 1;
consider Lg0 being Function of REAL,REAL such that
A33: for x being Element of REAL holds Lg0 . x = H1(x) from FUNCT_2:sch 8(A32);
A34: for x being Real holds Lg0 . x = H1(x)
proof
let x be Real; :: thesis: Lg0 . x = H1(x)
reconsider x = x as Element of REAL by XREAL_0:def 1;
Lg0 . x = H1(x) by A33;
hence Lg0 . x = H1(x) ; :: thesis: verum
end;
set Lg = Lg0 | [.0,1.];
A35: dom Lg0 = REAL by FUNCT_2:def 1;
then A36: dom (Lg0 | [.0,1.]) = [.0,1.] by RELAT_1:62;
now :: thesis: for y being object st y in rng sq holds
y in [.0,1.]
let y be object ; :: thesis: ( y in rng sq implies y in [.0,1.] )
assume y in rng sq ; :: thesis: y in [.0,1.]
then ex x being object st
( x in NAT & sq . x = y ) by FUNCT_2:11;
then y in B by A23;
then ex x being Real st
( y = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
hence y in [.0,1.] ; :: thesis: verum
end;
then A37: rng sq c= dom (Lg0 | [.0,1.]) by A36;
A38: upper_bound B in [.0,1.] by A18, A17;
now :: thesis: for r being Real st 0 < r holds
ex t being object st
( 0 < t & ( for x1 being Real st x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t holds
|.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r ) )
let r be Real; :: thesis: ( 0 < r implies ex t being object st
( 0 < t & ( for x1 being Real st x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t holds
|.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r ) ) )
set r3 = r / 3;
assume A39: 0 < r ; :: thesis: ex t being object st
( 0 < t & ( for x1 being Real st x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t holds
|.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r ) )
then consider t1 being Real such that
A40: ( 0 < t1 & ( for x1 being Real st x1 in [.0,1.] & |.(x1 - (upper_bound B)).| < t1 holds
||.((f /. x1) - (f /. (upper_bound B))).|| < r / 3 ) ) by A1, A38, NFCONT_3:17;
consider t2 being Real such that
A41: ( 0 < t2 & ( for x1 being Real st x1 in [.0,1.] & |.(x1 - (upper_bound B)).| < t2 holds
|.((g . x1) - (g . (upper_bound B))).| < r / 3 ) ) by A39, A38, A1, FCONT_1:14;
set t30 = (r / 3) / (e / 2);
set t3 = ((r / 3) / (e / 2)) / 2;
( 0 < ((r / 3) / (e / 2)) / 2 & ((r / 3) / (e / 2)) / 2 < (r / 3) / (e / 2) ) by A2, A39, XREAL_1:216;
then (e / 2) * (((r / 3) / (e / 2)) / 2) < ((r / 3) / (e / 2)) * (e / 2) by A2, XREAL_1:97;
then A42: (e / 2) * (((r / 3) / (e / 2)) / 2) < r / 3 by A2, XCMPLX_1:87;
take t = min ((min (t1,t2)),(((r / 3) / (e / 2)) / 2)); :: thesis: ( 0 < t & ( for x1 being Real st x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t holds
|.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r ) )
A43: ( min (t1,t2) <= t1 & min (t1,t2) <= t2 & 0 < min (t1,t2) ) by A40, A41, XXREAL_0:17, XXREAL_0:21;
hence 0 < t by A2, A39, XXREAL_0:21; :: thesis: for x1 being Real st x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t holds
|.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r
A44: t <= ((r / 3) / (e / 2)) / 2 by XXREAL_0:17;
A45: t <= min (t1,t2) by XXREAL_0:17;
then A46: t <= t1 by A43, XXREAL_0:2;
A47: t <= t2 by A43, A45, XXREAL_0:2;
thus for x1 being Real st x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t holds
|.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r :: thesis: verum
proof
let x1 be Real; :: thesis: ( x1 in dom (Lg0 | [.0,1.]) & |.(x1 - (upper_bound B)).| < t implies |.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r )
assume that
A48: x1 in dom (Lg0 | [.0,1.]) and
A49: |.(x1 - (upper_bound B)).| < t ; :: thesis: |.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r
x1 in [.0,1.] by A35, A48, RELAT_1:62;
then A50: (Lg0 | [.0,1.]) . x1 = Lg0 . x1 by FUNCT_1:49
.= ((||.((f /. x1) - (f /. 0)).|| - ((g . x1) - (g . 0))) - ((e / 2) * x1)) - (e / 2) by A34 ;
(Lg0 | [.0,1.]) . (upper_bound B) = Lg0 . (upper_bound B) by A38, FUNCT_1:49;
then (Lg0 | [.0,1.]) . (upper_bound B) = ((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2) by A34;
then ((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B)) = ((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B)))) - ((e / 2) * (x1 - (upper_bound B))) by A50;
then A51: |.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| <= |.((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B)))).| + |.((e / 2) * (x1 - (upper_bound B))).| by COMPLEX1:57;
|.((||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((g . x1) - (g . (upper_bound B)))).| + |.((e / 2) * (x1 - (upper_bound B))).| <= (|.(||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||).| + |.((g . x1) - (g . (upper_bound B))).|) + |.((e / 2) * (x1 - (upper_bound B))).| by COMPLEX1:57, XREAL_1:6;
then A52: |.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| <= (|.(||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||).| + |.((g . x1) - (g . (upper_bound B))).|) + |.((e / 2) * (x1 - (upper_bound B))).| by A51, XXREAL_0:2;
((f /. x1) - (f /. 0)) - ((f /. (upper_bound B)) - (f /. 0)) = (f /. x1) - ((f /. 0) - (- ((f /. (upper_bound B)) - (f /. 0)))) by RLVECT_1:29
.= (f /. x1) - ((f /. 0) + ((f /. (upper_bound B)) - (f /. 0))) by RLVECT_1:17
.= (f /. x1) - ((f /. (upper_bound B)) - ((f /. 0) - (f /. 0))) by RLVECT_1:29
.= (f /. x1) - ((f /. (upper_bound B)) - (0. T)) by RLVECT_1:5
.= (f /. x1) - (f /. (upper_bound B)) by RLVECT_1:13 ;
then |.(||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||).| + |.((g . x1) - (g . (upper_bound B))).| <= ||.((f /. x1) - (f /. (upper_bound B))).|| + |.((g . x1) - (g . (upper_bound B))).| by NORMSP_1:9, XREAL_1:6;
then (|.(||.((f /. x1) - (f /. 0)).|| - ||.((f /. (upper_bound B)) - (f /. 0)).||).| + |.((g . x1) - (g . (upper_bound B))).|) + |.((e / 2) * (x1 - (upper_bound B))).| <= (||.((f /. x1) - (f /. (upper_bound B))).|| + |.((g . x1) - (g . (upper_bound B))).|) + |.((e / 2) * (x1 - (upper_bound B))).| by XREAL_1:6;
then A54: |.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| <= (||.((f /. x1) - (f /. (upper_bound B))).|| + |.((g . x1) - (g . (upper_bound B))).|) + |.((e / 2) * (x1 - (upper_bound B))).| by A52, XXREAL_0:2;
|.(x1 - (upper_bound B)).| < t2 by A49, A47, XXREAL_0:2;
then |.((g . x1) - (g . (upper_bound B))).| < r / 3 by A48, A36, A41;
then A55: ||.((f /. x1) - (f /. (upper_bound B))).|| + |.((g . x1) - (g . (upper_bound B))).| < ||.((f /. x1) - (f /. (upper_bound B))).|| + (r / 3) by XREAL_1:8;
|.(x1 - (upper_bound B)).| < ((r / 3) / (e / 2)) / 2 by A49, A44, XXREAL_0:2;
then |.(x1 - (upper_bound B)).| * (e / 2) <= (((r / 3) / (e / 2)) / 2) * (e / 2) by A2, XREAL_1:64;
then |.(x1 - (upper_bound B)).| * |.(e / 2).| <= (((r / 3) / (e / 2)) / 2) * (e / 2) by A2, ABSVALUE:def 1;
then |.((e / 2) * (x1 - (upper_bound B))).| <= (((r / 3) / (e / 2)) / 2) * (e / 2) by COMPLEX1:65;
then A56: |.((e / 2) * (x1 - (upper_bound B))).| < r / 3 by A42, XXREAL_0:2;
|.(x1 - (upper_bound B)).| < t1 by A49, A46, XXREAL_0:2;
then ||.((f /. x1) - (f /. (upper_bound B))).|| < r / 3 by A48, A36, A40;
then ||.((f /. x1) - (f /. (upper_bound B))).|| + (r / 3) < (r / 3) + (r / 3) by XREAL_1:8;
then ||.((f /. x1) - (f /. (upper_bound B))).|| + |.((g . x1) - (g . (upper_bound B))).| < (r / 3) + (r / 3) by A55, XXREAL_0:2;
then (||.((f /. x1) - (f /. (upper_bound B))).|| + |.((g . x1) - (g . (upper_bound B))).|) + |.((e / 2) * (x1 - (upper_bound B))).| < ((r / 3) + (r / 3)) + (r / 3) by A56, XREAL_1:8;
hence |.(((Lg0 | [.0,1.]) . x1) - ((Lg0 | [.0,1.]) . (upper_bound B))).| < r by A54, XXREAL_0:2; :: thesis: verum
end;
end;
then A57: Lg0 | [.0,1.] is_continuous_in upper_bound B by FCONT_1:3;
then A57a: ( (Lg0 | [.0,1.]) /* sq is convergent & (Lg0 | [.0,1.]) . (upper_bound B) = lim ((Lg0 | [.0,1.]) /* sq) ) by A30, A31, A37, FCONT_1:def 1;
A58: for n being Nat holds 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n
proof
let n be Nat; :: thesis: 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n
A59: n in NAT by ORDINAL1:def 12;
(- ((Lg0 | [.0,1.]) /* sq)) . n = - (((Lg0 | [.0,1.]) /* sq) . n) by SEQ_1:10;
then A60: (- ((Lg0 | [.0,1.]) /* sq)) . n = - ((Lg0 | [.0,1.]) . (sq . n)) by A37, FUNCT_2:108, A59;
S1[n,sq . n] by A23;
then A61: ex x being Real st
( sq . n = x & x in [.0,1.] & ((||.((f /. x) - (f /. 0)).|| - ((g . x) - (g . 0))) - ((e / 2) * x)) - (e / 2) <= 0 ) ;
then Lg0 . (sq . n) <= 0 by A34;
then (Lg0 | [.0,1.]) . (sq . n) <= 0 by A61, FUNCT_1:49;
hence 0 <= (- ((Lg0 | [.0,1.]) /* sq)) . n by A60; :: thesis: verum
end;
- ((Lg0 | [.0,1.]) /* sq) is convergent by A57, A30, A31, A37, FCONT_1:def 1, SEQ_2:9;
then 0 <= lim (- ((Lg0 | [.0,1.]) /* sq)) by A58, SEQ_2:17;
then 0 <= - (lim ((Lg0 | [.0,1.]) /* sq)) by A57a, SEQ_2:10;
then (Lg0 | [.0,1.]) . (upper_bound B) <= 0 by A57a;
then Lg0 . (upper_bound B) <= 0 by A38, FUNCT_1:49;
then A62: ((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2) <= 0 by A34;
A63: upper_bound B = 1
proof
assume upper_bound B <> 1 ; :: thesis: contradiction
then upper_bound B < 1 by A18, XXREAL_0:1;
then A64: upper_bound B in ].0,1.[ by A17;
then f is_differentiable_in upper_bound B by A1, NDIFF_3:10;
then consider N1 being Neighbourhood of upper_bound B such that
A65: ( N1 c= dom f & ex L1 being LinearFunc of T ex R1 being RestFunc of T st
( diff (f,(upper_bound B)) = L1 /. 1 & ( for x being Real st x in N1 holds
(f /. x) - (f /. (upper_bound B)) = (L1 /. (x - (upper_bound B))) + (R1 /. (x - (upper_bound B))) ) ) ) by NDIFF_3:def 4;
consider L1 being LinearFunc of T, R1 being RestFunc of T such that
A66: ( diff (f,(upper_bound B)) = L1 /. 1 & ( for x being Real st x in N1 holds
(f /. x) - (f /. (upper_bound B)) = (L1 /. (x - (upper_bound B))) + (R1 /. (x - (upper_bound B))) ) ) by A65;
g is_differentiable_in upper_bound B by A1, A64, FDIFF_1:9;
then consider N2 being Neighbourhood of upper_bound B such that
A67: ( N2 c= dom g & ex L2 being LinearFunc ex R2 being RestFunc st
( diff (g,(upper_bound B)) = L2 . 1 & ( for x being Real st x in N2 holds
(g . x) - (g . (upper_bound B)) = (L2 . (x - (upper_bound B))) + (R2 . (x - (upper_bound B))) ) ) ) by FDIFF_1:def 5;
consider L2 being LinearFunc, R2 being RestFunc such that
A68: ( diff (g,(upper_bound B)) = L2 . 1 & ( for x being Real st x in N2 holds
(g . x) - (g . (upper_bound B)) = (L2 . (x - (upper_bound B))) + (R2 . (x - (upper_bound B))) ) ) by A67;
consider NN3 being Neighbourhood of upper_bound B such that
A69: ( NN3 c= N1 & NN3 c= N2 ) by RCOMP_1:17;
consider g0 being Real such that
A70: ( 0 < g0 & ].((upper_bound B) - g0),((upper_bound B) + g0).[ c= ].0,1.[ ) by A64, RCOMP_1:19;
reconsider NN4 = ].((upper_bound B) - g0),((upper_bound B) + g0).[ as Neighbourhood of upper_bound B by A70, RCOMP_1:def 6;
consider N3 being Neighbourhood of upper_bound B such that
A71: ( N3 c= NN3 & N3 c= NN4 ) by RCOMP_1:17;
consider d1 being Real such that
A73: ( 0 < d1 & N3 = ].((upper_bound B) - d1),((upper_bound B) + d1).[ ) by RCOMP_1:def 6;
set e2 = (e / 2) / 2;
( R1 is total & R1 is RestFunc-like ) by NDIFF_3:def 1;
then consider d2 being Real such that
A74: ( 0 < d2 & ( for t being Real st t <> 0 & |.t.| < d2 holds
||.(R1 /. t).|| / |.t.| < (e / 2) / 2 ) ) by A2, Th17;
( R2 is total & R2 is RestFunc-like ) by FDIFF_1:def 2;
then consider d3 being Real such that
A75: ( 0 < d3 & ( for t being Real st t <> 0 & |.t.| < d3 holds
|.(R2 . t).| / |.t.| < (e / 2) / 2 ) ) by A2, Th18;
A76: ( min (d1,d2) <= d1 & min (d1,d2) <= d2 & 0 < min (d1,d2) ) by A73, A74, XXREAL_0:17, XXREAL_0:21;
set d40 = min ((min (d1,d2)),d3);
A77: ( min ((min (d1,d2)),d3) <= min (d1,d2) & min ((min (d1,d2)),d3) <= d3 & 0 < min ((min (d1,d2)),d3) ) by A75, A76, XXREAL_0:17, XXREAL_0:21;
set d4 = (min ((min (d1,d2)),d3)) / 2;
A78: ( min ((min (d1,d2)),d3) <= d1 & min ((min (d1,d2)),d3) <= d2 ) by A76, A77, XXREAL_0:2;
(min ((min (d1,d2)),d3)) / 2 < min ((min (d1,d2)),d3) by A77, XREAL_1:216;
then A79a: ( 0 < (min ((min (d1,d2)),d3)) / 2 & (min ((min (d1,d2)),d3)) / 2 < d1 & (min ((min (d1,d2)),d3)) / 2 < d2 & (min ((min (d1,d2)),d3)) / 2 < d3 ) by A77, A78, XXREAL_0:2;
then ( (upper_bound B) - d1 < (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) & (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) < (upper_bound B) + d1 ) by XREAL_1:8;
then A80: (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in N3 by A73;
then A81: (f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B)) = (L1 /. (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) + (R1 /. (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) by A66, A71, A69;
A82: (g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B)) = (L2 . (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) + (R2 . (((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)) - (upper_bound B))) by A71, A69, A80, A68;
consider df1 being Point of T such that
A83: for p being Real holds L1 /. p = p * df1 by NDIFF_3:def 2;
L1 /. 1 = 1 * df1 by A83;
then L1 /. 1 = df1 by RLVECT_1:def 8;
then A84: L1 /. ((min ((min (d1,d2)),d3)) / 2) = ((min ((min (d1,d2)),d3)) / 2) * (diff (f,(upper_bound B))) by A66, A83;
consider df2 being Real such that
A85: for p being Real holds L2 . p = df2 * p by FDIFF_1:def 3;
L2 . 1 = df2 * 1 by A85;
then A86: L2 . ((min ((min (d1,d2)),d3)) / 2) = ((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B))) by A68, A85;
A87: ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= ||.(L1 /. ((min ((min (d1,d2)),d3)) / 2)).|| + ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| by A81, NORMSP_1:def 1;
A88: ||.(L1 /. ((min ((min (d1,d2)),d3)) / 2)).|| = |.((min ((min (d1,d2)),d3)) / 2).| * ||.(diff (f,(upper_bound B))).|| by A84, NORMSP_1:def 1
.= ||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2) by A77, ABSVALUE:def 1 ;
A89: 0 < |.((min ((min (d1,d2)),d3)) / 2).| by A77, ABSVALUE:def 1;
|.((min ((min (d1,d2)),d3)) / 2).| < d2 by A79a, ABSVALUE:def 1;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| / |.((min ((min (d1,d2)),d3)) / 2).| < (e / 2) / 2 by A74, A77;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= ((e / 2) / 2) * |.((min ((min (d1,d2)),d3)) / 2).| by A89, XREAL_1:81;
then ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= ((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2) by A77, ABSVALUE:def 1;
then ||.(L1 /. ((min ((min (d1,d2)),d3)) / 2)).|| + ||.(R1 /. ((min ((min (d1,d2)),d3)) / 2)).|| <= (||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A88, XREAL_1:6;
then A90: ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= (||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A87, XXREAL_0:2;
||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2) <= (diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2) by A64, A1, A77, XREAL_1:64;
then (||.(diff (f,(upper_bound B))).|| * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= ((diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by XREAL_1:6;
then A91: ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= ((diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A90, XXREAL_0:2;
|.((min ((min (d1,d2)),d3)) / 2).| < d3 by A79a, ABSVALUE:def 1;
then |.(R2 . ((min ((min (d1,d2)),d3)) / 2)).| / |.((min ((min (d1,d2)),d3)) / 2).| < (e / 2) / 2 by A75, A77;
then |.(R2 . ((min ((min (d1,d2)),d3)) / 2)).| <= ((e / 2) / 2) * |.((min ((min (d1,d2)),d3)) / 2).| by A89, XREAL_1:81;
then |.(R2 . ((min ((min (d1,d2)),d3)) / 2)).| <= ((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2) by A77, ABSVALUE:def 1;
then - (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= R2 . ((min ((min (d1,d2)),d3)) / 2) by ABSVALUE:5;
then (((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B)))) - (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= (g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B)) by A82, A86, XREAL_1:6;
then ((min ((min (d1,d2)),d3)) / 2) * (diff (g,(upper_bound B))) <= ((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by XREAL_1:20;
then ((diff (g,(upper_bound B))) * ((min ((min (d1,d2)),d3)) / 2)) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) <= (((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2))) + (((e / 2) / 2) * ((min ((min (d1,d2)),d3)) / 2)) by XREAL_1:6;
then ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| <= ((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + ((e / 2) * ((min ((min (d1,d2)),d3)) / 2)) by A91, XXREAL_0:2;
then ||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| - (((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . (upper_bound B))) + ((e / 2) * ((min ((min (d1,d2)),d3)) / 2))) <= 0 by XREAL_1:47;
then A92: (((||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| - (g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))) + (g . (upper_bound B))) - ((e / 2) * ((min ((min (d1,d2)),d3)) / 2))) + (((||.((f /. (upper_bound B)) - (f /. 0)).|| - ((g . (upper_bound B)) - (g . 0))) - ((e / 2) * (upper_bound B))) - (e / 2)) <= 0 + 0 by A62;
||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. 0)).|| - ((((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . 0)) + ((e / 2) * (((min ((min (d1,d2)),d3)) / 2) + (upper_bound B)))) + (e / 2)) <= (||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. (upper_bound B))).|| + ||.((f /. (upper_bound B)) - (f /. 0)).||) - ((((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . 0)) + ((e / 2) * (((min ((min (d1,d2)),d3)) / 2) + (upper_bound B)))) + (e / 2)) by NORMSP_1:10, XREAL_1:9;
then A93: ((||.((f /. ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (f /. 0)).|| - ((g . ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2))) - (g . 0))) - ((e / 2) * ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))) - (e / 2) <= 0 by A92;
|.((0 + 1) - (2 * ((upper_bound B) + ((min ((min (d1,d2)),d3)) / 2)))).| < 1 - 0 by A80, A71, A70, RCOMP_1:3;
then (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in [.0,1.] by RCOMP_1:2;
then A94: (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) in B by A93;
(upper_bound B) + 0 < (upper_bound B) + ((min ((min (d1,d2)),d3)) / 2) by A77, XREAL_1:8;
hence contradiction by A94, A4, SEQ_4:def 1; :: thesis: verum
end;
( 0 in dom g & 1 in dom g ) by A1;
then ( g /. 1 = g . 1 & g /. 0 = g . 0 ) by PARTFUN1:def 6;
then ((||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0))) - e) + e <= 0 + e by A63, A62, XREAL_1:6;
hence ||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0)) <= e ; :: thesis: verum
end;
then (||.((f /. 1) - (f /. 0)).|| - ((g /. 1) - (g /. 0))) + ((g /. 1) - (g /. 0)) <= 0 + ((g /. 1) - (g /. 0)) by Lm3, XREAL_1:6;
hence ||.((f /. 1) - (f /. 0)).|| <= (g /. 1) - (g /. 0) ; :: thesis: verum