Copyright (c) 1991 Association of Mizar Users
environ
vocabulary FDIFF_1, SEQ_1, SEQM_3, PARTFUN1, RCOMP_1, ARYTM_1, RELAT_1,
FUNCT_1, ARYTM_3, SEQ_2, ORDINAL2, LIMFUNC1, BOOLE, ABSVALUE, SQUARE_1,
FINSEQ_1, FDIFF_3, ARYTM;
notation TARSKI, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
NAT_1, RELSET_1, PARTFUN1, SEQ_1, SEQ_2, SEQM_3, ABSVALUE, SQUARE_1,
RFUNCT_1, RFUNCT_2, RCOMP_1, FDIFF_1, LIMFUNC1;
constructors REAL_1, NAT_1, SEQ_2, SEQM_3, ABSVALUE, RFUNCT_1, RFUNCT_2,
RCOMP_1, FDIFF_1, LIMFUNC1, PROB_1, PARTFUN1, MEMBERED, XBOOLE_0;
clusters FDIFF_1, RELSET_1, XREAL_0, SEQ_1, SEQM_3, ARYTM_3, MEMBERED,
ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
theorems REAL_1, REAL_2, NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4, ABSVALUE,
SQUARE_1, RFUNCT_1, RFUNCT_2, RCOMP_1, FDIFF_1, LIMFUNC2, FDIFF_2,
TARSKI, SCHEME1, AXIOMS, PROB_1, ZFMISC_1, FCONT_3, LIMFUNC1, FUNCT_1,
FUNCT_2, XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes SEQ_1, SCHEME1, RCOMP_1, FDIFF_2;
begin
reserve h,h1,h2 for convergent_to_0 Real_Sequence,
c,c1 for constant Real_Sequence,
f,f1,f2 for PartFunc of REAL,REAL,
x0,r,r0,r1,r2,g,g1,g2 for Real,
n0,k,n,m for Nat,
a,b,d for Real_Sequence,
x for set;
theorem Th1:
(ex r st r>0 & [.x0-r,x0.] c= dom f) implies
ex h,c st rng c ={x0} & rng (h+c) c= dom f & for n holds h.n < 0
proof given r such that
A1: r>0 & [.x0-r,x0.] c= dom f;
deffunc F(Nat) = x0;
consider a such that
A2: for n holds a.n = F(n) from ExRealSeq;
now let n; a.(n+1) = x0 & a.n = x0 by A2; hence a.(n+1) = a.n; end;
then reconsider a as constant Real_Sequence by SEQM_3:16;
deffunc F(Nat) = (-r)/($1+2);
consider b such that
A3: for n holds b.n = F(n) from ExRealSeq;
A4: b is convergent & lim b = 0 by A3,SEQ_4:46;
A5: now let n;
0<=n by NAT_1:18;
then 0+0 < n + 2 by REAL_1:67;
then 0 < r/(n+2) by A1,SEQ_2:6;
then -(r/(n+2)) < 0 by REAL_1:26,50;
then (-r)/(n+2) < 0 by XCMPLX_1:188;
hence b.n < 0 by A3;
end;
then for n holds 0 <> b.n;
then b is_not_0 by SEQ_1:7;
then reconsider b as convergent_to_0 Real_Sequence by A4,FDIFF_1:def 1;
take b; take a;
thus rng a = {x0}
proof
thus rng a c= {x0}
proof let x; assume x in rng a; then ex n st x = a.n by RFUNCT_2:9;
then x = x0 by A2;
hence x in {x0} by TARSKI:def 1;
end;
let x; assume x in {x0};
then x = x0 by TARSKI:def 1
.= a.0 by A2;
hence x in rng a by RFUNCT_2:10;
end;
thus rng (b+a) c= dom f
proof
let x; assume x in rng (b+a); then consider n such that
A6: x = (b+a).n by RFUNCT_2:9;
A7: x = b.n +a.n by A6,SEQ_1:11
.= (-r)/(n+2) + a.n by A3
.= x0 + (-r)/(n+2) by A2; 0<=n by NAT_1:18;
then A8: 0+1 < n + 2 by REAL_1:67;
then A9: r*1 < r*(n+2) by A1,SEQ_4:6;
A10: 0 < n + 2 by A8,AXIOMS:22;
A11: 0 <> n + 2 by A8;
0 < (n + 2)" by A10,REAL_1:72;
then r * (n+2)" < r*(n + 2)*((n + 2)") by A9,REAL_1:70;
then r * ((n+2)") < r*((n + 2)*(n + 2)") by XCMPLX_1:4;
then r * (n+2)" < r * 1 by A11,XCMPLX_0:def 7;
then r/(n+2) < r by XCMPLX_0:def 9;
then x0 - r < x0 - r/(n+2) by REAL_1:92;
then x0 - r < x0 + - r/(n+2) by XCMPLX_0:def 8;
then A12: x0 - r <= x0 + (-r)/(n+2) by XCMPLX_1:188;
0 < r/(n+2) by A1,A10,SEQ_2:6;
then x0 - r/(n+2) < x0 - 0 by REAL_1:92;
then x0 + - r/(n+2) <= x0 by XCMPLX_0:def 8;
then x0 + (-r)/(n+2) <= x0 by XCMPLX_1:188;
then x0 + (-r)/(n+2) in {g1: x0 - r <= g1 & g1 <= x0 } by A12;
then x in [.x0 - r, x0.] by A7,RCOMP_1:def 1;
hence x in dom f by A1;
end;
thus thesis by A5;
end;
theorem Th2:
(ex r st r>0 & [.x0,x0+r.] c= dom f) implies
ex h,c st rng c ={x0} & rng (h+c) c= dom f & for n holds h.n > 0
proof
given r such that A1: r>0 & [.x0,x0+r.] c= dom f;
deffunc F(Nat) = x0;
consider a such that
A2: for n holds a.n = F(n) from ExRealSeq;
now let n; a.(n+1) = x0 & a.n = x0 by A2; hence a.(n+1) = a.n; end;
then reconsider a as constant Real_Sequence by SEQM_3:16;
deffunc F(Nat) = r/($1+2);
consider b such that
A3: for n holds b.n = F(n) from ExRealSeq;
A4: b is convergent & lim b = 0 by A3,SEQ_4:46;
A5: now let n; 0<=n by NAT_1:18; then 0+0 < n + 2 by REAL_1:67;
then 0 < r/(n+2) by A1,SEQ_2:6; hence 0 < b.n by A3;
end;
then for n holds 0<>b.n;
then b is_not_0 by SEQ_1:7;
then reconsider b as convergent_to_0 Real_Sequence by A4,FDIFF_1:def 1;
take b; take a;
thus rng a = {x0}
proof
thus rng a c= {x0}
proof let x; assume x in rng a; then ex n st x = a.n by RFUNCT_2:9;
then x = x0 by A2;
hence x in {x0} by TARSKI:def 1;
end;
let x; assume x in {x0};
then x = x0 by TARSKI:def 1
.= a.0 by A2;
hence x in rng a by RFUNCT_2:10;
end;
thus rng (b+a) c= dom f
proof
let x; assume x in rng (b+a); then consider n such that
A6: x = (b+a).n by RFUNCT_2:9;
A7: x = b.n +a.n by A6,SEQ_1:11
.= r/(n+2) + a.n by A3
.= r/(n+2) + x0 by A2; 0<=n by NAT_1:18;
then A8: 0+1 < n + 2 by REAL_1:67;
then A9: r*1 < r*(n+2) by A1,SEQ_4:6;
A10: 0 < n + 2 by A8,AXIOMS:22;
A11: 0 <> n + 2 by A8;
0 < (n + 2)" by A10,REAL_1:72;
then r * (n+2)" < r*(n + 2)*((n + 2)") by A9,REAL_1:70;
then r * (n+2)" < r*((n + 2)*(n + 2)") by XCMPLX_1:4;
then r * (n+2)" < r * 1 by A11,XCMPLX_0:def 7;
then r/(n+2) < r by XCMPLX_0:def 9;
then A12: x0 + r/(n+2) <= x0 + r by AXIOMS:24;
0 < r/(n+2) by A1,A10,SEQ_2:6;
then x0 + 0 < x0 + r/(n+2) by REAL_1:67;
then x0 + r/(n+2) in {g1: x0 <= g1 & g1 <= x0 + r} by A12;
then x in [.x0,x0 + r.] by A7,RCOMP_1:def 1;
hence x in dom f by A1;
end;
thus thesis by A5;
end;
theorem Th3:
(for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n < 0) holds
h"(#)(f*(h + c) - f*c) is convergent) & {x0} c= dom f implies
for h1,h2,c st rng c ={x0} & rng (h1+c) c= dom f & (for n holds h1.n < 0) &
rng (h2+c) c= dom f & (for n holds h2.n < 0) holds
lim (h1"(#)(f*(h1 + c) - f*c)) = lim (h2"(#)(f*(h2 + c) - f*c))
proof assume
A1: (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n < 0)
holds
h"(#)(f*(h + c) - f*c) is convergent) & {x0} c= dom f;
let h1,h2,c such that
A2: rng c ={x0} & rng (h1+c) c= dom f & (for n holds h1.n < 0) &
rng (h2+c) c= dom f & (for n holds h2.n < 0);
deffunc F(Nat) = h1.$1;
deffunc G(Nat) = h2.$1;
consider d such that
A3: for n holds d.(2*n) = F(n) & d.(2*n + 1) = G(n) from ExRealSeq2;
A4: h1 is convergent & lim h1 = 0 & h1 is_not_0 by FDIFF_1:def 1;
A5: h2 is convergent & lim h2 = 0 & h2 is_not_0 by FDIFF_1:def 1;
then A6: d is convergent & lim d = 0 by A3,A4,FDIFF_2:1;
now let n;
consider m such that
A7: n = 2*m or n = 2*m + 1 by SCHEME1:1;
now per cases by A7;
suppose A8: n = 2*m;
d.(2*m) = h1.m by A3;
hence d.n <> 0 by A4,A8,SEQ_1:7;
suppose A9: n = 2*m + 1;
d.(2*m + 1) = h2.m by A3;
hence d.n <> 0 by A5,A9,SEQ_1:7;
end;
hence d.n <> 0;
end;
then d is_not_0 by SEQ_1:7;
then reconsider d as convergent_to_0 Real_Sequence by A6,FDIFF_1:def 1;
A10: rng (d + c) c= dom f
proof
let x; assume x in rng (d + c); then consider n such that
A11: x = (d + c).n by RFUNCT_2:9;
A12: x = d.n + c.n by A11,SEQ_1:11;
consider m such that
A13: n = 2*m or n = 2*m + 1 by SCHEME1:1;
now per cases by A13;
suppose n = 2*m;
then x = h1.m + c.(2*m) by A3,A12
.= h1.m + c.m by SEQM_3:18
.= (h1 + c).m by SEQ_1:11;
then x in rng (h1 + c) by RFUNCT_2:10;
hence x in dom f by A2;
suppose n = 2*m + 1;
then x = h2.m + c.(2*m +1) by A3,A12
.= h2.m + c.m by SEQM_3:18
.= (h2 + c).m by SEQ_1:11;
then x in rng (h2 + c) by RFUNCT_2:10;
hence x in dom f by A2;
end;
hence x in dom f;
end;
now let n;
consider m such that
A14: n = 2*m or n = 2*m + 1 by SCHEME1:1;
now per cases by A14;
suppose A15: n = 2*m;
d.(2*m) = h1.m by A3;
hence d.n < 0 by A2,A15;
suppose A16: n = 2*m + 1;
d.(2*m + 1) = h2.m by A3;
hence d.n < 0 by A2,A16;
end;
hence d.n < 0;
end;
then A17: d"(#)(f*(d + c) - f*c) is convergent by A1,A2,A10;
deffunc F(Nat) = 2*$1;
consider a such that A18: for n holds a.n = F(n) from ExRealSeq;
deffunc F(Nat) = 2*$1+1;
consider b such that A19: for n holds b.n = F(n) from ExRealSeq;
reconsider a as increasing Seq_of_Nat by A18,FDIFF_2:2;
reconsider b as increasing Seq_of_Nat by A19,FDIFF_2:3;
A20: (d"(#)(f*(d + c) - f*c))*a = h1"(#)(f*(h1 + c) - f*c)
proof
now let n;
thus ((d"(#)(f*(d + c) - f*c))*a).n = (d"(#)(f*(d + c) - f*c)).(a.n
)
by SEQM_3:31
.= (d"(#)(f*(d + c) - f*c)).(2*n) by A18
.= (d").(2*n)*(f*(d + c) - f*c).(2*n) by SEQ_1:12
.= (d").(2*n)*((f*(d + c)).(2*n) - (f*c).(2*n)) by RFUNCT_2:6
.= (d.(2*n))"*((f*(d + c)).(2*n) - (f*c).(2*n)) by SEQ_1:def 8
.= (h1.n)"*((f*(d + c)).(2*n) - (f*c).(2*n)) by A3
.= (h1").n*((f*(d + c)).(2*n) - (f*c).(2*n)) by SEQ_1:def 8
.= (h1").n*(f.((d + c).(2*n)) - (f*c).(2*n)) by A10,RFUNCT_2:21
.= (h1").n*(f.(d.(2*n) + c.(2*n)) - (f*c).(2*n)) by SEQ_1:11
.= (h1").n*(f.(h1.n + c.(2*n)) - (f*c).(2*n)) by A3
.= (h1").n*(f.(h1.n + c.n) - (f*c).(2*n)) by SEQM_3:18
.= (h1").n*(f.((h1 + c).n) - (f*c).(2*n)) by SEQ_1:11
.= (h1").n*((f*(h1 + c)).n - (f*c).(2*n)) by A2,RFUNCT_2:21
.= (h1").n*((f*(h1 + c)).n - f.(c.(2*n))) by A1,A2,RFUNCT_2:21
.= (h1").n*((f*(h1 + c)).n - f.(c.n)) by SEQM_3:18
.= (h1").n*((f*(h1 + c)).n - (f*c).n) by A1,A2,RFUNCT_2:21
.= (h1").n*(f*(h1 + c) - f*c).n by RFUNCT_2:6
.= (h1"(#)(f*(h1 + c) - f*c)).n by SEQ_1:12;
end;
hence thesis by FUNCT_2:113;
end;
A21: (d"(#)(f*(d + c) - f*c))*b = h2"(#)(f*(h2 + c) - f*c)
proof
now let n;
thus ((d"(#)(f*(d + c) - f*c))*b).n=(d"(#)(f*(d + c) - f*c)).(b.n)
by SEQM_3:31
.= (d"(#)(f*(d + c) - f*c)).(2*n + 1) by A19
.= (d").(2*n + 1)*(f*(d + c) - f*c).(2*n + 1) by SEQ_1:12
.= (d").(2*n +1)*((f*(d + c)).(2*n + 1) - (f*c).(2*n + 1))
by RFUNCT_2:6
.= (d.( 2*n + 1))"*((f*(d + c)).(2*n + 1) - (f*c).(2*n + 1))
by SEQ_1:def 8
.= (h2.n)"*((f*(d + c)).(2*n + 1) - (f*c).(2*n + 1)) by A3
.= (h2").n*((f*(d + c)).(2*n + 1) - (f*c).(2*n + 1)) by SEQ_1:def 8
.= (h2").n*(f.((d + c).(2*n + 1)) - (f*c).(2*n + 1))
by A10,RFUNCT_2:21
.= (h2").n*(f.(d.(2*n + 1) + c.(2*n + 1)) - (f*c).(2*n + 1))
by SEQ_1:11
.= (h2").n*(f.(h2.n + c.(2*n + 1)) - (f*c).(2*n + 1)) by A3
.= (h2").n*(f.(h2.n + c.n) - (f*c).(2*n + 1)) by SEQM_3:18
.= (h2").n*(f.((h2 + c).n) - (f*c).(2*n + 1)) by SEQ_1:11
.= (h2").n*((f*(h2 + c)).n - (f*c).(2*n + 1)) by A2,RFUNCT_2:21
.= (h2").n*((f*(h2 + c)).n - f.(c.(2*n + 1))) by A1,A2,RFUNCT_2:21
.= (h2").n*((f*(h2 + c)).n - f.(c.n)) by SEQM_3:18
.= (h2").n*((f*(h2 + c)).n - (f*c).n) by A1,A2,RFUNCT_2:21
.= (h2").n*(f*(h2 + c) - f*c).n by RFUNCT_2:6
.= (h2"(#)(f*(h2 + c) - f*c)).n by SEQ_1:12;
end;
hence thesis by FUNCT_2:113;
end;
h1"(#)(f*(h1 + c) - f*c) is_subsequence_of d"(#)(f*(d + c) - f*c)
by A20,SEQM_3:def 10;
then A22: lim (h1"(#)(f*(h1 + c) - f*c)) = lim (d"(#)
(f*(d + c) - f*c)) by A17,SEQ_4:30;
h2"(#)(f*(h2 + c) - f*c) is_subsequence_of d"(#)(f*(d + c) - f*c)
by A21,SEQM_3:def 10;
hence thesis by A17,A22,SEQ_4:30;
end;
theorem Th4:
(for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n>0) holds
h"(#)(f*(h+c) - f*c) is convergent) & {x0} c= dom f implies
for h1,h2,c st rng c ={x0} & rng (h1 + c)c= dom f & rng (h2 + c) c= dom f &
(for n holds h1.n >0) & (for n holds h2.n >0) holds
lim (h1"(#)(f*(h1+c) - f*c)) = lim (h2"(#)(f*(h2+c) - f*c))
proof assume
A1: (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n>0) holds
h"(#)(f*(h+c) - f*c) is convergent) & {x0} c= dom f;
let h1,h2,c such that
A2: rng c ={x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f &
(for n holds h1.n >0) & (for n holds h2.n >0);
deffunc F(Nat) = h1.$1;
deffunc G(Nat) = h2.$1;
consider d such that
A3: for n holds d.(2*n)=F(n) & d.(2*n+1)=G(n) from ExRealSeq2;
A4: h1 is convergent & lim h1 =0 & h1 is_not_0 by FDIFF_1:def 1;
A5: h2 is convergent & lim h2 =0 & h2 is_not_0 by FDIFF_1:def 1;
then A6: d is convergent & lim d =0 by A3,A4,FDIFF_2:1;
d is_not_0
proof
now let n; consider m such that
A7: n = 2*m or n = 2*m+1 by SCHEME1:1;
now per cases by A7;
suppose n = 2*m;
then d.n = h1.m by A3;
hence d.n<>0 by A4,SEQ_1:7;
suppose n = 2*m+1;
then d.n = h2.m by A3;
hence d.n<>0 by A5,SEQ_1:7;
end;
hence d.n<>0;
end;
hence thesis by SEQ_1:7;
end;
then reconsider d as convergent_to_0 Real_Sequence by A6,FDIFF_1:def 1;
A8: rng (d+c) c= dom f
proof
let x;assume x in rng (d+c); then consider n such that
A9: x = (d+c).n by RFUNCT_2:9; consider m such that
A10: n=2*m or n=2*m+1 by SCHEME1:1;
now per cases by A10;
suppose n = 2*m;
then x = d.(2*m) + c.(2*m) by A9,SEQ_1:11
.= h1.m + c.(2*m) by A3
.= h1.m + c.m by SEQM_3:18
.= (h1+c).m by SEQ_1:11;
hence x in dom f by A2,RFUNCT_2:8;
suppose n = 2*m+1;
then x = d.(2*m+1) + c.(2*m+1) by A9,SEQ_1:11
.= h2.m + c.(2*m+1) by A3
.= h2.m + c.m by SEQM_3:18
.= (h2 + c).m by SEQ_1:11;
hence x in dom f by A2,RFUNCT_2:8;
end;
hence x in dom f;
end;
for n holds d.n > 0
proof
let n; consider m such that
A11: n = 2*m or n = 2*m+1 by SCHEME1:1;
now per cases by A11;
suppose n = 2*m;
then d.n = h1.m by A3;
hence d.n>0 by A2;
suppose n = 2*m+1;
then d.n = h2.m by A3;
hence d.n>0 by A2;
end;
hence d.n>0;
end;
then A12: d"(#)(f*(d+c) - f*c) is convergent by A1,A2,A8;
deffunc F(Nat) = 2*$1;
consider a such that
A13: for n holds a.n = F(n) from ExRealSeq;
reconsider a as increasing Seq_of_Nat by A13,FDIFF_2:2;
deffunc F(Nat) = 2*$1+1;
consider b such that
A14: for n holds b.n = F(n) from ExRealSeq;
reconsider b as increasing Seq_of_Nat by A14,FDIFF_2:3;
A15: (d"(#)(f*(d+c) - f*c))*a = h1"(#)(f*(h1+c) - f*c)
proof
now let n;
thus ((d"(#)(f*(d+c) - f*c))*a).n = (d"(#)
(f*(d+c) - f*c)).(a.n) by SEQM_3:31
.= (d"(#)(f*(d+c) - f*c)).(2*n) by A13
.= (d").(2*n) * (f*(d+c) - f*c).(2*n) by SEQ_1:12
.= (d.(2*n))" * (f*(d+c) - f*c).(2*n) by SEQ_1:def 8
.= (h1.n)" * (f*(d+c) - f*c).(2*n) by A3
.= (h1").n * (f*(d+c) - f*c).(2*n) by SEQ_1:def 8
.= (h1").n *((f*(d+c)).(2*n) - (f*c).(2*n)) by RFUNCT_2:6
.= (h1").n *(f.((d+c).(2*n)) - (f*c).(2*n)) by A8,RFUNCT_2:21
.= (h1").n *(f.((d+c).(2*n)) - f.(c.(2*n))) by A1,A2,RFUNCT_2:21
.= (h1").n *(f.(d.(2*n)+c.(2*n)) - f.(c.(2*n))) by SEQ_1:11
.= (h1").n *(f.(h1.n+c.(2*n)) - f.(c.(2*n))) by A3
.= (h1").n *(f.(h1.n+c.(2*n)) - f.(c.n)) by SEQM_3:18
.= (h1").n *(f.(h1.n+c.n) - f.(c.n)) by SEQM_3:18
.= (h1").n *(f.((h1+c).n) - f.(c.n)) by SEQ_1:11
.= (h1").n *((f*(h1+c)).n - f.(c.n)) by A2,RFUNCT_2:21
.= (h1").n *((f*(h1+c)).n - (f*c).n) by A1,A2,RFUNCT_2:21
.= (h1").n *(f*(h1+c) - f*c).n by RFUNCT_2:6
.= (h1"(#)(f*(h1+c) - f*c)).n by SEQ_1:12;
end;
hence thesis by FUNCT_2:113;
end;
A16: (d"(#)(f*(d+c) - f*c))*b = h2"(#)(f*(h2+c) - f*c)
proof
now let n;
thus ((d"(#)(f*(d+c) - f*c))*b).n = (d"(#)
(f*(d+c) - f*c)).(b.n) by SEQM_3:31
.= (d"(#)(f*(d+c) - f*c)).(2*n+1) by A14
.= (d").(2*n+1) * (f*(d+c) - f*c).(2*n+1) by SEQ_1:12
.= (d.(2*n+1))" * (f*(d+c) - f*c).(2*n+1) by SEQ_1:def 8
.= (h2.n)" * (f*(d+c) - f*c).(2*n+1) by A3
.= (h2").n * (f*(d+c) - f*c).(2*n+1) by SEQ_1:def 8
.= (h2").n *((f*(d+c)).(2*n+1) - (f*c).(2*n+1)) by RFUNCT_2:6
.= (h2").n *(f.((d+c).(2*n+1)) - (f*c).(2*n+1)) by A8,RFUNCT_2:21
.= (h2").n *(f.((d+c).(2*n+1)) - f.(c.(2*n+1))) by A1,A2,RFUNCT_2:21
.= (h2").n *(f.(d.(2*n+1)+c.(2*n+1)) - f.(c.(2*n+1))) by SEQ_1:11
.= (h2").n *(f.(h2.n+c.(2*n+1)) - f.(c.(2*n+1))) by A3
.= (h2").n *(f.(h2.n+c.(2*n+1)) - f.(c.n)) by SEQM_3:18
.= (h2").n *(f.(h2.n+c.n) - f.(c.n)) by SEQM_3:18
.= (h2").n *(f.((h2+c).n) - f.(c.n)) by SEQ_1:11
.= (h2").n *((f*(h2+c)).n - f.(c.n)) by A2,RFUNCT_2:21
.= (h2").n *((f*(h2+c)).n - (f*c).n) by A1,A2,RFUNCT_2:21
.= (h2").n *(f*(h2+c) - f*c).n by RFUNCT_2:6
.= (h2"(#)(f*(h2+c) - f*c)).n by SEQ_1:12;
end;
hence thesis by FUNCT_2:113;
end;
A17: h1"(#)(f*(h1+c) - f*c) is_subsequence_of d"(#)(f*(d+c) - f*c)
by A15,SEQM_3:def 10;
A18: h2"(#)(f*(h2+c) - f*c) is_subsequence_of d"(#)(f*(d+c) - f*c)
by A16,SEQM_3:def 10;
lim (h1"(#)(f*(h1+c) - f*c)) = lim (d"(#)
(f*(d+c) -f*c)) by A12,A17,SEQ_4:30;
hence thesis by A12,A18,SEQ_4:30;
end;
definition let f,x0;
pred f is_Lcontinuous_in x0 means :Def1:
x0 in dom f &
for a st rng a c= left_open_halfline(x0) /\ dom f & a is convergent &
lim a = x0 holds f*a is convergent & f.x0 = lim(f*a);
pred f is_Rcontinuous_in x0 means :Def2:
x0 in dom f &
for a st rng a c= right_open_halfline(x0) /\ dom f &
a is convergent & lim a = x0 holds f*a is convergent & f.x0 = lim(f*a);
pred f is_right_differentiable_in x0 means :Def3:
(ex r st r>0 & [.x0, x0+r.] c= dom f) &
for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n > 0) holds
h"(#)(f*(h + c) - f*c) is convergent;
pred f is_left_differentiable_in x0 means :Def4:
(ex r st r>0 & [.x0-r,x0.] c= dom f) &
for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n<0) holds
h"(#)(f*(h + c) - f*c) is convergent;
end;
theorem Th5:
f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0
proof
assume A1: f is_left_differentiable_in x0;
A2: x0 in dom f
proof
consider r such that A3: 0 < r & [.x0 - r,x0.] c= dom f by A1,Def4;
x0 - r <= x0 by A3,SQUARE_1:29;
then x0 in [.x0 - r,x0.] by RCOMP_1:15;
hence x0 in dom f by A3;
end;
for a st rng a c= left_open_halfline(x0) /\ dom f & a is convergent &
lim a = x0 holds f*a is convergent & f.x0 = lim(f*a)
proof let a such that
A4: rng a c= left_open_halfline(x0) /\
dom f & a is convergent & lim a = x0;
consider r such that A5: 0 < r & [.x0 - r, x0.] c= dom f by A1,Def4;
x0 - r < x0 by A5,SQUARE_1:29;
then consider n0 such that
A6: for k st k>=n0 holds x0 - r<a.k by A4,LIMFUNC2:1;
A7: for n holds (a^\n0).n in [.x0 - r,x0.]
proof
let n; 0 <= n & 0 + n0 = n0 by NAT_1:18;
then n0 <= n0 + n by AXIOMS:24;
then x0 - r <= a.(n + n0) by A6;
then A8: x0 - r <= (a^\n0).n by SEQM_3:def 9;
a.(n + n0) in rng a by RFUNCT_2:10;
then (a^\n0).n in rng a by SEQM_3:def 9;
then (a^\n0).n in left_open_halfline(x0) by A4,XBOOLE_0:def 3;
then (a^\n0).n in {g:g < x0} by PROB_1:def 15;
then ex g st g = (a^\n0).n & g < x0;
then (a^\n0).n in {g: x0 - r <= g & g <= x0} by A8;
hence (a^\n0).n in [.x0 - r,x0.] by RCOMP_1:def 1;
end;
deffunc F(Nat) = x0;
consider b such that A9: for n holds b.n = F(n) from ExRealSeq;
deffunc F(Nat) = a.$1-b.$1;
consider d such that A10: for n holds d.n = F(n) from ExRealSeq;
A11: b is constant by A9,SEQM_3:def 6;
then A12: b is convergent by SEQ_4:39;
A13: lim b = b.0 by A11,SEQ_4:41
.= x0 by A9;
A14: d = a - b by A10,RFUNCT_2:6;
then A15: d is convergent by A4,A12,SEQ_2:25;
lim d = x0 - x0 by A4,A12,A13,A14,SEQ_2:26
.= 0 by XCMPLX_1:14;
then A16: d^\n0 is convergent & lim (d^\n0) = 0 by A15,SEQ_4:33;
A17: for n holds d.n < 0 & d.n <> 0
proof let n;
A18: d.n = a.n - b.n by A10;
a.n in rng a by RFUNCT_2:10;
then a.n in left_open_halfline(x0) by A4,XBOOLE_0:def 3;
then a.n in { r1: r1 < x0 } by PROB_1:def 15;
then ex r1 st r1 = a.n & r1 < x0;
then a.n - x0 < x0 - x0 by REAL_1:54;
then A19: d.n < x0 - x0 by A9,A18;
hence d.n < 0 by XCMPLX_1:14;
thus thesis by A19,XCMPLX_1:14;
end;
A20: for n holds (d^\n0).n < 0
proof let n;
(d^\n0).n = d.(n + n0) by SEQM_3:def 9;
hence (d^\n0).n < 0 by A17;
end;
then for n holds (d^\n0).n <>0;
then d ^\n0 is_not_0 by SEQ_1:7;
then reconsider h = d^\n0 as convergent_to_0 Real_Sequence by A16,FDIFF_1:
def 1;
A21: b^\n0 is_subsequence_of b by SEQM_3:47;
b is constant by A9,SEQM_3:def 6;
then reconsider c = b^\n0 as constant Real_Sequence by A21,SEQM_3:54;
A22: rng c = {x0}
proof
thus rng c c= {x0}
proof let x;
assume x in rng c; then consider n such that
A23: x = (b^\n0).n by RFUNCT_2:9;
x = b.(n + n0) by A23,SEQM_3:def 9;
then x = x0 by A9;
hence x in {x0} by TARSKI:def 1;
end;
let x; assume x in {x0};
then A24: x = x0 by TARSKI:def 1;
c.0 = b.(0 + n0) by SEQM_3:def 9
.= x by A9,A24;
hence x in rng c by RFUNCT_2:9;
end;
rng (h + c) c= [.x0 - r,x0.]
proof let x; assume x in rng(h + c); then consider n such that
A25: x = (h+c).n by RFUNCT_2:9;
(h+c).n=((a - b +b)^\n0).n by A14,SEQM_3:37
.= (a - b + b) .(n + n0) by SEQM_3:def 9
.= (a - b).(n + n0) + b.(n + n0) by SEQ_1:11
.= a.(n + n0) - b.(n + n0) + b.(n + n0) by RFUNCT_2:6
.= a.(n + n0) by XCMPLX_1:27
.= (a^\n0).n by SEQM_3:def 9;
hence x in [.x0 - r,x0.] by A7,A25;
end;
then rng (h + c) c= dom f by A5,XBOOLE_1:1;
then A26: h"(#)(f*(h+c) - f*c) is convergent by A1,A20,A22,Def4;
then A27: lim (h(#)(h"(#)(f*(h+c) - f*c)))=0*lim(h"(#)
(f*(h+c) - f*c)) by A16,SEQ_2:29
.=0;
now let n;
A28: h.n<>0 by A20;
thus (h(#)(h"(#)(f*(h+c) - f*c))).n=h.n *(h"(#)
(f*(h+c) - f*c)).n by SEQ_1:12
.= h.n*((h").n*(f*(h+c) - f*c).n) by SEQ_1:12
.= h.n*(((h.n)")*(f*(h+c) - f*c).n) by SEQ_1:def 8
.= h.n*((h.n)")*(f*(h+c) - f*c).n by XCMPLX_1:4
.= 1*(f*(h+c) - f*c).n by A28,XCMPLX_0:def 7
.= (f*(h+c) - f*c).n;
end;
then A29: h(#)(h"(#)(f*(h+c) - f*c))=f*(h+c)-f*c by FUNCT_2:113;
then A30: f*(h+c)-f*c is convergent by A16,A26,SEQ_2:28;
A31: now let g be real number such that A32: 0<g;
take n=0; let m such that n<=m;
x0 - r <= x0 by A5,SQUARE_1:29;
then x0 in [.x0 - r,x0.] by RCOMP_1:15;
then rng c c= dom f by A5,A22,ZFMISC_1:37;
then abs((f*c).m-f.x0) = abs(f.(c.m)-f.x0) by RFUNCT_2:21
.= abs(f.(b.(m+n0))-f.x0) by SEQM_3:def 9
.= abs(f.x0-f.x0) by A9
.= abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:7;
hence abs((f*c).m-f.x0)<g by A32;
end;
then A33: f*c is convergent by SEQ_2:def 6;
then A34: lim(f*c)=f.x0 by A31,SEQ_2:def 7;
A35: f*(h+c)-f*c+f*c is convergent by A30,A33,SEQ_2:19;
A36: lim(f*(h+c)-f*c+f*c) = 0+f.x0 by A27,A29,A30,A33,A34,SEQ_2:20
.= f.x0;
now let n;
thus (f*(h+c)-f*c+f*c).n=(f*(h+c)-f*c).n+(f*c).n by SEQ_1:11
.= (f*(h+c)).n-(f*c).n+(f*c).n by RFUNCT_2:6
.= (f*(h+c)).n by XCMPLX_1:27;
end;
then A37: f*(h+c)-f*c+(f*c)=f*(h+c) by FUNCT_2:113;
A38: rng a c= dom f
proof let x; assume x in rng a; hence thesis by A4,XBOOLE_0:def 3;
end;
now let n;
thus (h+c).n=((a-b+b)^\n0).n by A14,SEQM_3:37
.= (a-b+b).(n+n0) by SEQM_3:def 9
.= (a-b).(n+n0)+b.(n+n0) by SEQ_1:11
.= a.(n+n0)-b.(n+n0)+b.(n+n0) by RFUNCT_2:6
.= a.(n+n0) by XCMPLX_1:27
.= (a^\n0).n by SEQM_3:def 9;
end;
then A39: f*(h+c)-f*c+(f*c)=f*(a^\n0) by A37,FUNCT_2:113
.= (f*a)^\n0 by A38,RFUNCT_2:22;
hence f*a is convergent by A35,SEQ_4:35;
thus f.x0=lim(f*a) by A35,A36,A39,SEQ_4:36;
end;
hence thesis by A2,Def1;
end;
theorem Th6:
f is_Lcontinuous_in x0 & f.x0<>g2 & (ex r st r>0 & [.x0-r,x0.] c= dom f)
implies ex r1 st r1 > 0 & [.x0-r1,x0.] c= dom f &
for g st g in [.x0-r1,x0.] holds f.g <> g2
proof
assume A1: f is_Lcontinuous_in x0 & f.x0 <> g2;
given r such that A2: r>0 & [.x0-r,x0.] c= dom f;
assume A3: for r1 st r1>0 & [.x0-r1,x0.] c= dom f
ex g st g in [.x0-r1,x0.] & f.g = g2;
defpred P[Nat,set] means $2 in [.x0-r/($1+1),x0.] & $2 in dom f & f.$2 = g2;
A4: for n ex g be real number st P[n,g]
proof let n;
A5: 0 <= n by NAT_1:18;
then 0 < n + 1 by NAT_1:38;
then A6: 0 < r/(n+1) by A2,SEQ_2:6;
0 + 1 <= n + 1 by A5,REAL_1:55;
then r/(n+1) <= r/1 by A2,REAL_2:201;
then A7: x0 - r <= x0 - r/(n+1) by REAL_1:92;
x0 - r/(n+1) <= x0 by A6,SQUARE_1:29;
then x0 - r/(n+1) in {g1: x0 - r <= g1 & g1 <= x0} by A7;
then A8: x0 - r/(n+1) in [.x0 - r, x0.] by RCOMP_1:def 1;
x0 - r <= x0 by A2,SQUARE_1:29;
then x0 in [.x0 - r,x0.] by RCOMP_1:15;
then [.x0 - r/(n+1),x0.] c= [.x0 - r,x0.] by A8,RCOMP_1:16;
then A9: [.x0 - r/(n+1),x0.] c= dom f by A2,XBOOLE_1:1;
then consider g such that A10: g in [.x0-r/(n+1),x0.] & f.g = g2 by A3,A6;
take g;
thus thesis by A9,A10;
end;
consider a such that
A11: for n holds P[n,a.n] from RealSeqChoice(A4);
deffunc F(Nat) = x0 - r/($1+1);
consider b such that
A12: for n holds b.n = F(n) from ExRealSeq;
deffunc F(Nat) = x0;
consider d such that
A13: for n holds d.n = F(n) from ExRealSeq;
A14: b is convergent & lim b = x0 by A12,FCONT_3:13;
now let n;
d.n = x0 & d.(n+1) = x0 by A13;
hence d.n = d.(n+1);
end;
then A15: d is constant by SEQM_3:16;
then A16: d is convergent by SEQ_4:39;
A17: lim d = d.0 by A15,SEQ_4:41
.= x0 by A13;
A18: now let n;
a.n in [.x0 - r/(n+1), x0.] by A11;
then a.n in {g1: x0 - r/(n+1) <= g1 & g1 <= x0} by RCOMP_1:def 1;
then ex g1 st g1 = a.n & x0 - r/(n+1) <= g1 & g1 <=x0;
hence b.n <= a.n & a.n <= d.n by A12,A13;
end;
then A19: a is convergent by A14,A16,A17,SEQ_2:33;
A20: lim a = x0 by A14,A16,A17,A18,SEQ_2:34;
A21: rng a c= left_open_halfline(x0) /\ dom f & rng a c= dom f
proof
thus A22: rng a c= left_open_halfline(x0) /\ dom f
proof
let x;
assume x in rng a;
then consider n such that A23: x=a.n by RFUNCT_2:9;
A24: a.n in [.x0-r/(n+1),x0.] & a.n in dom f by A11;
then a.n in {g1: x0 - r/(n+1) <= g1 & g1 <= x0} by RCOMP_1:def 1;
then A25: ex g1 st g1 = a.n & x0 - r/(n+1) <= g1 & g1 <=x0;
a.n <> x0 by A1,A11;
then a.n < x0 by A25,REAL_1:def 5;
then a.n in {g1: g1 < x0};
then a.n in left_open_halfline(x0) by PROB_1:def 15;
hence thesis by A23,A24,XBOOLE_0:def 3;
end;
left_open_halfline(x0) /\ dom f c= dom f by XBOOLE_1:17;
hence thesis by A22,XBOOLE_1:1;
end;
A26: for n holds (f*a).n = g2
proof let n;
thus (f*a).n = f.(a.n) by A21,RFUNCT_2:21
.= g2 by A11;
end;
now let n;
(f*a).n = g2 & (f*a).(n+1) = g2 by A26;
hence (f*a).n =(f*a).(n+1);
end;
then f*a is constant by SEQM_3:16;
then lim (f*a) = (f*a).0 by SEQ_4:41
.= g2 by A26;
hence contradiction by A1,A19,A20,A21,Def1;
end;
theorem Th7:
f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0
proof
assume A1: f is_right_differentiable_in x0;
then consider r such that A2: r>0 & [.x0 ,x0 + r.] c= dom f by Def3;
A3: x0 in dom f
proof
x0 + 0 <= x0 +r by A2,REAL_1:55;
then x0 in [.x0 , x0 + r.] by RCOMP_1:15;
hence x0 in dom f by A2;
end;
for a st rng a c= right_open_halfline(x0) /\ dom f & a is convergent &
lim a = x0 holds f*a is convergent & f.x0 = lim(f*a)
proof let a such that
A4: rng a c= right_open_halfline(x0) /\ dom f & a is convergent & lim a =
x0;
consider r such that A5:r > 0 & [.x0 , x0 + r.] c= dom f by A1,Def3;
x0 + 0 < x0 + r by A5,REAL_1:53;
then consider n0 be Nat such that
A6: for k st k>=n0 holds a.k < x0 +r by A4,LIMFUNC2:2;
A7: for n holds (a^\n0).n in [.x0 , x0 + r.]
proof
let n; 0 <= n & 0 + n0 = n0 by NAT_1:18;
then n0 <= n0 + n by AXIOMS:24;
then a.(n + n0) <= x0 +r by A6;
then A8:(a^\n0).n <= x0 + r by SEQM_3:def 9;
a.(n + n0) in rng a by RFUNCT_2:10;
then (a^\n0).n in rng a by SEQM_3:def 9;
then (a^\n0).n in right_open_halfline(x0) by A4,XBOOLE_0:def 3;
then (a^\n0).n in {g:x0 < g} by LIMFUNC1:def 3;
then ex g st g = (a^\n0).n & x0 < g;
then (a^\n0).n in {g: x0 <= g & g <= x0 + r} by A8;
hence (a^\n0).n in [.x0 ,x0 + r.] by RCOMP_1:def 1;
end;
deffunc F(Nat) = x0;
consider b such that A9: for n holds b.n = F(n) from ExRealSeq;
deffunc F(Nat) = a.$1-b.$1;
consider d such that A10: for n holds d.n = F(n) from ExRealSeq;
A11: b is constant by A9,SEQM_3:def 6;
then A12: b is convergent by SEQ_4:39;
A13: lim b = b.0 by A11,SEQ_4:41
.= x0 by A9;
A14: d = a - b by A10,RFUNCT_2:6;
then A15: d is convergent by A4,A12,SEQ_2:25;
lim d = x0 - x0 by A4,A12,A13,A14,SEQ_2:26
.= 0 by XCMPLX_1:14;
then A16: d^\n0 is convergent & lim (d^\n0) = 0 by A15,SEQ_4:33;
A17: for n holds d.n > 0 & d.n <> 0
proof let n;
A18: d.n = a.n - b.n by A10;
a.n in rng a by RFUNCT_2:10;
then a.n in right_open_halfline(x0) by A4,XBOOLE_0:def 3;
then a.n in { r1: x0 < r1 } by LIMFUNC1:def 3;
then ex r1 st r1 = a.n & x0 < r1;
then a.n - x0 > x0 - x0 by REAL_1:54;
then A19: d.n > x0 - x0 by A9,A18;
hence d.n > 0 by XCMPLX_1:14;
thus thesis by A19,XCMPLX_1:14;
end;
A20: for n holds (d^\n0).n > 0
proof let n;
(d^\n0).n = d.(n + n0) by SEQM_3:def 9;
hence (d^\n0).n > 0 by A17;
end;
then for n holds (d^\n0).n <>0;
then d ^\n0 is_not_0 by SEQ_1:7;
then reconsider h = d^\n0 as convergent_to_0 Real_Sequence by A16,FDIFF_1:
def 1;
A21: b^\n0 is_subsequence_of b by SEQM_3:47;
b is constant by A9,SEQM_3:def 6;
then reconsider c = b^\n0 as constant Real_Sequence by A21,SEQM_3:54;
A22: rng c = {x0}
proof
thus rng c c= {x0}
proof let x;
assume x in rng c; then consider n such that
A23: x = (b^\n0).n by RFUNCT_2:9;
x = b.(n + n0) by A23,SEQM_3:def 9;
then x = x0 by A9;
hence x in {x0} by TARSKI:def 1;
end;
let x; assume x in {x0};
then A24: x = x0 by TARSKI:def 1;
c.0 = b.(0 + n0) by SEQM_3:def 9
.= x by A9,A24;
hence x in rng c by RFUNCT_2:9;
end;
rng (h + c) c= [.x0,x0 + r.]
proof let x; assume x in rng(h + c); then consider n such that
A25: x = (h+c).n by RFUNCT_2:9;
(h+c).n=((a - b +b)^\n0).n by A14,SEQM_3:37
.= (a - b + b) .(n + n0) by SEQM_3:def 9
.= (a - b).(n + n0) + b.(n + n0) by SEQ_1:11
.= a.(n + n0) - b.(n + n0) + b.(n + n0) by RFUNCT_2:6
.= a.(n + n0) by XCMPLX_1:27
.= (a^\n0).n by SEQM_3:def 9;
hence x in [.x0 ,x0 + r.] by A7,A25;
end;
then rng (h + c) c= dom f by A5,XBOOLE_1:1;
then A26: h"(#)(f*(h+c) - f*c) is convergent by A1,A20,A22,Def3;
then A27: lim (h(#)(h"(#)(f*(h+c) - f*c)))=0*lim(h"(#)
(f*(h+c) - f*c)) by A16,SEQ_2:29
.=0;
now let n;
A28: h.n<>0 by A20;
thus (h(#)(h"(#)(f*(h+c) - f*c))).n=h.n *(h"(#)
(f*(h+c) - f*c)).n by SEQ_1:12
.= h.n*((h").n*(f*(h+c) - f*c).n) by SEQ_1:12
.= h.n*(((h.n)")*(f*(h+c) - f*c).n) by SEQ_1:def 8
.= h.n*((h.n)")*(f*(h+c) - f*c).n by XCMPLX_1:4
.= 1*(f*(h+c) - f*c).n by A28,XCMPLX_0:def 7
.= (f*(h+c) - f*c).n;
end;
then A29: h(#)(h"(#)(f*(h+c) - f*c))=f*(h+c)-f*c by FUNCT_2:113;
then A30: f*(h+c)-f*c is convergent by A16,A26,SEQ_2:28;
A31: now let g be real number such that A32: 0<g;
take n=0; let m such that n<=m;
x0 + 0 <= x0 +r by A5,REAL_1:55;
then x0 in [.x0 , x0 + r.] by RCOMP_1:15;
then rng c c= dom f by A5,A22,ZFMISC_1:37;
then abs((f*c).m-f.x0) = abs(f.(c.m)-f.x0) by RFUNCT_2:21
.= abs(f.(b.(m+n0))-f.x0) by SEQM_3:def 9
.= abs(f.x0-f.x0) by A9
.= abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:7;
hence abs((f*c).m-f.x0)<g by A32;
end;
then A33: f*c is convergent by SEQ_2:def 6;
then A34: lim(f*c)=f.x0 by A31,SEQ_2:def 7;
A35: f*(h+c)-f*c+f*c is convergent by A30,A33,SEQ_2:19;
A36: lim(f*(h+c)-f*c+f*c) = 0+f.x0 by A27,A29,A30,A33,A34,SEQ_2:20
.= f.x0;
now let n;
thus (f*(h+c)-f*c+f*c).n=(f*(h+c)-f*c).n+(f*c).n by SEQ_1:11
.= (f*(h+c)).n-(f*c).n+(f*c).n by RFUNCT_2:6
.= (f*(h+c)).n by XCMPLX_1:27;
end;
then A37: f*(h+c)-f*c+(f*c)=f*(h+c) by FUNCT_2:113;
A38: rng a c= dom f
proof let x; assume x in rng a; hence thesis by A4,XBOOLE_0:def 3;
end;
now let n;
thus (h+c).n=((a-b+b)^\n0).n by A14,SEQM_3:37
.= (a-b+b).(n+n0) by SEQM_3:def 9
.= (a-b).(n+n0)+b.(n+n0) by SEQ_1:11
.= a.(n+n0)-b.(n+n0)+b.(n+n0) by RFUNCT_2:6
.= a.(n+n0) by XCMPLX_1:27
.= (a^\n0).n by SEQM_3:def 9;
end;
then A39: f*(h+c)-f*c+(f*c)=f*(a^\n0) by A37,FUNCT_2:113
.= (f*a)^\n0 by A38,RFUNCT_2:22;
hence f*a is convergent by A35,SEQ_4:35;
thus f.x0=lim(f*a) by A35,A36,A39,SEQ_4:36;
end;
hence thesis by A3,Def2;
end;
theorem Th8:
f is_Rcontinuous_in x0 & f.x0 <> g2 & (ex r st r>0 & [.x0 , x0+r.] c= dom f)
implies ex r1 st r1>0 & [.x0 , x0+r1.] c= dom f &
for g st g in [.x0 , x0+r1.] holds f.g <> g2
proof
assume A1: f is_Rcontinuous_in x0 & f.x0 <> g2;
given r such that A2: r>0 & [.x0 , x0+r.] c= dom f;
assume A3: for r1 st r1>0 & [.x0 , x0+r1.] c= dom f
ex g st g in [.x0 , x0+r1.] & f.g = g2;
defpred P[Nat,set] means
$2 in [.x0, x0+r/($1+1).] & $2 in dom f & f.$2 = g2;
A4: for n ex g be real number st P[n,g]
proof let n;
A5:0 <= n by NAT_1:18; then A6: 0 < n+1 by NAT_1:38;
then A7: r/(n+1) > 0 by A2,SEQ_2:6;
x0 + 0 <= x0 +r by A2,REAL_1:55;
then A8: x0 in [.x0 , x0 + r.] by RCOMP_1:15;
0 + 1 <= n + 1 by A5,REAL_1:55;
then r/(n+1) <= r/1 by A2,REAL_2:201;
then A9: x0 + r/(n+1) <= x0 + r by REAL_1:55;
0 <= r/(n+1) & x0 + 0 =x0 by A2,A6,SEQ_2:6;
then x0 <= x0 + r/(n+1) by REAL_1:55;
then x0 + r/(n+1) in {g1:x0 <= g1 & g1 <= x0+r} by A9;
then x0 +r/(n+1) in [.x0,x0+r.] by RCOMP_1:def 1;
then [.x0,x0+r/(n+1).] c= [.x0,x0+r.] by A8,RCOMP_1:16;
then A10: [.x0,x0+r/(n+1).] c= dom f by A2,XBOOLE_1:1;
then consider g such that
A11: g in [.x0,x0+r/(n+1).] & f.g = g2 by A3,A7;
take g;
thus thesis by A10,A11;
end;
consider a such that
A12: for n holds P[n,a.n] from RealSeqChoice(A4);
deffunc F(Nat) = x0;
consider b such that A13:for n holds b.n = F(n) from ExRealSeq;
now
let n;
b.n = x0 & b.(n+1) = x0 by A13;
hence b.n = b.(n+1);
end;
then A14:b is constant by SEQM_3:16;
then A15:b is convergent by SEQ_4:39;
A16:lim b = b.0 by A14,SEQ_4:41
.=x0 by A13;
deffunc F(Nat) = x0+r/($1+1);
consider d such that A17:for n holds d.n = F(n) from ExRealSeq;
A18:d is convergent & lim d = x0 by A17,FCONT_3:14;
A19: now let n;
a.n in [.x0 , x0 + r/(n+1).] by A12;
then a.n in{g1: x0<=g1 & g1<=x0+ r/(n+1)} by RCOMP_1:def 1;
then ex g1 st g1=a.n & x0<=g1 & g1<=x0+ r/(n+1);
hence b.n <=a.n & a.n <= d.n by A13,A17;
end;
then A20: a is convergent by A15,A16,A18,SEQ_2:33;
A21: lim a = x0 by A15,A16,A18,A19,SEQ_2:34;
A22: rng a c= right_open_halfline(x0) /\ dom f & rng a c= dom f
proof
thus A23:rng a c= right_open_halfline(x0) /\ dom f
proof
let x;
assume x in rng a;
then consider n such that A24: x = a.n by RFUNCT_2:9;
A25:a.n in [.x0 , x0 + r/(n+1).] & a.n in dom f by A12;
then a.n in{g1: x0<=g1 & g1<=x0+ r/(n+1)} by RCOMP_1:def 1;
then A26: ex g1 st g1=a.n & x0<=g1 & g1<=x0+ r/(n+1);
x0 <> a.n by A1,A12;
then x0 < a.n by A26,REAL_1:def 5;
then a.n in {g1:x0 <g1};
then a.n in right_open_halfline(x0)by LIMFUNC1:def 3;
hence thesis by A24,A25,XBOOLE_0:def 3;
end;
right_open_halfline(x0) /\ dom f c= dom f by XBOOLE_1:17;
hence thesis by A23,XBOOLE_1:1;
end;
A27: for n holds (f*a).n = g2
proof
let n;thus
g2 =f.(a.n) by A12
.=(f*a).n by A22,RFUNCT_2:21;
end;
now let n;
(f*a).n=g2 & (f*a).(n+1) = g2 by A27;
hence (f*a).n=(f*a).(n+1);
end;
then f*a is constant by SEQM_3:16;
then lim (f*a) = (f*a).0 by SEQ_4:41
.= g2 by A27;
hence contradiction by A1,A20,A21,A22,Def2;
end;
definition let x0,f;
assume A1:f is_left_differentiable_in x0;
func Ldiff (f,x0) -> Real means: Def5:
for h,c st rng c = {x0} & rng (h + c) c= dom f & (for n holds h.n <0) holds
it =lim (h"(#)(f*(h + c) - f*c));
existence
proof
ex r st r > 0 & [.x0 - r, x0.] c= dom f by A1,Def4;
then consider h1,c1 such that
A2: rng c1 = {x0} & rng (h1 + c1) c= dom f & for n holds h1.n < 0 by Th1;
take lim (h1"(#)(f*(h1 + c1) - f*c1));
A3: {x0} c= dom f
proof
let x; assume x in {x0};
then A4: x = x0 by TARSKI:def 1;
consider r such that A5: r > 0 & [.x0 - r,x0.] c= dom f by A1,Def4;
x0 - r <= x0 by A5,SQUARE_1:29;
then x0 in [.x0 - r,x0.] by RCOMP_1:15;
hence thesis by A4,A5;
end;
let h,c such that
A6: rng c = {x0} & rng (h + c) c= dom f & (for n holds h.n <0);
A7: for h,c st rng c = {x0} & rng (h + c) c= dom f & (for n holds h.n <0)
holds h"(#)(f*(h + c) - f*c) is convergent by A1,Def4;
c1 = c by A2,A6,FDIFF_2:5;
hence thesis by A2,A3,A6,A7,Th3;
end;
uniqueness
proof let g1,g2 such that
A8: (for h,c st rng c = {x0} & rng (h + c) c= dom f & (for n holds h.n <0)
holds g1=lim (h"(#)(f*(h + c) - f*c))) &
for h,c st rng c = {x0} & rng (h + c) c= dom f & (for n holds h.n <0)
holds g2=lim (h"(#)(f*(h + c) - f*c));
ex r st r > 0 & [.x0 - r, x0.] c= dom f by A1,Def4;
then consider h,c such that
A9: rng c = {x0} & rng (h + c) c= dom f & for n holds h.n < 0 by Th1;
g1 = lim (h"(#)(f*(h + c) - f*c)) by A8,A9;
hence thesis by A8,A9;
end;
end;
definition let x0 ,f;
assume A1: f is_right_differentiable_in x0;
func Rdiff(f,x0) -> Real means :Def6:
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n > 0) holds
it=lim (h"(#)(f*(h + c) - f*c));
existence
proof
ex r st r>0 & [.x0,x0+r.] c=dom f by A1,Def3;
then consider h,c such that
A2: rng c = {x0} & rng (h+c) c= dom f & for n holds h.n>0 by Th2;
take lim(h"(#)(f*(h+c) - f*c));
let h1,c1 such that
A3: rng c1 ={x0} & rng(h1 + c1) c=dom f & for n holds h1.n>0;
A4: for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n>0) holds
h"(#)(f*(h+c) - f*c) is convergent by A1,Def3;
A5: {x0} c= dom f
proof let x; assume x in {x0};
then A6: x = x0 by TARSKI:def 1; consider r such that
A7: r>0 & [.x0,x0+r.] c= dom f by A1,Def3;
x0 + 0 <= x0 + r by A7,REAL_1:55;
then x0 in [.x0,x0+r.] by RCOMP_1:15;
hence thesis by A6,A7;
end;
c1 = c by A2,A3,FDIFF_2:5;
hence thesis by A2,A3,A4,A5,Th4;
end;
uniqueness
proof let g1,g2 such that
A8: (for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n > 0)
holds g1=lim (h"(#)(f*(h + c) - f*c))) &
for h,c st rng c ={x0} & rng (h+c) c= dom f & (for n holds h.n > 0)
holds g2=lim (h"(#)(f*(h + c) - f*c));
ex r st r>0 & [.x0,x0 + r.] c=dom f by A1,Def3;
then consider h,c such that
A9: rng c ={x0} & rng (h+c) c= dom f & for n holds h.n >0 by Th2;
g1 = lim (h"(#)(f*(h + c) - f*c)) by A8,A9;
hence thesis by A8,A9;
end;
end;
theorem Th9:
f is_left_differentiable_in x0 & Ldiff(f,x0) = g iff
(ex r st 0 < r & [.x0 -r,x0.] c= dom f) &
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n < 0)
holds h"(#)(f*(h + c) - f*c) is convergent & lim(h"(#)(f*(h + c) - f*c)) = g
proof
thus f is_left_differentiable_in x0 & Ldiff(f,x0) = g implies
(ex r st 0 < r & [.x0 -r,x0.] c= dom f) &
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n < 0)
holds h"(#)(f*(h + c) - f*c) is convergent & lim(h"(#)(f*(h + c) - f*c)) = g
by Def4,Def5;
thus (ex r st 0 <r & [.x0 -r,x0.] c= dom f) &
(for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n < 0)
holds h"(#)(f*(h + c) - f*c) is convergent & lim(h"(#)(f*(h + c) - f*c)) = g)
implies f is_left_differentiable_in x0 & Ldiff(f,x0) = g
proof
assume A1: (ex r st 0 < r & [.x0 -r,x0.] c= dom f) &
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n < 0)
holds h"(#)(f*(h + c) - f*c) is convergent & lim(h"(#)
(f*(h + c) - f*c)) = g;
then for h,c holds ( rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n
< 0))
implies h"(#)(f*(h + c) - f*c) is convergent;
hence A2: f is_left_differentiable_in x0 by A1,Def4;
for h,c holds ( rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n < 0
)
)
implies lim(h"(#)(f*(h + c) - f*c)) = g by A1;
hence thesis by A2,Def5;
end;
end;
theorem
f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies
f1 + f2 is_left_differentiable_in x0 &
Ldiff(f1+f2,x0) = Ldiff(f1,x0) + Ldiff(f2,x0)
proof assume
A1: f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0;
then consider r1 such that
A2: 0 < r1 & [.x0 -r1,x0.] c= dom f1 by Def4;
consider r2 such that
A3: 0 < r2 & [.x0 -r2,x0.] c= dom f2 by A1,Def4;
set r = min(r1,r2);
A4: 0 < r by A2,A3,SQUARE_1:38;
then A5: x0 - r <= x0 by PROB_1:2;
r <= r1 by SQUARE_1:35;
then A6: x0 - r1 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r1 <= g & g <= x0 } by A5;
then A7: x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
x0 - r1 <= x0 by A5,A6,AXIOMS:22;
then x0 in [.x0 - r1,x0.] by RCOMP_1:15;
then A8: [.x0 - r,x0.] c= [.x0 - r1,x0.] by A7,RCOMP_1:16;
r <= r2 by SQUARE_1:35;
then A9: x0 - r2 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r2 <= g & g <= x0 } by A5;
then A10: x0 - r in [.x0 - r2,x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A5,A9,AXIOMS:22;
then x0 in [.x0 - r2,x0.] by RCOMP_1:15;
then A11: [.x0 - r,x0.] c= [.x0 - r2,x0.] by A10,RCOMP_1:16;
A12: [.x0 - r,x0.] c= dom f1 by A2,A8,XBOOLE_1:1;
[.x0 - r,x0.] c= dom f2 by A3,A11,XBOOLE_1:1;
then A13: [.x0 - r,x0.] c= dom f1 /\ dom f2 by A12,XBOOLE_1:19;
then A14: [.x0 - r,x0.] c= dom (f1 + f2) by SEQ_1:def 3;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1 + f2) &
(for n holds h.n < 0) holds
h"(#)((f1 + f2)*(h + c) - (f1 + f2)*c) is convergent &
lim(h"(#)((f1 + f2)*(h + c) - (f1 + f2)*c)) = Ldiff(f1,x0) + Ldiff(f2,x0)
proof let h,c;
assume that
A15: rng c = {x0} and
A16: rng (h+c) c= dom (f1 + f2) and
A17: for n holds h.n < 0;
A18: rng (h + c) c= dom f1 /\ dom f2 by A16,SEQ_1:def 3;
dom f1 /\ dom f2 c= dom f1 & dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17
;
then A19: rng (h + c) c= dom f1 & rng (h + c) c= dom f2 by A18,XBOOLE_1:1;
Ldiff(f1,x0) = Ldiff(f1,x0);
then A20: h"(#)(f1*(h + c) - f1*c) is convergent &
lim(h"(#)(f1*(h + c) - f1*c)) = Ldiff(f1,x0) by A1,A15,A17,A19,Th9;
Ldiff(f2,x0) = Ldiff(f2,x0);
then A21: h"(#)(f2*(h + c) - f2*c) is convergent &
lim(h"(#)(f2*(h + c) - f2*c)) = Ldiff(f2,x0) by A1,A15,A17,A19,Th9;
then A22: (h"(#)(f1*(h + c) - f1*c) + h"(#)
(f2*(h + c) - f2*c)) is convergent
by A20,SEQ_2:19;
A23: (h"(#)(f1*(h + c) - f1*c) + h"(#)(f2*(h + c) - f2*c))
= h"(#)(f1*(h + c) - f1*c + (f2*(h + c) - f2*c)) by SEQ_1:24;
A24: now let n;
A25: rng c c= dom f1 /\ dom f2
proof let x;
assume x in rng c;
then A26: x = x0 by A15,TARSKI:def 1;
x0 in [.x0 - r,x0.] by A5,RCOMP_1:15;
hence thesis by A13,A26;
end;
thus
(f1*(h + c) - f1*c + (f2*(h + c) - f2*c)).n =
(f1*(h + c) - f1*c).n + (f2*(h + c) - f2*c).n by SEQ_1:11
.=(f1*(h+c) + (-(f1*c))).n + (f2*(h+c) - f2*c).n by SEQ_1:15
.=(f1*(h+c) + (-(f1*c))).n + (f2*(h+c) + (-(f2*c))).n by SEQ_1:15
.=(f1*(h+c)).n + (-(f1*c)).n + (f2*(h+c) + (-(f2*c))).n by SEQ_1:11
.=(f1*(h+c)).n + (-(f1*c)).n + ((f2*(h+c)).n + (-(f2*c)).n) by SEQ_1:11
.=(f1*(h+c)).n + ((-(f1*c)).n + ((f2*(h+c)).n + (-(f2*c)).n)) by XCMPLX_1:
1
.=(f1*(h+c)).n + (((f2*(h+c)).n + (-(f1*c)).n) + (-(f2*c)).n) by XCMPLX_1:
1
.=(f1*(h+c)).n + ((f2*(h+c)).n + (-(f1*c)).n) + (-(f2*c)).n by XCMPLX_1:1
.=(f1*(h+c)).n + (f2*(h+c)).n + (-(f1*c)).n + (-(f2*c)).n by XCMPLX_1:1
.=(f1*(h+c)).n + (f2*(h + c)).n+ ((-(f1*c)).n +(-(f2*c)).n) by XCMPLX_1:1
.=(f1*(h+c)).n + (f2*(h + c)).n + (-(f1*c).n + (-(f2*c)).n) by SEQ_1:14
.=(f1*(h+c)).n + (f2*(h + c)).n + (-(f1*c).n + -(f2*c).n) by SEQ_1:14
.=(f1*(h+c)).n + (f2*(h + c)).n + -((f1*c).n + (f2*c).n) by XCMPLX_1:140
.=(f1*(h+c)).n + (f2*(h + c)).n - ((f1*c).n + (f2*c).n) by XCMPLX_0:def 8
.=(f1*(h+c) + f2*(h + c)).n - ((f1*c).n + (f2*c).n) by SEQ_1:11
.=(f1*(h+c) + f2*(h + c)).n - ((f1*c + f2*c).n) by SEQ_1:11
.=(f1*(h+c) + f2*(h + c) - (f1*c + f2*c)).n by RFUNCT_2:6
.=((f1 + f2)*(h + c) - (f1*c + f2*c)).n by A18,RFUNCT_2:23
.=((f1 + f2)*(h + c) - (f1 + f2)*c).n by A25,RFUNCT_2:23;
end;
then A27: f1*(h + c) - f1*c + (f2*(h + c) - f2*c) =
(f1 + f2)*(h + c) - (f1 + f2)*c by FUNCT_2:113;
thus h"(#)((f1 + f2)*(h + c) - (f1 + f2)*c) is convergent by A22,A23,A24,
FUNCT_2:113;
thus lim (h"(#)((f1 + f2)*(h + c) - (f1 + f2)*c)) =
Ldiff(f1,x0) + Ldiff(f2,x0) by A20,A21,A23,A27,SEQ_2:20;
end;
hence thesis by A4,A14,Th9;
end;
theorem
f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies
f1 - f2 is_left_differentiable_in x0 &
Ldiff(f1-f2,x0) = Ldiff(f1,x0) - Ldiff(f2,x0)
proof assume
A1: f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0;
then consider r1 such that
A2: 0 < r1 & [.x0 -r1,x0.] c= dom f1 by Def4;
consider r2 such that
A3: 0 < r2 & [.x0 -r2,x0.] c= dom f2 by A1,Def4;
set r = min(r1,r2);
A4: 0 < r by A2,A3,SQUARE_1:38;
then A5: x0 - r <= x0 by PROB_1:2;
r <= r1 by SQUARE_1:35;
then A6: x0 - r1 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r1 <= g & g <= x0 } by A5;
then A7: x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
x0 - r1 <= x0 by A5,A6,AXIOMS:22;
then x0 in [.x0 - r1,x0.] by RCOMP_1:15;
then A8: [.x0 - r,x0.] c= [.x0 - r1,x0.] by A7,RCOMP_1:16;
r <= r2 by SQUARE_1:35;
then A9: x0 - r2 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r2 <= g & g <= x0 } by A5;
then A10: x0 - r in [.x0 - r2,x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A5,A9,AXIOMS:22;
then x0 in [.x0 - r2,x0.] by RCOMP_1:15;
then A11: [.x0 - r,x0.] c= [.x0 - r2,x0.] by A10,RCOMP_1:16;
A12: [.x0 - r,x0.] c= dom f1 by A2,A8,XBOOLE_1:1;
[.x0 - r,x0.] c= dom f2 by A3,A11,XBOOLE_1:1;
then A13: [.x0 - r,x0.] c= dom f1 /\ dom f2 by A12,XBOOLE_1:19;
then A14: [.x0 - r,x0.] c= dom (f1 - f2) by SEQ_1:def 4;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1 - f2) &
(for n holds h.n < 0) holds
h"(#)((f1 - f2)*(h + c) - (f1 - f2)*c) is convergent &
lim(h"(#)((f1 - f2)*(h + c) - (f1 - f2)*c)) = Ldiff(f1,x0) - Ldiff(f2,x0)
proof let h,c;
assume that
A15: rng c = {x0} and
A16: rng (h+c) c= dom (f1 - f2) and
A17: for n holds h.n < 0;
A18: rng (h + c) c= dom f1 /\ dom f2 by A16,SEQ_1:def 4;
dom f1 /\ dom f2 c= dom f1 & dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17
;
then A19: rng (h + c) c= dom f1 & rng (h + c) c= dom f2 by A18,XBOOLE_1:1;
Ldiff(f1,x0) = Ldiff(f1,x0);
then A20: h"(#)(f1*(h + c) - f1*c) is convergent &
lim(h"(#)(f1*(h + c) - f1*c)) = Ldiff(f1,x0) by A1,A15,A17,A19,Th9;
Ldiff(f2,x0) = Ldiff(f2,x0);
then A21: h"(#)(f2*(h + c) - f2*c) is convergent &
lim(h"(#)(f2*(h + c) - f2*c)) = Ldiff(f2,x0) by A1,A15,A17,A19,Th9;
then A22: (h"(#)(f1*(h + c) - f1*c) - h"(#)
(f2*(h + c) - f2*c)) is convergent
by A20,SEQ_2:25;
A23: (h"(#)(f1*(h + c) - f1*c) - h"(#)(f2*(h + c) - f2*c))
= h"(#)(f1*(h + c) - f1*c - (f2*(h + c) - f2*c)) by SEQ_1:29;
A24: now let n;
A25: rng c c= dom f1 /\ dom f2
proof
let x;
assume x in rng c;
then A26: x = x0 by A15,TARSKI:def 1;
x0 in [.x0 - r,x0.] by A5,RCOMP_1:15;
hence thesis by A13,A26;
end;
thus
(f1*(h + c) - f1*c - (f2*(h + c) - f2*c)).n =
(f1*(h + c) - f1*c).n - (f2*(h + c) - f2*c).n by RFUNCT_2:6
.=(f1*(h + c)).n - (f1*c).n - (f2*(h + c) - (f2*c)).n by RFUNCT_2:6
.=(f1*(h + c)).n - (f1*c).n - ((f2*(h + c)).n - (f2*c).n) by RFUNCT_2:6
.=(f1*(h + c)).n - (f1*c).n - (f2*(h + c)).n + (f2*c).n by XCMPLX_1:37
.=(f1*(h + c)).n - (f2*(h + c)).n - (f1*c).n + (f2*c).n by XCMPLX_1:21
.=(f1*(h + c)).n - (f2*(h + c)).n - ((f1*c).n - (f2*c).n) by XCMPLX_1:37
.=(f1*(h + c) - f2*(h + c)).n - ((f1*c).n - (f2*c).n) by RFUNCT_2:6
.=(f1*(h + c) - f2*(h + c)).n - ((f1*c - f2*c).n) by RFUNCT_2:6
.=(f1*(h + c) - f2*(h + c) - (f1*c - f2*c)).n by RFUNCT_2:6
.=((f1 - f2)*(h + c) - (f1*c - f2*c)).n by A18,RFUNCT_2:23
.=((f1 - f2)*(h + c) - (f1 - f2)*c).n by A25,RFUNCT_2:23;
end;
then A27: f1*(h + c) - f1*c - (f2*(h + c) - f2*c) =
(f1 - f2)*(h + c) - (f1 - f2)*c by FUNCT_2:113;
thus h"(#)((f1 - f2)*(h + c) - (f1 - f2)*c) is convergent by A22,A23,A24,
FUNCT_2:113;
thus thesis by A20,A21,A23,A27,SEQ_2:26;
end;
hence thesis by A4,A14,Th9;
end;
theorem
f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies
f1(#)f2 is_left_differentiable_in x0 &
Ldiff(f1(#)f2,x0) = Ldiff(f1,x0)*f2.x0 + Ldiff(f2,x0)*f1.x0
proof
assume A1: f1 is_left_differentiable_in x0 &
f2 is_left_differentiable_in x0;
then consider r1 such that
A2: 0 < r1 & [.x0 -r1,x0.] c= dom f1 by Def4;
consider r2 such that
A3: 0 < r2 & [.x0 -r2,x0.] c= dom f2 by A1,Def4;
set r = min(r1,r2);
A4: 0 < r by A2,A3,SQUARE_1:38;
then A5: x0 - r <= x0 by PROB_1:2;
r <= r1 by SQUARE_1:35;
then A6: x0 - r1 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r1 <= g & g <= x0 } by A5;
then A7: x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
x0 - r1 <= x0 by A5,A6,AXIOMS:22;
then x0 in [.x0 - r1,x0.] by RCOMP_1:15;
then A8: [.x0 - r,x0.] c= [.x0 - r1,x0.] by A7,RCOMP_1:16;
r <= r2 by SQUARE_1:35;
then A9: x0 - r2 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r2 <= g & g <= x0 } by A5;
then A10: x0 - r in [.x0 - r2,x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A5,A9,AXIOMS:22;
then x0 in [.x0 - r2,x0.] by RCOMP_1:15;
then A11: [.x0 - r,x0.] c= [.x0 - r2,x0.] by A10,RCOMP_1:16;
A12: [.x0 - r,x0.] c= dom f1 by A2,A8,XBOOLE_1:1;
A13: [.x0 - r,x0.] c= dom f2 by A3,A11,XBOOLE_1:1;
then [.x0 - r,x0.] c= dom f1 /\ dom f2 by A12,XBOOLE_1:19;
then A14: [.x0 - r,x0.] c= dom (f1(#)f2) by SEQ_1:def 5;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1(#)f2) &
(for n holds h.n < 0) holds
h"(#)((f1(#)f2)*(h + c) - (f1(#)f2)*c) is convergent &
lim(h"(#)((f1(#)f2)*(h + c) - (f1(#)f2)*c)) =
Ldiff(f1,x0)*f2.x0 + Ldiff(f2,x0)*f1.x0
proof let h,c;
assume that
A15: rng c = {x0} and
A16: rng (h+c) c= dom (f1(#)f2) and
A17: for n holds h.n < 0;
A18: rng (h + c) c= dom f1 /\ dom f2 by A16,SEQ_1:def 5;
dom f1 /\ dom f2 c= dom f1 & dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17
;
then A19: rng (h + c) c= dom f1 & rng (h + c) c= dom f2 by A18,XBOOLE_1:1;
Ldiff(f1,x0) = Ldiff(f1,x0);
then A20: h"(#)(f1*(h + c) - f1*c) is convergent &
lim(h"(#)(f1*(h + c) - f1*c)) = Ldiff(f1,x0) by A1,A15,A17,A19,Th9;
Ldiff(f2,x0) = Ldiff(f2,x0);
then A21: h"(#)(f2*(h + c) - f2*c) is convergent &
lim(h"(#)(f2*(h + c) - f2*c)) = Ldiff(f2,x0) by A1,A15,A17,A19,Th9;
A22: for m holds c.m = x0
proof
let m; c.m in rng c by RFUNCT_2:10;
hence c.m = x0 by A15,TARSKI:def 1;
end;
0 <= r by A2,A3,SQUARE_1:38;
then x0 - r <= x0 by PROB_1:2;
then A23: x0 in [.x0 -r,x0.] by RCOMP_1:15;
then A24: x0 in dom f1 by A12;
A25: rng c c= dom f1
proof let x;
assume x in rng c;
hence x in dom f1 by A15,A24,TARSKI:def 1;
end;
A26: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f1*c).m - f1.x0) < g
proof let g be real number such that A27: 0 < g;
take n = 0;
let m such that n <= m;
abs((f1*c).m - f1.x0) = abs(f1.(c.m) - f1.x0) by A25,RFUNCT_2:21
.= abs(f1.x0 - f1.x0) by A22
.= abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f1*c).m - f1.x0) < g by A27;
end;
A28: h is convergent & lim h = 0 by FDIFF_1:def 1;
A29: f1*c is convergent by A26,SEQ_2:def 6;
then A30: lim(f1*c) = f1.x0 by A26,SEQ_2:def 7;
A31: h"(#)(f1*(h + c) - f1*c) is convergent by A1,A15,A17,A19,Def4;
then A32: h(#)(h"(#)(f1*(h + c) - f1*c)) is convergent by A28,SEQ_2:28;
A33: h(#)(h"(#)(f1*(h + c) - f1*c)) = (f1*(h + c) - f1*c)
proof
now let n;
A34: h.n <> 0 by A17;
thus (h(#)(h"(#)(f1*(h + c) - f1*c))).n = ((h(#)h")(#)
(f1*(h + c) - f1*c)).n
by SEQ_1:22
.= (h(#)h").n *(f1*(h + c) - f1*c).n by SEQ_1:12
.= h.n * (h").n *(f1*(h + c) - f1*c).n by SEQ_1:12
.= h.n * (h.n)" *(f1*(h + c) - f1*c).n by SEQ_1:def 8
.= 1*(f1*(h + c) - f1*c).n by A34,XCMPLX_0:def 7
.= (f1*(h + c) - f1*c).n;
end;
hence thesis by FUNCT_2:113;
end;
f1*c + (f1*(h + c) - f1*c) = f1*(h + c)
proof
now let n;
thus (f1*c + (f1*(h + c) - f1*c)).n = (f1*c).n + (f1*(h + c) - f1*c).
n
by SEQ_1:11
.= (f1*c).n + ((f1*(h + c)).n - (f1*c).n) by RFUNCT_2:6
.= (f1*(h + c)).n by XCMPLX_1:27;
end;
hence thesis by FUNCT_2:113;
end;
then A35: f1*(h +c) is convergent by A29,A32,A33,SEQ_2:19;
lim (h(#)(h"(#)(f1*(h + c) - f1*c))) = lim h *lim (h"(#)
(f1*(h + c) - f1*c))
by A28,A31,SEQ_2:29
.= 0 by A28;
then A36: 0 = lim (f1*(h + c)) - f1.x0 by A29,A30,A33,A35,SEQ_2:26;
A37: x0 in dom f2 by A13,A23;
A38: rng c c= dom f2
proof let x; assume x in rng c;
hence x in dom f2 by A15,A37,TARSKI:def 1;
end;
A39: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f2*c).m - f2.x0) < g
proof let g be real number such that A40: 0 < g;
take n = 0;
let m such that n <= m;
abs((f2*c).m - f2.x0) = abs(f2.(c.m) - f2.x0) by A38,RFUNCT_2:21
.= abs(f2.x0 - f2.x0) by A22
.= abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f2*c).m - f2.x0) < g by A40;
end;
then A41: f2*c is convergent by SEQ_2:def 6;
A42: rng c c= dom f1 /\ dom f2 by A25,A38,XBOOLE_1:19;
A43: h"(#) (f2*(h + c) - f2*c)(#)
(f1*(h + c)) is convergent by A21,A35,SEQ_2:28;
A44: h"(#) (f1*(h + c) - f1*c)(#)(f2*c) is convergent by A20,A41,SEQ_2:28;
A45: now let n;
thus (h"(#)((f1(#)f2)*(h + c) - (f1(#)f2)*c)).n =
((h").n) * ((f1(#)f2)*(h + c) - (f1(#)f2)*c).n by SEQ_1:12
.= ((h").n) * (((f1(#)f2)*(h + c)).n - ((f1(#)f2)*c).n) by RFUNCT_2:6
.= h".n * (((f1*(h + c))(#)(f2*(h + c))).n - ((f1(#)f2)*c).n)
by A18,RFUNCT_2:23
.= h".n * (((f1*(h + c))(#)(f2*(h + c))).n - ((f1*c)(#)(f2*c)).n)
by A42,RFUNCT_2:23
.= h".n * ((f1*(h + c)).n * (f2*(h + c)).n - ((f1*c)(#)(f2*c)).n)
by SEQ_1:12
.= h".n * ((f1*(h + c)).n * (f2*(h + c)).n
- ((f1*c).n * (f2*c).n)) by SEQ_1:12
.= h".n * (((f1*(h+c)).n * (f2*(h + c)).n - (((f1*(h + c)).n)*(f2*c).n))
+(((f1*(h + c)).n*(f2*c).n) - ((f1*c).n*(f2*c).n))) by XCMPLX_1:39
.= h".n * (((f1*(h + c)).n*((f2*(h + c)).n - (f2*c).n))
+(((f1*(h + c)).n*(f2*c).n) - ((f1*c).n*(f2*c).n))) by XCMPLX_1:40
.= h".n * ((((f2*(h + c)).n - (f2*c).n)*(f1*(h + c)).n)
+(((f1*(h + c)).n - (f1*c).n)*(f2*c).n)) by XCMPLX_1:40
.= h".n * (((f2*(h + c)).n - (f2*c).n)*(f1*(h + c)).n)
+ h".n * (((f1*(h + c)).n - (f1*c).n)*(f2*c).n) by XCMPLX_1:8
.= h".n * (((f2*(h + c)).n - (f2*c).n)*(f1*(h + c)).n)
+ (h".n * ((f1*(h + c)).n - (f1*c).n))*(f2*c).n by XCMPLX_1:4
.= h".n * ((f2*(h + c)).n - (f2*c).n)*(f1*(h + c)).n
+ (h".n * ((f1*(h + c)).n - (f1*c).n))*(f2*c).n by XCMPLX_1:4
.= h".n * (f2*(h + c) - f2*c).n * (f1*(h + c)).n
+ (h".n * ((f1*(h + c)).n - (f1*c).n))*(f2*c).n by RFUNCT_2:6
.= (h"(#) (f2*(h + c) - f2*c)).n * (f1*(h + c)).n
+ (h".n * ((f1*(h + c)).n - (f1*c).n))*(f2*c).n by SEQ_1:12
.= (h"(#) (f2*(h + c) - f2*c)).n * (f1*(h + c)).n
+ (h".n * (f1*(h + c) - (f1*c)).n)*(f2*c).n by RFUNCT_2:6
.= (h"(#) (f2*(h + c) - f2*c)).n * (f1*(h + c)).n
+ (h"(#) (f1*(h + c) - f1*c)).n*(f2*c).n by SEQ_1:12
.= (h"(#) (f2*(h + c) - f2*c) (#) (f1*(h + c))).n
+ (h"(#) (f1*(h + c) - f1*c)).n*(f2*c).n by SEQ_1:12
.= (h"(#) (f2*(h + c) - f2*c)(#)(f1*(h + c))).n
+ (h"(#) (f1*(h + c) - f1*c)(#)(f2*c)).n by SEQ_1:12
.= (h"(#) (f2*(h + c) - f2*c)(#)(f1*(h + c))
+ h"(#) (f1*(h + c) - f1*c)(#)(f2*c)).n by SEQ_1:11;
end;
then A46: h"(#)((f1(#)f2)*(h + c) - (f1(#)f2)*c) = h"(#) (f2*(h + c) - f2*c)(#)
(f1*(h+c))
+ h"(#) (f1*(h + c) - f1*c)(#)(f2*c) by FUNCT_2:113;
lim (h"(#)((f1(#)f2)*(h + c) - (f1(#)f2)*c)) =
lim (h"(#) (f2*(h+c) - f2*c)(#)(f1*(h+c)) + h"(#) (f1*(h + c) - f1*c)(#)
(f2*c))
by A45,FUNCT_2:113
.= lim (h"(#) (f2*(h + c) - f2*c)(#)(f1*(h + c))) +
lim (h"(#) (f1*(h + c) - f1*c)(#)(f2*c)) by A43,A44,SEQ_2:20
.= lim (h"(#) (f2*(h + c) - f2*c))*lim(f1*(h + c)) +
lim (h"(#) (f1*(h + c) - f1*c)(#)(f2*c)) by A21,A35,SEQ_2:29
.= lim (h"(#) (f2*(h + c) - f2*c))*lim(f1*(h + c)) +
lim (h"(#) (f1*(h + c) - f1*c))*lim(f2*c) by A20,A41,SEQ_2:29
.= lim (h"(#) (f2*(h + c) - f2*c))* f1.x0 +
lim (h"(#) (f1*(h + c) - f1*c))*lim(f2*c) by A36,XCMPLX_1:15
.= Ldiff(f1,x0) * f2.x0 + Ldiff(f2,x0) * f1.x0 by A20,A21,A39,A41,SEQ_2:
def 7;
hence thesis by A43,A44,A46,SEQ_2:19;
end;
hence thesis by A4,A14,Th9;
end;
Lm1:
f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 &
(ex r0 st r0 > 0 & for g st g in dom f2 & g in [.x0 - r0,x0.] holds
f2.g <> 0) implies f1/f2 is_left_differentiable_in x0 &
Ldiff(f1/f2,x0) = (Ldiff(f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume A1: f1 is_left_differentiable_in x0 &
f2 is_left_differentiable_in x0;
given r0 such that
A2: r0 > 0 & for g st g in dom f2 & g in [.x0 - r0,x0.] holds f2.g <> 0;
consider r1 such that
A3: 0 < r1 & [.x0 -r1,x0.] c= dom f1 by A1,Def4;
consider r2 such that
A4: 0 < r2 & [.x0 -r2,x0.] c= dom f2 by A1,Def4;
set r3 = min(r0,r2);
A5: 0 < r3 by A2,A4,SQUARE_1:38;
then A6: x0 - r3 <= x0 by PROB_1:2;
r3 <= r0 by SQUARE_1:35;
then A7: x0 - r0 <= x0 - r3 by REAL_1:92;
then x0 - r3 in { g: x0 - r0 <= g & g <= x0 } by A6;
then A8: x0 - r3 in [.x0 - r0,x0.] by RCOMP_1:def 1;
x0 - r0 <= x0 by A6,A7,AXIOMS:22;
then A9: x0 in [.x0 - r0,x0.] by RCOMP_1:15;
then A10: [.x0 - r3,x0.] c= [.x0 - r0,x0.] by A8,RCOMP_1:16;
r3 <= r2 by SQUARE_1:35;
then A11: x0 - r2 <= x0 - r3 by REAL_1:92;
then x0 - r3 in { g: x0 - r2 <= g & g <= x0 } by A6;
then A12: x0 - r3 in [.x0 - r2,x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A6,A11,AXIOMS:22;
then A13: x0 in [.x0 - r2,x0.] by RCOMP_1:15;
then [.x0 - r3,x0.] c= [.x0 - r2,x0.] by A12,RCOMP_1:16;
then A14: [.x0 - r3,x0.] c= dom f2 by A4,XBOOLE_1:1;
set r = min(r1,r3);
A15: 0 < r by A3,A5,SQUARE_1:38;
then A16: x0 - r <= x0 by PROB_1:2;
r <= r1 by SQUARE_1:35;
then A17: x0 - r1 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r1 <= g & g <= x0 } by A16;
then A18: x0 - r in [.x0 - r1,x0.] by RCOMP_1:def 1;
x0 - r1 <= x0 by A16,A17,AXIOMS:22;
then x0 in [.x0 - r1,x0.] by RCOMP_1:15;
then A19: [.x0 - r,x0.] c= [.x0 - r1,x0.] by A18,RCOMP_1:16;
r <= r3 by SQUARE_1:35;
then A20: x0 - r3 <= x0 - r by REAL_1:92;
then x0 - r in { g: x0 - r3 <= g & g <= x0 } by A16;
then A21: x0 - r in [.x0 - r3,x0.] by RCOMP_1:def 1;
x0 - r3 <= x0 by A16,A20,AXIOMS:22;
then x0 in [.x0 - r3,x0.] by RCOMP_1:15;
then A22: [.x0 - r,x0.] c= [.x0 - r3,x0.] by A21,RCOMP_1:16;
A23: [.x0 - r,x0.] c= dom f1 by A3,A19,XBOOLE_1:1;
[.x0 - r,x0.] c= dom(f2^)
proof
assume not thesis;
then consider x such that
A24: x in [.x0 - r ,x0.] & not x in dom (f2^) by TARSKI:def 3;
reconsider x as Real by A24;
A25: not x in dom f2 \ f2"{0} by A24,RFUNCT_1:def 8;
A26: x in [.x0 - r3 ,x0.] by A22,A24;
now per cases by A25,XBOOLE_0:def 4;
suppose not x in dom f2;
hence contradiction by A14,A26;
suppose x in f2"{0};
then x in dom f2 & f2.x in {0} by FUNCT_1:def 13;
then x in dom f2 & f2.x = 0 by TARSKI:def 1;
hence contradiction by A2,A10,A26;
end;
hence contradiction;
end;
then A27: [.x0 - r,x0.] c= dom f2\f2"{0} by RFUNCT_1:def 8;
then [.x0 - r,x0.] c= dom f1 /\ (dom f2\f2"{0}) by A23,XBOOLE_1:19;
then A28: [.x0 - r,x0.] c= dom (f1/f2) by RFUNCT_1:def 4;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1/f2) &
(for n holds h.n < 0) holds
h"(#)((f1/f2)*(h + c) - (f1/f2)*c) is convergent &
lim(h"(#)((f1/f2)*(h + c) - (f1/f2)*c)) =
(Ldiff(f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof let h,c;
assume that
A29: rng c = {x0} and
A30: rng (h+c) c= dom (f1/f2) and
A31: for n holds h.n < 0;
A32: rng (h + c) c= dom f1 /\ (dom f2\f2"{0}) by A30,RFUNCT_1:def 4;
dom f1 /\ (dom f2\f2"{0}) c= dom f1 &
dom f1 /\ (dom f2\f2"{0}) c=(dom f2\f2"{0}) by XBOOLE_1:17;
then A33: rng (h + c) c= dom f1 & rng (h + c) c= (dom f2\f2"{0}) by A32,
XBOOLE_1:1;
dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
then A34: rng (h + c) c= dom f2 by A33,XBOOLE_1:1;
Ldiff(f1,x0) = Ldiff(f1,x0);
then A35: h"(#)(f1*(h + c) - f1*c) is convergent &
lim(h"(#)(f1*(h + c) - f1*c)) = Ldiff(f1,x0) by A1,A29,A31,A33,Th9;
Ldiff(f2,x0) = Ldiff(f2,x0);
then A36: h"(#)(f2*(h + c) - f2*c) is convergent &
lim(h"(#)(f2*(h + c) - f2*c)) = Ldiff(f2,x0) by A1,A29,A31,A34,Th9;
A37: rng (h + c) c= dom (f2^) by A33,RFUNCT_1:def 8;
then A38: rng (h + c) c= dom f1 /\ dom (f2^) by A33,XBOOLE_1:19;
A39: f2*(h + c) is_not_0 by A37,RFUNCT_2:26;
A40: for m holds c.m = x0
proof
let m; c.m in rng c by RFUNCT_2:10;
hence c.m = x0 by A29,TARSKI:def 1;
end;
0 <= r by A3,A5,SQUARE_1:38;
then x0 - r <= x0 by PROB_1:2;
then A41: x0 in [.x0 -r,x0.] by RCOMP_1:15;
then A42: x0 in dom f1 by A23;
A43: rng c c= dom f1
proof
let x be set;
assume x in rng c;
hence x in dom f1 by A29,A42,TARSKI:def 1;
end;
A44: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f1*c).m - f1.x0) < g
proof
let g be real number such that A45: 0 < g;
take n = 0;
let m such that n <= m;
abs((f1*c).m - f1.x0) = abs(f1.(c.m) - f1.x0) by A43,RFUNCT_2:21
.=abs(f1.x0 - f1.x0) by A40
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f1*c).m - f1.x0) < g by A45;
end;
A46: h is convergent & lim h = 0 by FDIFF_1:def 1;
A47: f1*c is convergent by A44,SEQ_2:def 6;
then A48: lim(f1*c) = f1.x0 by A44,SEQ_2:def 7;
A49: h"(#)(f1*(h + c) - f1*c) is convergent & h"(#)(f2*(h + c) - f2*c)
is convergent by A1,A29,A31,A33,A34,Def4;
A50: x0 in (dom f2\f2"{0}) by A27,A41;
rng c c= dom f2\f2"{0}
proof
let x be set;
assume x in rng c;
hence x in (dom f2\f2"{0}) by A29,A50,TARSKI:def 1;
end;
then A51: rng c c= dom (f2^) by RFUNCT_1:def 8;
then A52: rng c c= dom f1 /\ dom (f2^) by A43,XBOOLE_1:19;
A53: f2*c is_not_0 by A51,RFUNCT_2:26;
then A54: (f2*(h + c)) (#) (f2*c) is_not_0 by A39,SEQ_1:43;
dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 8;
then dom (f2^) c= dom f2 by XBOOLE_1:36;
then A55: rng c c= dom f2 by A51,XBOOLE_1:1;
A56: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f2*c).m - f2.x0) < g
proof
let g be real number such that A57: 0 < g;
take n = 0;
let m such that n <= m;
abs((f2*c).m - f2.x0) = abs(f2.(c.m) - f2.x0) by A55,RFUNCT_2:21
.=abs(f2.x0 - f2.x0) by A40
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f2*c).m - f2.x0) < g by A57;
end;
then A58: f2*c is convergent by SEQ_2:def 6;
then A59: lim(f2*c) = f2.x0 by A56,SEQ_2:def 7;
A60: h(#)(h"(#)(f2*(h + c) - f2*c)) is convergent by A36,A46,SEQ_2:28;
A61: h(#)(h"(#)(f2*(h + c) - f2*c)) = (f2*(h + c) - f2*c)
proof
now let n;
A62: h.n <> 0 by A31;
thus (h(#)(h"(#)(f2*(h + c) - f2*c))).n = ((h(#)h")(#)(f2*(h + c) - f2*c)).
n
by SEQ_1:22
.= (h(#)h").n *(f2*(h + c) - f2*c).n by SEQ_1:12
.= h.n * (h").n *(f2*(h + c) - f2*c).n by SEQ_1:12
.= h.n * (h.n)" *(f2*(h + c) - f2*c).n by SEQ_1:def 8
.= 1*(f2*(h + c) - f2*c).n by A62,XCMPLX_0:def 7
.= (f2*(h + c) - f2*c).n;
end;
hence thesis by FUNCT_2:113;
end;
f2*c + (f2*(h + c) - f2*c) = f2*(h + c)
proof
now let n;
thus (f2*c + (f2*(h + c) - f2*c)).n = (f2*c).n + (f2*(h + c) - f2*c).n
by SEQ_1:11
.= (f2*c).n + ((f2*(h + c)).n - (f2*c).n) by RFUNCT_2:6
.= (f2*(h + c)).n by XCMPLX_1:27;
end;
hence thesis by FUNCT_2:113;
end;
then A63: f2*(h +c) is convergent by A58,A60,A61,SEQ_2:19;
lim (h(#)(h"(#)(f2*(h + c) - f2*c))) = lim h *lim (h"(#)(f2*(h + c) - f2*c)
)
by A46,A49,SEQ_2:29
.= 0 by A46;
then A64: 0 = lim (f2*(h + c)) - f2.x0 by A58,A59,A61,A63,SEQ_2:26;
A65: f2*(h + c) (#) (f2*c) is convergent by A58,A63,SEQ_2:28;
A66: lim(f2*(h + c) (#) (f2*c)) = (f2.x0)^2
proof
thus lim(f2*(h + c) (#) (f2*c)) = lim(f2*(h + c)) *lim(f2*c)
by A58,A63,SEQ_2:29
.= f2.x0 * f2.x0 by A59,A64,XCMPLX_1:15
.=(f2.x0)^2 by SQUARE_1:def 3;
end;
A67: lim(f2*(h + c) (#) (f2*c))<> 0
proof assume not thesis;
then f2.x0 = 0 by A66,SQUARE_1:73;
hence contradiction by A2,A4,A9,A13;
end;
A68: (f1*c)(#)(h"(#) (f2*(h + c) - f2*c)) is convergent by A36,A47,SEQ_2:28;
A69: h"(#) (f1*(h + c) - f1*c)(#)(f2*c) is convergent by A35,A58,SEQ_2:28;
A70: h"(#) ((f1/f2)*(h + c) - (f1/f2)*c)=h"(#)((f1(#)
(f2^))*(h + c) - (f1/f2)*c)
by RFUNCT_1:47
.=h"(#)((f1(#)(f2^))*(h + c) - (f1(#)(f2^))*c) by RFUNCT_1:47
.=h"(#)((f1*(h + c))(#)((f2^)*(h + c)) - (f1(#)
(f2^))*c) by A38,RFUNCT_2:23
.=h"(#)((f1*(h + c))(#)(f2*(h + c))" - (f1(#)(f2^))*c) by A37,RFUNCT_2:27
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1(#)(f2^))*c) by SEQ_1:def 9
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1*c)(#)
((f2^)*c)) by A52,RFUNCT_2:23
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1*c)(#)(f2*c)") by A51,RFUNCT_2:27
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1*c)/"(f2*c)) by SEQ_1:def 9
.=h"(#)(((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c)))/"((f2*(h + c))(#)
(f2*c)))
by A39,A53,SEQ_1:58
.=(h"(#)((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c))))/"((f2*(h + c))(#)
(f2*c))
by SEQ_1:49;
A71: ((h"(#)(f1*(h + c) - (f1*c)))(#)(f2*c) - (f1*c)(#)(h"(#)
(f2*(h + c)-(f2*c))))
is convergent by A68,A69,SEQ_2:25;
now let n;
thus (h"(#)((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c)))).n =
(h").n * ((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c))).n by SEQ_1:12
.= (h").n * (((f1*(h + c))(#)(f2*c)).n - ((f1*c)(#)
(f2*(h + c))).n) by RFUNCT_2:6
.= (h").n * ((f1*(h + c)).n * (f2*c).n - ((f1*c)(#)(f2*(h + c))).n)
by SEQ_1:12
.= (h").n * ((f1*(h + c)).n * (f2*c).n - 0 - (f1*c).n * (f2*(h + c)).n) by
SEQ_1:12
.= (h").n * ((f1*(h + c)).n * (f2*c).n - ((f1*c).n*(f2*c).n -(f1*c).n*
(f2*c).n) - (f1*c).n * (f2*(h + c)).n) by XCMPLX_1:14
.= (h").n * (((f1*(h + c)).n * (f2*c).n - (f1*c).n*(f2*c).n) + (f1*c).n*
(f2*c).n - (f1*c).n * (f2*(h + c)).n) by XCMPLX_1:37
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n + ((f1*c).n*(f2*c).n)
- ((f1*c).n * (f2*(h + c)).n)) by XCMPLX_1:40
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n + (((f1*c).n*(f2*c).n)
- ((f1*c).n * (f2*(h + c)).n))) by XCMPLX_1:29
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n - ((f1*c).n *
(f2*(h + c)).n - (f1*c).n*(f2*c).n)) by XCMPLX_1:38
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n - (f1*c).n *
((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:40
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n) - ((h").n) *
((f1*c).n * ((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:40
.= (h").n * ((f1*(h + c)).n - (f1*c).n) * (f2*c).n - ((h").n) *
((f1*c).n * ((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:4
.= (h").n * ((f1*(h + c)).n - (f1*c).n) * (f2*c).n - (f1*c).n * ((h").n *
((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:4
.= (h").n * ((f1*(h + c)) - (f1*c)).n * (f2*c).n - (f1*c).n * ((h").n *
((f2*(h + c)).n - (f2*c).n)) by RFUNCT_2:6
.= (h").n * (f1*(h + c) - (f1*c)).n * (f2*c).n - (f1*c).n * ((h").n *
(f2*(h + c) - (f2*c)).n) by RFUNCT_2:6
.= (h" (#) (f1*(h + c) - (f1*c))).n * (f2*c).n - (f1*c).n * ((h").n *
(f2*(h + c) - (f2*c)).n) by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))).n * (f2*c).n - (f1*c).n * (h"(#)(f2*(h + c)
- (f2*c))).n by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))(#)(f2*c)).n - (f1*c).n * (h"(#)(f2*(h + c)
- (f2*c))).n by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))(#)(f2*c)).n -
((f1*c)(#)(h"(#)(f2*(h + c)-(f2*c)))).n by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))(#)(f2*c) - (f1*c)(#)(h"(#)
(f2*(h + c)-(f2*c)))).n by RFUNCT_2:6;
end;
then A72: h"(#) ((f1/f2)*(h + c) - (f1/f2)*c) =((h"(#)(f1*(h + c) - (f1*c)))
(#)
(f2*c) -
(f1*c)(#)(h"(#)(f2*(h + c)-(f2*c))))/"(f2*(h + c)(#)
(f2*c)) by A70,FUNCT_2:113
;
then lim(h"(#) ((f1/f2)*(h + c) - (f1/f2)*c))
= lim((h"(#)(f1*(h + c) - (f1*c)))(#)(f2*c) - (f1*c)(#)(h"(#)
(f2*(h + c)-(f2*c))))/
lim(f2*(h + c)(#)(f2*c)) by A54,A65,A67,A71,SEQ_2:38
.=(lim((h"(#)(f1*(h + c)-(f1*c)))(#)(f2*c))-lim((f1*c)(#)(h"(#)(f2*(h + c)-
(f2*c)))))/lim(f2*(h + c)(#)(f2*c)) by A68,A69,SEQ_2:26
.=( lim(h"(#)(f1*(h + c)-(f1*c)))*lim(f2*c) -
lim((f1*c) (#) (h"(#)(f2*(h + c)-(f2*c)))) )
/ lim(f2*(h + c)(#)(f2*c)) by A49,A58,SEQ_2:29
.=(Ldiff(f1,x0) * f2.x0 - Ldiff(f2,x0) * f1.x0)/(f2.x0)^2 by A35,A36,A47,A48
,A59,A66,SEQ_2:29;
hence thesis by A54,A65,A67,A71,A72,SEQ_2:37;
end;
hence thesis by A15,A28,Th9;
end;
theorem
f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 &
f2.x0 <> 0 implies f1/f2 is_left_differentiable_in x0 &
Ldiff(f1/f2,x0) = (Ldiff(f1,x0)*f2.x0 - Ldiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume A1: f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0
& f2.x0 <> 0;
then A2: f2 is_Lcontinuous_in x0 by Th5;
ex r st r > 0 &[.x0-r,x0.] c= dom f2 by A1,Def4;
then consider r1 such that A3: r1 > 0 & [.x0-r1,x0.] c= dom f2 &
for g st g in [.x0-r1,x0.] holds f2.g <> 0 by A1,A2,Th6;
now
take r1;
thus r1 > 0 by A3;
let g;
assume g in dom f2 & g in [.x0 - r1,x0.];
hence f2.g <> 0 by A3;
end;
hence thesis by A1,Lm1;
end;
Lm2:
f is_left_differentiable_in x0 &
(ex r0 st r0 > 0 & for g st g in dom f & g in [.x0 - r0,x0.] holds
f.g <> 0) implies f^ is_left_differentiable_in x0 &
Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2
proof
assume A1: f is_left_differentiable_in x0;
given r0 such that
A2: r0 > 0 & for g st g in dom f & g in [.x0 - r0,x0.] holds f.g <> 0;
consider r2 such that
A3: 0 < r2 & [.x0 -r2,x0.] c= dom f by A1,Def4;
set r3 = min(r0,r2);
A4: 0 < r3 by A2,A3,SQUARE_1:38;
then A5: x0 - r3 <= x0 by PROB_1:2;
then A6: x0 in [.x0 - r3,x0.] by RCOMP_1:15;
r3 <= r0 by SQUARE_1:35;
then A7: x0 - r0 <= x0 - r3 by REAL_1:92;
then x0 - r3 in { g: x0 - r0 <= g & g <= x0 } by A5;
then A8: x0 - r3 in [.x0 - r0,x0.] by RCOMP_1:def 1;
x0 - r0 <= x0 by A5,A7,AXIOMS:22;
then A9: x0 in [.x0 - r0,x0.] by RCOMP_1:15;
then A10: [.x0 - r3,x0.] c= [.x0 - r0,x0.] by A8,RCOMP_1:16;
r3 <= r2 by SQUARE_1:35;
then A11: x0 - r2 <= x0 - r3 by REAL_1:92;
then x0 - r3 in { g: x0 - r2 <= g & g <= x0 } by A5;
then A12: x0 - r3 in [.x0 - r2,x0.] by RCOMP_1:def 1;
x0 - r2 <= x0 by A5,A11,AXIOMS:22;
then A13: x0 in [.x0 - r2,x0.] by RCOMP_1:15;
then [.x0 - r3,x0.] c= [.x0 - r2,x0.] by A12,RCOMP_1:16;
then A14: [.x0 - r3,x0.] c= dom f by A3,XBOOLE_1:1;
A15: [.x0 - r3,x0.] c= dom(f^)
proof
assume not thesis;
then consider x such that
A16: x in [.x0 - r3 ,x0.] & not x in dom (f^) by TARSKI:def 3;
reconsider x as Real by A16;
A17: not x in dom f \ f"{0} by A16,RFUNCT_1:def 8;
now per cases by A17,XBOOLE_0:def 4;
suppose not x in dom f;
hence contradiction by A14,A16;
suppose x in f"{0};
then x in dom f & f.x in {0} by FUNCT_1:def 13;
then x in dom f & f.x = 0 by TARSKI:def 1;
hence contradiction by A2,A10,A16;
end;
hence contradiction;
end;
for h,c st rng c = {x0} & rng (h+c) c= dom (f^) &
(for n holds h.n < 0) holds h"(#)((f^)*(h + c) - (f^)*c) is convergent &
lim(h"(#)((f^)*(h + c) - (f^)*c)) = - Ldiff(f,x0)/(f.x0)^2
proof let h,c; assume that
A18: rng c = {x0} and
A19: rng (h+c) c= dom (f^) and
A20: for n holds h.n < 0;
A21: rng (h + c) c= dom f\f"{0} by A19,RFUNCT_1:def 8;
A22: h is convergent & lim h = 0 & h is_not_0 by FDIFF_1:def 1;
dom f \ f"{0} c= dom f by XBOOLE_1:36;
then A23: rng (h + c) c= dom f by A21,XBOOLE_1:1;
Ldiff(f,x0) = Ldiff(f,x0);
then A24: h"(#)(f*(h + c) - f*c) is convergent &
lim(h"(#)(f*(h + c) - f*c)) = Ldiff(f,x0) by A1,A18,A20,A23,Th9;
A25: f*(h + c) is_not_0 by A19,RFUNCT_2:26;
A26: for m holds c.m = x0
proof
let m; c.m in rng c by RFUNCT_2:10;
hence c.m = x0 by A18,TARSKI:def 1;
end;
x0 in dom (f^) by A6,A15;
then A27: x0 in (dom f\f"{0}) by RFUNCT_1:def 8;
rng c c= dom f\f"{0}
proof let x; assume x in rng c;
hence x in (dom f\f"{0}) by A18,A27,TARSKI:def 1;
end;
then A28: rng c c= dom (f^) by RFUNCT_1:def 8;
then A29: f*c is_not_0 by RFUNCT_2:26;
then A30: (f*(h + c)) (#) (f*c) is_not_0 by A25,SEQ_1:43;
dom (f^) = dom f \ f"{0} by RFUNCT_1:def 8;
then dom (f^) c= dom f by XBOOLE_1:36;
then A31: rng c c= dom f by A28,XBOOLE_1:1;
A32: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f*c).m - f.x0) < g
proof
let g be real number such that A33: 0 < g;
take n = 0;
let m such that n <= m;
abs((f*c).m - f.x0) = abs(f.(c.m) - f.x0) by A31,RFUNCT_2:21
.=abs(f.x0 - f.x0) by A26
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f*c).m - f.x0) < g by A33;
end;
then A34: f*c is convergent by SEQ_2:def 6;
then A35: lim(f*c) = f.x0 by A32,SEQ_2:def 7;
A36: h(#)(h"(#)(f*(h + c) - f*c)) is convergent by A22,A24,SEQ_2:28;
A37: h(#)(h"(#)(f*(h + c) - f*c)) = (f*(h + c) - f*c)
proof
now let n;
A38: h.n <> 0 by A20;
thus (h(#)(h"(#)(f*(h+c) - f*c))).n = ((h(#)h")(#)
(f*(h+c) - f*c)).n by SEQ_1:22
.= (h(#)h").n *(f*(h + c) - f*c).n by SEQ_1:12
.= h.n * (h").n *(f*(h + c) - f*c).n by SEQ_1:12
.= h.n * (h.n)" *(f*(h + c) - f*c).n by SEQ_1:def 8
.= 1*(f*(h + c) - f*c).n by A38,XCMPLX_0:def 7
.= (f*(h + c) - f*c).n;
end;
hence thesis by FUNCT_2:113;
end;
f*c + (f*(h + c) - f*c) = f*(h + c)
proof
now let n;
thus (f*c + (f*(h + c) - f*c)).n = (f*c).n + (f*(h + c) - f*c).n
by SEQ_1:11
.= (f*c).n + ((f*(h + c)).n - (f*c).n) by RFUNCT_2:6
.= (f*(h + c)).n by XCMPLX_1:27;
end;
hence thesis by FUNCT_2:113;
end;
then A39: f*(h +c) is convergent by A34,A36,A37,SEQ_2:19;
lim (h(#)(h"(#)(f*(h + c) - f*c))) = lim h *lim (h"(#)(f*(h + c) - f*c))
by A22,A24,SEQ_2:29
.= 0 by A22;
then A40: 0 = lim (f*(h + c)) - f.x0 by A34,A35,A37,A39,SEQ_2:26;
A41: f*(h + c) (#) (f*c) is convergent by A34,A39,SEQ_2:28;
A42: lim(f*(h + c) (#)
(f*c)) = lim(f*(h + c)) *lim(f*c) by A34,A39,SEQ_2:29
.= f.x0 * f.x0 by A35,A40,XCMPLX_1:15
.=(f.x0)^2 by SQUARE_1:def 3;
A43: lim(f*(h + c) (#) (f*c))<> 0
proof assume not thesis;
then f.x0 = 0 by A42,SQUARE_1:73;
hence contradiction by A2,A3,A9,A13;
end;
A44: -(h"(#)((f*(h+c)) - (f*c))) is convergent by A24,SEQ_2:23;
now let n;
A45: (f*(h+c)).n <>0 by A25,SEQ_1:7;
A46: (f*c).n <>0 by A29,SEQ_1:7;
thus (h"(#) ((f^)*(h+c) - (f^)*c)).n =
(h").n* ((f^)*(h+c) - (f^)*c).n by SEQ_1:12
.= (h").n* (((f^)*(h+c)).n - ((f^)*c).n) by RFUNCT_2:6
.= (h").n* (((f*(h+c))").n - ((f^)*c).n) by A19,RFUNCT_2:27
.= (h").n* (((f*(h+c))").n - ((f*c)").n) by A28,RFUNCT_2:27
.= (h").n* (((f*(h+c)).n)" - ((f*c)").n) by SEQ_1:def 8
.= (h").n* (((f*(h+c)).n)" - ((f*c).n)") by SEQ_1:def 8
.= (h").n* (1/(f*(h+c)).n - ((f*c).n)") by XCMPLX_1:217
.= (h").n* (1/(f*(h+c)).n - 1/(f*c).n) by XCMPLX_1:217
.= (h").n* ((1*((f*c).n) - 1*((f*(h+c)).n))/((f*(h+c)).n*(f*c).n))
by A45,A46,XCMPLX_1:131
.= (h").n* (((f*c).n - (f*(h+c)).n)/((f*(h+c))(#)(f*c)).n) by SEQ_1:12
.= (h").n* ((-((f*(h+c)).n - (f*c).n))/((f*(h+c))(#)(f*c)).n)
by XCMPLX_1:143
.= (h").n* ((-((f*(h+c) - (f*c)).n))/((f*(h+c))(#)(f*c)).n) by RFUNCT_2:6
.= (h").n*(-(((f*(h+c) - (f*c)).n)/((f*(h+c))(#)(f*c)).n)) by XCMPLX_1:
188
.= -((h").n*(((f*(h+c) - (f*c)).n)/(((f*(h+c))(#)(f*c)).n))) by XCMPLX_1:
175
.= -((h").n*((f*(h+c) - (f*c)).n))/((f*(h+c))(#)(f*c)).n by XCMPLX_1:75
.= -( ((h" (#) ((f*(h+c)) - (f*c))).n) )/((f*(h+c))(#)(f*c)).n by SEQ_1:12
.= -(((h"(#)((f*(h+c)) - (f*c))).n))*(((f*(h+c))(#)
(f*c)).n)" by XCMPLX_0:def 9
.= -((((h"(#)((f*(h+c)) - (f*c))).n))*(((f*(h+c))(#)
(f*c))").n) by SEQ_1:def 8
.= -((((h"(#)((f*(h+c)) - (f*c))))(#)(((f*(h+c))(#)
(f*c))")).n) by SEQ_1:12
.= -(((h")(#)((f*(h+c)) - (f*c)))/"((f*(h+c))(#)(f*c))).n by SEQ_1:def 9
.= (-((h"(#)((f*(h+c)) - (f*c)))/"((f*(h+c))(#)(f*c)))).n by SEQ_1:14
.= ((-(h"(#)((f*(h+c)) - (f*c))))/"((f*(h+c))(#)(f*c))).n by SEQ_1:56;
end;
then A47: h"(#) ((f^)*(h+c) - (f^)*c) =
(-(h"(#)((f*(h+c)) - (f*c))))/"((f*(h + c))(#)
(f*c)) by FUNCT_2:113;
then lim(h"(#) ((f^)*(h + c) - (f^)*c))
= lim (-(h"(#)
((f*(h+c)) - (f*c))))/(f.x0)^2 by A30,A41,A42,A43,A44,SEQ_2:38
.= (-Ldiff(f,x0))/(f.x0)^2 by A24,SEQ_2:24
.= -Ldiff(f,x0)/(f.x0)^2 by XCMPLX_1:188;
hence thesis by A30,A41,A43,A44,A47,SEQ_2:37;
end;
hence thesis by A4,A15,Th9;
end;
theorem
f is_left_differentiable_in x0 & f.x0 <> 0 implies
f^ is_left_differentiable_in x0 & Ldiff(f^,x0) = - Ldiff(f,x0)/(f.x0)^2
proof
assume A1: f is_left_differentiable_in x0 & f.x0 <> 0;
then A2: f is_Lcontinuous_in x0 by Th5;
ex r st r > 0 &[.x0-r,x0.] c= dom f by A1,Def4;
then consider r1 such that A3: r1 > 0 & [.x0-r1,x0.] c= dom f &
for g st g in [.x0-r1,x0.] holds f.g <> 0 by A1,A2,Th6;
now
take r1;
thus r1 > 0 by A3;
let g;
assume g in dom f & g in [.x0 - r1,x0.];
hence f.g <> 0 by A3;
end;
hence thesis by A1,Lm2;
end;
theorem Th15:
f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 iff
(ex r st r>0 & [.x0,x0+r.] c= dom f) &
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n > 0) holds
h"(#)(f*(h+c) - f*c) is convergent & lim (h"(#)(f*(h+c) - f*c)) = g1
proof
thus f is_right_differentiable_in x0 & Rdiff(f,x0) = g1 implies
(ex r st r>0 & [.x0,x0+r.] c= dom f) &
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n > 0) holds
h"(#)(f*(h+c) - f*c) is convergent & lim (h"(#)(f*(h+c) - f*c)) = g1
by Def3,Def6;
assume A1: (ex r st r>0 & [.x0,x0+r.] c= dom f) &
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n > 0) holds
h"(#)(f*(h+c) - f*c) is convergent & lim (h"(#)(f*(h+c) - f*c)) = g1;
then for h,c holds ( rng c = {x0} & rng (h+c) c= dom f & for n holds h.n > 0
)
implies h"(#)(f*(h+c) - f*c) is convergent;
hence A2: f is_right_differentiable_in x0 by A1,Def3;
for h,c holds ( rng c = {x0} & rng (h+c) c= dom f & for n holds h.n > 0)
implies lim (h"(#)(f*(h+c) - f*c)) = g1 by A1;
hence thesis by A2,Def6;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies
f1+f2 is_right_differentiable_in x0 &
Rdiff(f1+f2,x0) = Rdiff(f1,x0)+Rdiff(f2,x0)
proof assume
A1: f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0;
then consider r1 such that
A2: r1>0 & [.x0,x0+r1.] c= dom f1 by Def3;
consider r2 such that
A3: r2>0 & [.x0,x0+r2.] c=dom f2 by A1,Def3;
set r = min (r1,r2);
A4: 0<r by A2,A3,SQUARE_1:38;
A5: 0 <= r & x0+0 = x0 by A2,A3,SQUARE_1:38;
r<=r1 by SQUARE_1:35;
then A6: x0 + r <= x0 + r1 by REAL_1:55;
A7: x0 <= x0 + r by A5,REAL_1:55;
then A8: x0 <= x0 + r1 by A6,AXIOMS:22;
x0 + r in {g: x0 <= g & g <= x0 +r1} by A6,A7;
then A9: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
x0 in [.x0,x0+r1.] by A8,RCOMP_1:15;
then A10: [.x0,x0+r.] c= [.x0,x0+r1.] by A9,RCOMP_1:16;
r<=r2 by SQUARE_1:35;
then A11: x0 + r <= x0 + r2 by REAL_1:55;
then A12: x0 <= x0 + r2 by A7,AXIOMS:22;
x0 + r in {g: x0 <= g & g <= x0 +r2} by A7,A11;
then A13: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
x0 in [.x0,x0+r2.] by A12,RCOMP_1:15;
then A14: [.x0,x0+r.] c= [.x0,x0+r2.] by A13,RCOMP_1:16;
A15: [.x0,x0+r.] c= dom f1 by A2,A10,XBOOLE_1:1;
[.x0,x0+r.] c= dom f2 by A3,A14,XBOOLE_1:1;
then A16: [.x0,x0+r.] c= dom f1 /\ dom f2 by A15,XBOOLE_1:19;
then A17: [.x0,x0+r.] c= dom(f1 + f2) by SEQ_1:def 3;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1+f2) & (for n holds h.n > 0)
holds h"(#)((f1+f2)*(h+c) - (f1+f2)*c) is convergent &
lim (h"(#)((f1+f2)*(h+c) - (f1+f2)*c)) = Rdiff(f1,x0) + Rdiff(f2,x0)
proof let h,c; assume that
A18: rng c = {x0} and
A19: rng (h+c) c= dom (f1+f2) and
A20: (for n holds h.n > 0);
A21: rng (h+c) c= dom f1 /\ dom f2 by A19,SEQ_1:def 3;
dom f1 /\ dom f2 c= dom f1 & dom f1 /\dom f2 c= dom f2 by XBOOLE_1:17;
then A22: rng (h+c) c= dom f1 & rng (h+c) c= dom f2 by A21,XBOOLE_1:1;
Rdiff(f1,x0) = Rdiff(f1,x0);
then A23: h"(#)(f1*(h+c) - f1*c) is convergent &
lim(h"(#)(f1*(h+c) - f1*c)) = Rdiff(f1,x0) by A1,A18,A20,A22,Th15;
Rdiff(f2,x0) = Rdiff(f2,x0);
then A24: h"(#)(f2*(h+c) - f2*c) is convergent &
lim(h"(#)(f2*(h+c) - f2*c)) = Rdiff(f2,x0) by A1,A18,A20,A22,Th15;
then A25: (h"(#)(f1*(h+c) - f1*c) + h"(#)(f2*(h+c) - f2*c)) is convergent
by A23,SEQ_2:19;
A26: (h"(#)(f1*(h+c) - f1*c) +h"(#)(f2*(h+c) - f2*c))
= h"(#)(f1*(h+c) -f1*c + (f2*(h+c) - f2*c)) by SEQ_1:24;
A27: now let n;
A28: rng c c= dom f1 /\ dom f2
proof let x; assume x in rng c;
then A29: x = x0 by A18,TARSKI:def 1;
x0 in [.x0,x0 + r.] by A7,RCOMP_1:15;
hence thesis by A16,A29;
end;
thus (f1*(h+c) - f1*c + (f2*(h+c) - f2*c)).n =
(f1*(h+c) - f1*c).n + (f2*(h+c) - f2*c).n by SEQ_1:11
.= (f1*(h+c) + (-(f1*c))).n + (f2*(h+c) - f2*c).n by SEQ_1:15
.= (f1*(h+c) + (-(f1*c))).n + (f2*(h+c) + (-(f2*c))).n by SEQ_1:15
.= (f1*(h+c)).n + (-(f1*c)).n + (f2*(h+c) + (-(f2*c))).n by SEQ_1:11
.= (f1*(h+c)).n + (-(f1*c)).n + ((f2*(h+c)).n + (-(f2*c)).n)
by SEQ_1:11
.= (f1*(h+c)).n + ((-(f1*c)).n + ((f2*(h+c)).n + (-(f2*c)).n))
by XCMPLX_1:1
.= (f1*(h+c)).n + (((f2*(h+c)).n + (-(f1*c)).n) + (-(f2*c)).n) by
XCMPLX_1:1
.= (f1*(h+c)).n + ((f2*(h+c)).n + (-(f1*c)).n) + (-(f2*c)).n by XCMPLX_1:
1
.= (f1*(h+c)).n + (f2*(h+c)).n + (-(f1*c)).n + (-(f2*c)).n by XCMPLX_1:1
.= (f1*(h+c)).n + (f2*(h+c)).n+ ((-(f1*c)).n +(-(f2*c)).n) by XCMPLX_1:1
.= (f1*(h+c)).n + (f2*(h+c)).n + (-(f1*c).n + (-(f2*c)).n) by SEQ_1:14
.= (f1*(h+c)).n + (f2*(h+c)).n + (-(f1*c).n + -(f2*c).n) by SEQ_1:14
.= (f1*(h+c)).n + (f2*(h+c)).n + -((f1*c).n + (f2*c).n) by XCMPLX_1:140
.= (f1*(h+c)).n + (f2*(h+c)).n - ((f1*c).n + (f2*c).n) by XCMPLX_0:def 8
.= (f1*(h+c) + f2*(h+c)).n - ((f1*c).n + (f2*c).n) by SEQ_1:11
.= (f1*(h+c) + f2*(h+c)).n - ((f1*c + f2*c).n) by SEQ_1:11
.= (f1*(h+c) + f2*(h+c) - (f1*c + f2*c)).n by RFUNCT_2:6
.= ((f1 + f2)*(h+c) - (f1*c + f2*c)).n by A21,RFUNCT_2:23
.= ((f1 + f2)*(h+c) - (f1 + f2)*c).n by A28,RFUNCT_2:23;
end;
then A30: f1*(h+c)-f1*c + (f2*(h+c) - f2*c)=(f1+f2)*(h+c) - (f1+f2)*c by
FUNCT_2:113;
thus h"(#)((f1 + f2)*(h+c) - (f1 + f2)*c) is convergent by A25,A26,A27,
FUNCT_2:113;
thus lim(h"(#)((f1 + f2)*(h+c) - (f1 + f2)*c)) =
Rdiff(f1,x0) + Rdiff(f2,x0) by A23,A24,A26,A30,SEQ_2:20;
end;
hence thesis by A4,A17,Th15;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies
f1 - f2 is_right_differentiable_in x0 &
Rdiff(f1-f2,x0) = Rdiff(f1,x0) - Rdiff(f2,x0)
proof assume
A1: f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0;
then consider r1 such that
A2: r1>0 & [.x0,x0+r1.] c= dom f1 by Def3;
consider r2 such that
A3: r2>0 & [.x0,x0+r2.] c=dom f2 by A1,Def3;
set r = min (r1,r2);
A4: 0<r by A2,A3,SQUARE_1:38;
r<=r1 by SQUARE_1:35;
then A5: x0 + r <= x0 + r1 by REAL_1:55;
A6: x0 + 0 <= x0 + r by A4,REAL_1:55;
then A7: x0 <= x0 + r1 by A5,AXIOMS:22;
x0 + r in {g: x0 <= g & g <= x0 +r1} by A5,A6;
then A8: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
x0 in [.x0,x0+r1.] by A7,RCOMP_1:15;
then A9: [.x0,x0+r.] c= [.x0,x0+r1.] by A8,RCOMP_1:16;
r<=r2 by SQUARE_1:35;
then A10: x0 + r <= x0 + r2 by REAL_1:55;
then A11: x0 <= x0 + r2 by A6,AXIOMS:22;
x0 + r in {g: x0 <= g & g <= x0 +r2} by A6,A10;
then A12: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
x0 in [.x0,x0+r2.] by A11,RCOMP_1:15;
then A13: [.x0,x0+r.] c= [.x0,x0+r2.] by A12,RCOMP_1:16;
A14: [.x0,x0+r.] c= dom f1 by A2,A9,XBOOLE_1:1;
[.x0,x0+r.] c= dom f2 by A3,A13,XBOOLE_1:1;
then A15: [.x0,x0+r.] c= dom f1 /\ dom f2 by A14,XBOOLE_1:19;
then A16: [.x0,x0+r.] c= dom (f1 - f2) by SEQ_1:def 4;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1 - f2) & (for n holds h.n > 0
)
holds h"(#)((f1-f2)*(h+c) - (f1-f2)*c) is convergent &
lim(h"(#)((f1-f2)*(h+c) - (f1-f2)*c)) = Rdiff(f1,x0) - Rdiff(f2,x0)
proof let h,c; assume that
A17: rng c ={x0} and
A18: rng (h+c) c= dom(f1-f2) and
A19: for n holds h.n > 0;
A20: rng (h+c) c= dom f1 /\ dom f2 by A18,SEQ_1:def 4;
dom f1 /\ dom f2 c= dom f1 & dom f1 /\ dom f2 c= dom f2 by XBOOLE_1:17
;
then A21: rng (h+c) c= dom f1 & rng (h+c) c= dom f2 by A20,XBOOLE_1:1;
Rdiff(f1,x0) = Rdiff(f1,x0);
then A22: h"(#)(f1*(h+c) - f1*c) is convergent &
lim(h"(#)((f1*(h+c) - f1*c))) =Rdiff(f1,x0) by A1,A17,A19,A21,Th15;
Rdiff(f2,x0) = Rdiff(f2,x0);
then A23: h"(#)(f2*(h+c) - f2*c) is convergent &
lim(h"(#)((f2*(h+c) - f2*c))) =Rdiff(f2,x0) by A1,A17,A19,A21,Th15;
then A24: (h"(#)(f1*(h+c) - f1*c) - h"(#)(f2*(h+c) - f2*c)) is convergent
by A22,SEQ_2:25;
A25: (h"(#)(f1*(h+c) - f1*c) - h"(#)(f2*(h+c) - f2*c)) =
h"(#)(f1*(h+c) -f1*c - (f2*(h+c) - f2*c)) by SEQ_1:29;
A26: now let n;
A27: rng c c= dom f1 /\ dom f2
proof let x; assume x in rng c;
then A28: x = x0 by A17,TARSKI:def 1;
x0 in [.x0,x0+r.] by A6,RCOMP_1:15;
hence thesis by A15,A28;
end;
thus (f1*(h+c) - f1*c - (f2*(h+c) - f2*c)).n =
(f1*(h+c) - f1*c).n - (f2*(h + c) - f2*c).n by RFUNCT_2:6
.= (f1*(h+c)).n - (f1*c).n - (f2*(h+c) - (f2*c)).n by RFUNCT_2:6
.= (f1*(h+c)).n - (f1*c).n - ((f2*(h+c)).n - (f2*c).n) by RFUNCT_2:6
.= (f1*(h+c)).n - (f1*c).n - (f2*(h+c)).n + (f2*c).n by XCMPLX_1:37
.= (f1*(h+c)).n - (f2*(h+c)).n - (f1*c).n + (f2*c).n by XCMPLX_1:21
.= (f1*(h+c)).n - (f2*(h+c)).n - ((f1*c).n - (f2*c).n) by XCMPLX_1:37
.= (f1*(h+c) - f2*(h+c)).n - ((f1*c).n - (f2*c).n) by RFUNCT_2:6
.= (f1*(h+c) - f2*(h+c)).n - ((f1*c - f2*c).n) by RFUNCT_2:6
.= (f1*(h+c) - f2*(h+c) - (f1*c - f2*c)).n by RFUNCT_2:6
.= ((f1 - f2)*(h+c) - (f1*c - f2*c)).n by A20,RFUNCT_2:23
.= ((f1 - f2)*(h+c) - (f1 - f2)*c).n by A27,RFUNCT_2:23;
end;
then A29: f1*(h+c) - f1*c - (f2*(h+c) - f2*c) =
(f1 - f2)*(h+c) - (f1 - f2)*c by FUNCT_2:113;
thus h"(#)((f1 - f2)*(h+c) - (f1 - f2)*c) is convergent by A24,A25,A26,
FUNCT_2:113;
thus thesis by A22,A23,A25,A29,SEQ_2:26;
end;
hence thesis by A4,A16,Th15;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies
f1(#)f2 is_right_differentiable_in x0 &
Rdiff(f1(#)f2,x0) = Rdiff(f1,x0)*f2.x0 + Rdiff(f2,x0)*f1.x0
proof assume
A1: f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0;
then consider r1 such that
A2: r1>0 & [.x0,x0+r1.] c= dom f1 by Def3;
consider r2 such that
A3: r2>0 & [.x0,x0+r2.] c=dom f2 by A1,Def3;
set r = min (r1,r2);
A4: 0<r by A2,A3,SQUARE_1:38;
A5: 0 <= r & x0 + 0 =x0 by A2,A3,SQUARE_1:38;
r<=r1 by SQUARE_1:35;
then A6: x0 + r <= x0 + r1 by REAL_1:55;
A7: x0 <= x0 + r by A5,REAL_1:55;
then A8: x0 <= x0+r1 by A6,AXIOMS:22;
x0 + r in {g: x0 <= g & g <= x0 +r1} by A6,A7;
then A9: x0 + r in [.x0,x0+r1.] by RCOMP_1:def 1;
x0 in [.x0,x0+r1.] by A8,RCOMP_1:15;
then A10: [.x0,x0+r.] c= [.x0,x0+r1.] by A9,RCOMP_1:16;
r<=r2 by SQUARE_1:35;
then A11: x0 + r <= x0 + r2 by REAL_1:55;
then A12: x0 <= x0 + r2 by A7,AXIOMS:22;
x0 + r in {g: x0 <= g & g <= x0 +r2} by A7,A11;
then A13: x0 + r in [.x0,x0+r2.] by RCOMP_1:def 1;
x0 in [.x0,x0+r2.] by A12,RCOMP_1:15;
then A14: [.x0,x0+r.] c= [.x0,x0+r2.] by A13,RCOMP_1:16;
A15: [.x0,x0+r.] c= dom f1 by A2,A10,XBOOLE_1:1;
A16: [.x0,x0+r.] c= dom f2 by A3,A14,XBOOLE_1:1;
then [.x0,x0+r.] c= dom f1 /\ dom f2 by A15,XBOOLE_1:19;
then A17: [.x0,x0+r.] c= dom (f1 (#) f2) by SEQ_1:def 5;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1(#)f2) & (for n holds h.n > 0
)
holds h"(#)((f1(#)f2)*(h+c) - (f1(#)f2)*c) is convergent &
lim(h"(#)((f1(#)f2)*(h+c) - (f1(#)
f2)*c))=Rdiff(f1,x0)*f2.x0 + Rdiff(f2,x0)*f1.x0
proof let h,c; assume that
A18: rng c = {x0} and
A19: rng (h+c) c= dom (f1(#)f2) and
A20: for n holds h.n > 0;
A21: rng (h + c) c= dom f1 /\ dom f2 by A19,SEQ_1:def 5;
dom f1 /\ dom f2 c= dom f1 & dom f1 /\ dom f2 c=dom f2 by XBOOLE_1:17;
then A22: rng (h + c) c= dom f1 & rng (h + c) c= dom f2 by A21,XBOOLE_1:1;
Rdiff(f1,x0) = Rdiff(f1,x0);
then A23: h"(#)(f1*(h + c) - f1*c) is convergent &
lim(h"(#)(f1*(h + c) - f1*c)) = Rdiff(f1,x0) by A1,A18,A20,A22,Th15;
Rdiff(f2,x0) = Rdiff(f2,x0);
then A24: h"(#)(f2*(h + c) - f2*c) is convergent &
lim(h"(#)(f2*(h + c) - f2*c)) = Rdiff(f2,x0) by A1,A18,A20,A22,Th15;
A25: for m holds c.m = x0
proof let m; c.m in rng c by RFUNCT_2:10;
hence c.m = x0 by A18,TARSKI:def 1;
end;
x0 + 0 <= x0 +r by A4,REAL_1:55;
then A26: x0 in [.x0 ,x0+ r.] by RCOMP_1:15;
then A27: x0 in dom f1 by A15;
A28: rng c c=dom f1
proof let x; assume x in rng c;
hence x in dom f1 by A18,A27,TARSKI:def 1;
end;
A29: for g be real number st 0<g
ex n st for m st n <= m holds abs((f1*c).m - f1.x0 )<g
proof let g be real number such that A30: 0<g;
take n=0;
let m such that n <= m;
abs((f1*c).m - f1.x0 ) = abs(f1.(c.m) - f1.x0 ) by A28,RFUNCT_2:21
.=abs( f1.x0 - f1.x0 ) by A25
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f1*c).m - f1.x0 )<g by A30;
end;
A31: h is convergent & lim h = 0 by FDIFF_1:def 1;
A32: f1*c is convergent by A29,SEQ_2:def 6;
A33: h"(#)(f1*(h + c) - f1*c) is convergent by A1,A18,A20,A22,Def3;
then A34: h(#)(h"(#)(f1*(h + c) - f1*c)) is convergent by A31,SEQ_2:28;
A35: h(#)(h"(#)(f1*(h + c) - f1*c)) =(f1*(h + c) - f1*c)
proof
now let n;
A36: h.n <> 0 by A20;
thus (h(#)(h"(#)(f1*(h+c) - f1*c))).n =((h(#)h")(#)(f1*(h+c) - f1*c)).
n
by SEQ_1:22
.= (h(#)h").n*(f1*(h+c) - f1*c).n by SEQ_1:12
.= h.n*(h").n*(f1*(h+c) - f1*c).n by SEQ_1:12
.= h.n*(h.n)"*(f1*(h+c) - f1*c).n by SEQ_1:def 8
.= 1*(f1*(h+c) - f1*c).n by A36,XCMPLX_0:def 7
.= (f1*(h+c) - f1*c).n;
end;
hence thesis by FUNCT_2:113;
end;
f1*c + (f1*(h + c) - f1*c) = f1*( h + c )
proof
now let n;
thus (f1*c + (f1*(h+c) - f1*c)).n = (f1*c).n + (f1*(h+c) - f1*c).n
by SEQ_1:11
.= (f1*c).n + ((f1*(h+c)).n - (f1*c).n) by RFUNCT_2:6
.= (f1*(h+c)).n by XCMPLX_1:27;
end;
hence thesis by FUNCT_2:113;
end;
then A37: f1*(h+c) is convergent by A32,A34,A35,SEQ_2:19;
lim(h(#)(h"(#)(f1*(h + c) - f1*c))) =lim h *lim(h"(#)(f1*(h+c) - f1*c))
by A31,A33,SEQ_2:29
.= 0 by A31;
then A38: 0 = lim (f1*(h+c)) - lim(f1*c) by A32,A35,A37,SEQ_2:26
.= lim (f1*(h+c)) - f1.x0 by A29,A32,SEQ_2:def 7;
A39: x0 in dom f2 by A16,A26;
A40: rng c c=dom f2
proof let x; assume x in rng c;
hence x in dom f2 by A18,A39,TARSKI:def 1;
end;
A41: for g be real number st 0<g
ex n st for m st n <= m holds abs((f2*c).m - f2.x0 )<g
proof let g be real number such that A42:0<g;
take n=0;
let m such that n <= m;
abs((f2*c).m - f2.x0 ) = abs(f2.(c.m) - f2.x0 ) by A40,RFUNCT_2:21
.=abs( f2.x0 - f2.x0 ) by A25
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f2*c).m - f2.x0 )<g by A42;
end;
then A43: f2*c is convergent by SEQ_2:def 6;
A44: rng c c= dom f1 /\ dom f2 by A28,A40,XBOOLE_1:19;
A45: h"(#) (f2*(h+c)-f2*c) (#)
(f1*(h+c)) is convergent by A24,A37,SEQ_2:28;
A46: h"(#) (f1*(h+c) - f1*c) (#) (f2*c) is convergent by A23,A43,SEQ_2:28;
A47: now let n;
thus (h"(#)((f1(#)f2)*(h+c) - (f1(#)f2)*c)).n =
((h").n) * ((f1(#)f2)*(h+c) - (f1(#)f2)*c).n by SEQ_1:12
.= ((h").n) * (((f1(#)f2)*(h+c)).n - ((f1(#)f2)*c).n) by RFUNCT_2:6
.= h".n * (((f1*(h+c))(#)(f2*(h+c))).n - ((f1(#)f2)*c).n)
by A21,RFUNCT_2:23
.= h".n * (((f1*(h+c))(#)(f2*(h+c))).n - ((f1*c)(#)(f2*c)).n)
by A44,RFUNCT_2:23
.= h".n * ((f1*(h+c)).n * (f2*(h+c)).n - ((f1*c)(#)(f2*c)).n)
by SEQ_1:12
.= h".n * ((f1*(h+c)).n * (f2*(h+c)).n - ((f1*c).n * (f2*c).n))
by SEQ_1:12
.= h".n * (((f1*(h+c)).n * (f2*(h+c)).n - (((f1*(h+c)).n)*(f2*c).n))
+(((f1*(h+c)).n*(f2*c).n) - ((f1*c).n*(f2*c).n))) by XCMPLX_1:39
.= h".n * (((f1*(h+c)).n*((f2*(h+c)).n - (f2*c).n))
+(((f1*(h+c)).n*(f2*c).n) - ((f1*c).n*(f2*c).n))) by XCMPLX_1:40
.= h".n * ((((f2*(h+c)).n - (f2*c).n)*(f1*(h+c)).n)
+(((f1*(h+c)).n - (f1*c).n)*(f2*c).n)) by XCMPLX_1:40
.= h".n * (((f2*(h+c)).n - (f2*c).n)*(f1*(h+c)).n)
+ h".n * (((f1*(h+c)).n - (f1*c).n)*(f2*c).n) by XCMPLX_1:8
.= h".n * (((f2*(h+c)).n - (f2*c).n)*(f1*(h+c)).n)
+ (h".n * ((f1*(h+c)).n - (f1*c).n))*(f2*c).n by XCMPLX_1:4
.= h".n * ((f2*(h+c)).n - (f2*c).n)*(f1*(h+c)).n
+ (h".n * ((f1*(h+c)).n - (f1*c).n))*(f2*c).n by XCMPLX_1:4
.= h".n * (f2*(h+c) - f2*c).n * (f1*(h+c)).n
+ (h".n * ((f1*(h+c)).n - (f1*c).n))*(f2*c).n by RFUNCT_2:6
.= (h"(#) (f2*(h+c) - f2*c)).n * (f1*(h+c)).n
+ (h".n * ((f1*(h+c)).n - (f1*c).n))*(f2*c).n by SEQ_1:12
.= (h"(#) (f2*(h+c) - f2*c)).n * (f1*(h+c)).n
+ (h".n * (f1*(h+c) - (f1*c)).n)*(f2*c).n by RFUNCT_2:6
.= (h"(#) (f2*(h+c) - f2*c)).n * (f1*(h+c)).n
+ (h"(#) (f1*(h+c) - f1*c)).n*(f2*c).n by SEQ_1:12
.= (h"(#) (f2*(h+c) - f2*c) (#) (f1*(h+c))).n
+ (h"(#) (f1*(h+c) - f1*c)).n*(f2*c).n by SEQ_1:12
.= (h"(#) (f2*(h+c) - f2*c)(#)(f1*(h+c))).n
+ (h"(#) (f1*(h+c) - f1*c)(#)(f2*c)).n by SEQ_1:12
.= (h"(#) (f2*(h+c) - f2*c)(#)(f1*(h + c))
+ h"(#) (f1*(h+c) - f1*c)(#)(f2*c)).n by SEQ_1:11;
end;
then A48: h"(#)((f1(#)f2)*(h+c) - (f1(#)f2)*c) = h"(#) (f2*(h+c) - f2*c)(#)
(f1*(h+c))
+ h"(#) (f1*(h+c) - f1*c)(#)(f2*c) by FUNCT_2:113;
lim (h"(#)((f1(#)f2)*(h+c) - (f1(#)f2)*c)) =
lim (h"(#) (f2*(h+c) - f2*c)(#)(f1*(h+c)) + h"(#) (f1*(h+c) - f1*c)(#)
(f2*c)) by A47,FUNCT_2:113
.= lim (h"(#) (f2*(h+c) - f2*c)(#)(f1*(h + c))) +
lim (h"(#) (f1*(h+c) - f1*c)(#)(f2*c)) by A45,A46,SEQ_2:20
.= lim (h"(#) (f2*(h+c) - f2*c))*lim(f1*(h + c)) +
lim (h"(#) (f1*(h+c) - f1*c)(#)(f2*c)) by A24,A37,SEQ_2:29
.= lim (h"(#) (f2*(h+c) - f2*c))*lim(f1*(h + c)) +
lim (h"(#) (f1*(h+c) - f1*c))*lim(f2*c) by A23,A43,SEQ_2:29
.= lim (h"(#) (f2*(h+c) - f2*c))* f1.x0 +
lim (h"(#) (f1*(h+c) - f1*c))*lim(f2*c) by A38,XCMPLX_1:15
.= Rdiff(f1,x0)*f2.x0 + Rdiff(f2,x0)*f1.x0 by A23,A24,A41,A43,SEQ_2:def 7;
hence thesis by A45,A46,A48,SEQ_2:19;
end;
hence thesis by A4,A17,Th15;
end;
Lm3:
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0
& ( ex r0 st r0 > 0 & for g st g in dom f2 & g in [.x0 , x0 + r0.] holds
f2.g <> 0 ) implies
f1/f2 is_right_differentiable_in x0 &
Rdiff(f1/f2,x0) =(Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume A1: f1 is_right_differentiable_in x0 &
f2 is_right_differentiable_in x0;
given r0 such that
A2: r0 > 0 & for g st g in dom f2 & g in [.x0 ,x0 + r0.] holds f2.g <> 0;
consider r1 such that
A3: 0 < r1 & [.x0,x0 + r1.] c= dom f1 by A1,Def3;
consider r2 such that
A4: 0 < r2 & [.x0,x0 + r2.] c= dom f2 by A1,Def3;
set r3 = min(r0,r2);
A5: 0 < r3 by A2,A4,SQUARE_1:38;
0 <= r3 & 0 + x0 =x0 by A2,A4,SQUARE_1:38;
then A6: x0 <= x0 +r3 by AXIOMS:24;
r3 <= r0 by SQUARE_1:35;
then A7: x0 + r3 <= x0 + r0 by REAL_1:55;
then x0 + r3 in { g: x0 <= g & g<= x0 + r0 } by A6;
then A8: x0 + r3 in [.x0,x0 + r0.] by RCOMP_1:def 1;
x0 <= x0 +r0 by A6,A7,AXIOMS:22;
then A9:x0 in [.x0,x0 + r0.] by RCOMP_1:15;
then A10: [.x0,x0 +r3.] c= [.x0,x0 +r0.] by A8,RCOMP_1:16;
r3 <= r2 by SQUARE_1:35;
then A11: x0 + r3 <= x0 + r2 by REAL_1:55;
then x0 + r3 in { g:x0 <= g & g <= x0 + r2 } by A6;
then A12: x0 + r3 in [.x0,x0 +r2.] by RCOMP_1:def 1;
x0 <= x0 + r2 by A6,A11,AXIOMS:22;
then A13:x0 in [.x0,x0 + r2.] by RCOMP_1:15;
then [.x0,x0 + r3.] c= [.x0,x0 + r2.] by A12,RCOMP_1:16;
then A14: [.x0,x0 + r3.] c= dom f2 by A4,XBOOLE_1:1;
set r = min(r1,r3);
A15: 0 < r by A3,A5,SQUARE_1:38;
0 <= r & x0 +0 = x0 by A3,A5,SQUARE_1:38;
then A16: x0 <= x0 + r by REAL_1:55;
r <= r1 by SQUARE_1:35;
then A17: x0 + r <= x0 + r1 by REAL_1:55;
then x0 + r in { g:x0 <= g & g <= x0 + r1 } by A16;
then A18: x0 + r in [.x0,x0 + r1.] by RCOMP_1:def 1;
x0 <= x0 + r1 by A16,A17,AXIOMS:22;
then x0 in [.x0,x0 +r1.] by RCOMP_1:15;
then A19: [.x0,x0 +r.] c= [.x0 ,x0 + r1.] by A18,RCOMP_1:16;
r <= r3 by SQUARE_1:35;
then A20: x0 + r <= x0 + r3 by REAL_1:55;
then x0 + r in {g:x0 <= g & g <= x0 + r3} by A16;
then A21: x0 + r in [.x0,x0 +r3.] by RCOMP_1:def 1;
x0 <= x0 + r3 by A16,A20,AXIOMS:22;
then x0 in [.x0,x0 + r3.] by RCOMP_1:15;
then A22: [.x0,x0 + r.] c= [.x0,x0 +r3.] by A21,RCOMP_1:16;
A23: [.x0,x0 + r.] c= dom f1 by A3,A19,XBOOLE_1:1;
[.x0,x0 + r.] c= dom(f2^)
proof
assume not thesis;
then consider x such that
A24: x in [.x0,x0 + r.] & not x in dom (f2^) by TARSKI:def 3;
reconsider x as Real by A24;
A25: not x in dom f2 \ f2"{0} by A24,RFUNCT_1:def 8;
A26: x in [.x0,x0 + r3.] by A22,A24;
now per cases by A25,XBOOLE_0:def 4;
suppose not x in dom f2;
hence contradiction by A14,A26;
suppose x in f2"{0};
then x in dom f2 & f2.x in {0} by FUNCT_1:def 13;
then x in dom f2 & f2.x = 0 by TARSKI:def 1;
hence contradiction by A2,A10,A26;
end;
hence contradiction;
end;
then A27: [.x0,x0 + r.] c= dom f2\f2"{0} by RFUNCT_1:def 8;
then [.x0,x0 + r.] c= dom f1 /\ (dom f2\f2"{0}) by A23,XBOOLE_1:19;
then A28: [.x0,x0 + r.] c= dom (f1/f2) by RFUNCT_1:def 4;
for h,c st rng c = {x0} & rng (h+c) c= dom (f1/f2) &
(for n holds h.n > 0) holds
h"(#)((f1/f2)*(h + c) - (f1/f2)*c) is convergent &
lim(h"(#)((f1/f2)*(h + c) - (f1/f2)*c)) =
(Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof let h,c;
assume that
A29: rng c = {x0} and
A30: rng (h+c) c= dom (f1/f2) and
A31: for n holds h.n > 0;
A32: rng (h + c) c= dom f1 /\ (dom f2\f2"{0}) by A30,RFUNCT_1:def 4;
dom f1 /\ (dom f2\f2"{0}) c= dom f1 &
dom f1 /\ (dom f2\f2"{0}) c=(dom f2\f2"{0}) by XBOOLE_1:17;
then A33: rng (h + c) c= dom f1 & rng (h + c) c= (dom f2\f2"{0}) by A32,
XBOOLE_1:1;
dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
then A34: rng (h + c) c= dom f2 by A33,XBOOLE_1:1;
Rdiff(f1,x0) = Rdiff(f1,x0);
then A35: h"(#)(f1*(h + c) - f1*c) is convergent &
lim(h"(#)(f1*(h + c) - f1*c)) = Rdiff(f1,x0) by A1,A29,A31,A33,Th15;
Rdiff(f2,x0) = Rdiff(f2,x0);
then A36: h"(#)(f2*(h + c) - f2*c) is convergent &
lim(h"(#)(f2*(h + c) - f2*c)) = Rdiff(f2,x0) by A1,A29,A31,A34,Th15;
A37: rng (h + c) c= dom (f2^) by A33,RFUNCT_1:def 8;
then A38: rng (h + c) c= dom f1 /\ dom (f2^) by A33,XBOOLE_1:19;
A39: f2*(h + c) is_not_0 by A37,RFUNCT_2:26;
A40: for m holds c.m = x0
proof
let m; c.m in rng c by RFUNCT_2:10;
hence c.m = x0 by A29,TARSKI:def 1;
end;
0 <= r & x0 + 0 = x0 by A3,A5,SQUARE_1:38;
then x0 <= x0 + r by REAL_1:55;
then A41: x0 in [.x0,x0 + r.] by RCOMP_1:15;
then A42: x0 in dom f1 by A23;
A43: rng c c= dom f1
proof
let x be set;
assume x in rng c;
hence x in dom f1 by A29,A42,TARSKI:def 1;
end;
A44: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f1*c).m - f1.x0) < g
proof
let g be real number such that A45: 0 < g;
take n = 0;
let m such that n <= m;
abs((f1*c).m - f1.x0) = abs(f1.(c.m) - f1.x0) by A43,RFUNCT_2:21
.=abs(f1.x0 - f1.x0) by A40
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f1*c).m - f1.x0) < g by A45;
end;
A46: h is convergent & lim h = 0 by FDIFF_1:def 1;
A47: f1*c is convergent by A44,SEQ_2:def 6;
then A48: lim(f1*c) = f1.x0 by A44,SEQ_2:def 7;
A49: h"(#)(f1*(h + c) - f1*c) is convergent & h"(#)(f2*(h + c) - f2*c)
is convergent by A1,A29,A31,A33,A34,Def3;
A50: x0 in (dom f2\f2"{0}) by A27,A41;
rng c c= (dom f2\f2"{0})
proof
let x be set;
assume x in rng c;
hence x in (dom f2\f2"{0}) by A29,A50,TARSKI:def 1;
end;
then A51: rng c c= dom (f2^) by RFUNCT_1:def 8;
then A52: rng c c= dom f1 /\ dom (f2^) by A43,XBOOLE_1:19;
A53: f2*c is_not_0 by A51,RFUNCT_2:26;
then A54: (f2*(h + c)) (#) (f2*c) is_not_0 by A39,SEQ_1:43;
dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 8;
then dom (f2^) c= dom f2 by XBOOLE_1:36;
then A55: rng c c= dom f2 by A51,XBOOLE_1:1;
A56: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f2*c).m - f2.x0) < g
proof
let g be real number such that A57: 0 < g;
take n = 0;
let m such that n <= m;
abs((f2*c).m - f2.x0) = abs(f2.(c.m) - f2.x0) by A55,RFUNCT_2:21
.=abs(f2.x0 - f2.x0) by A40
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f2*c).m - f2.x0) < g by A57;
end;
then A58: f2*c is convergent by SEQ_2:def 6;
then A59: lim(f2*c) = f2.x0 by A56,SEQ_2:def 7;
A60: h(#)(h"(#)(f2*(h + c) - f2*c)) is convergent by A36,A46,SEQ_2:28;
A61: h(#)(h"(#)(f2*(h + c) - f2*c)) = (f2*(h + c) - f2*c)
proof
now let n;
A62: h.n <> 0 by A31;
thus (h(#)(h"(#)(f2*(h + c) - f2*c))).n = ((h(#)h")(#)(f2*(h + c) - f2*c)).
n
by SEQ_1:22
.= (h(#)h").n *(f2*(h + c) - f2*c).n by SEQ_1:12
.= h.n * (h").n *(f2*(h + c) - f2*c).n by SEQ_1:12
.= h.n * (h.n)" *(f2*(h + c) - f2*c).n by SEQ_1:def 8
.= 1*(f2*(h + c) - f2*c).n by A62,XCMPLX_0:def 7
.= (f2*(h + c) - f2*c).n;
end;
hence thesis by FUNCT_2:113;
end;
f2*c + (f2*(h + c) - f2*c) = f2*(h + c)
proof
now let n;
thus (f2*c + (f2*(h + c) - f2*c)).n = (f2*c).n + (f2*(h + c) - f2*c).n
by SEQ_1:11
.= (f2*c).n + ((f2*(h + c)).n - (f2*c).n) by RFUNCT_2:6
.= (f2*(h + c)).n by XCMPLX_1:27;
end;
hence thesis by FUNCT_2:113;
end;
then A63: f2*(h +c) is convergent by A58,A60,A61,SEQ_2:19;
lim (h(#)(h"(#)(f2*(h + c) - f2*c))) = lim h *lim (h"(#)(f2*(h + c) - f2*c)
)
by A46,A49,SEQ_2:29
.= 0 by A46;
then A64: 0 = lim (f2*(h + c)) - f2.x0 by A58,A59,A61,A63,SEQ_2:26;
A65: f2*(h + c) (#) (f2*c) is convergent by A58,A63,SEQ_2:28;
A66: lim(f2*(h + c) (#) (f2*c)) = (f2.x0)^2
proof
now let n;
thus lim(f2*(h + c) (#) (f2*c)) = lim(f2*(h + c)) *lim(f2*c)
by A58,A63,SEQ_2:29
.= f2.x0 * f2.x0 by A59,A64,XCMPLX_1:15
.=(f2.x0)^2 by SQUARE_1:def 3;
end;
hence thesis;
end;
A67: lim(f2*(h + c) (#) (f2*c))<> 0
proof assume not thesis;
then f2.x0 = 0 by A66,SQUARE_1:73;
hence contradiction by A2,A4,A9,A13;
end;
A68: (f1*c)(#)(h"(#) (f2*(h + c) - f2*c)) is convergent by A36,A47,SEQ_2:28;
A69: h"(#) (f1*(h + c) - f1*c)(#)(f2*c) is convergent by A35,A58,SEQ_2:28;
A70: h"(#) ((f1/f2)*(h + c) - (f1/f2)*c)=h"(#)((f1(#)
(f2^))*(h + c) - (f1/f2)*c)
by RFUNCT_1:47
.=h"(#)((f1(#)(f2^))*(h + c) - (f1(#)(f2^))*c) by RFUNCT_1:47
.=h"(#)((f1*(h + c))(#)((f2^)*(h + c)) - (f1(#)
(f2^))*c) by A38,RFUNCT_2:23
.=h"(#)((f1*(h + c))(#)(f2*(h + c))" - (f1(#)(f2^))*c) by A37,RFUNCT_2:27
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1(#)(f2^))*c) by SEQ_1:def 9
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1*c)(#)
((f2^)*c)) by A52,RFUNCT_2:23
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1*c)(#)(f2*c)") by A51,RFUNCT_2:27
.=h"(#)((f1*(h + c))/"(f2*(h + c)) - (f1*c)/"(f2*c)) by SEQ_1:def 9
.=h"(#)(((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c)))/"((f2*(h + c))(#)
(f2*c)))
by A39,A53,SEQ_1:58
.=(h"(#)((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c))))/"((f2*(h + c))(#)
(f2*c))
by SEQ_1:49;
A71: ((h"(#)(f1*(h + c) - (f1*c)))(#)(f2*c) - (f1*c)(#)(h"(#)
(f2*(h + c)-(f2*c))))
is convergent by A68,A69,SEQ_2:25;
now let n;
thus (h"(#)((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c)))).n =
(h").n * ((f1*(h + c))(#)(f2*c) - (f1*c)(#)(f2*(h + c))).n by SEQ_1:12
.= (h").n * (((f1*(h + c))(#)(f2*c)).n - ((f1*c)(#)
(f2*(h + c))).n) by RFUNCT_2:6
.= (h").n * ((f1*(h + c)).n * (f2*c).n - ((f1*c)(#)(f2*(h + c))).n)
by SEQ_1:12
.= (h").n * ((f1*(h + c)).n * (f2*c).n - 0 - (f1*c).n * (f2*(h + c)).n) by
SEQ_1:12
.= (h").n * ((f1*(h + c)).n * (f2*c).n - ((f1*c).n*(f2*c).n -(f1*c).n*
(f2*c).n) - (f1*c).n * (f2*(h + c)).n) by XCMPLX_1:14
.= (h").n * (((f1*(h + c)).n * (f2*c).n - (f1*c).n*(f2*c).n) + (f1*c).n*
(f2*c).n - (f1*c).n * (f2*(h + c)).n) by XCMPLX_1:37
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n + ((f1*c).n*(f2*c).n)
- ((f1*c).n * (f2*(h + c)).n)) by XCMPLX_1:40
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n + (((f1*c).n*(f2*c).n)
- ((f1*c).n * (f2*(h + c)).n))) by XCMPLX_1:29
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n - ((f1*c).n *
(f2*(h + c)).n - (f1*c).n*(f2*c).n)) by XCMPLX_1:38
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n - (f1*c).n *
((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:40
.= (h").n * (((f1*(h + c)).n - (f1*c).n) * (f2*c).n) - ((h").n) *
((f1*c).n * ((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:40
.= (h").n * ((f1*(h + c)).n - (f1*c).n) * (f2*c).n - ((h").n) *
((f1*c).n * ((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:4
.= (h").n * ((f1*(h + c)).n - (f1*c).n) * (f2*c).n - (f1*c).n * ((h").n *
((f2*(h + c)).n - (f2*c).n)) by XCMPLX_1:4
.= (h").n * ((f1*(h + c)) - (f1*c)).n * (f2*c).n - (f1*c).n * ((h").n *
((f2*(h + c)).n - (f2*c).n)) by RFUNCT_2:6
.= (h").n * (f1*(h + c) - (f1*c)).n * (f2*c).n - (f1*c).n * ((h").n *
(f2*(h + c) - (f2*c)).n) by RFUNCT_2:6
.= (h" (#) (f1*(h + c) - (f1*c))).n * (f2*c).n - (f1*c).n * ((h").n *
(f2*(h + c) - (f2*c)).n) by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))).n * (f2*c).n - (f1*c).n * (h"(#)(f2*(h + c)
- (f2*c))).n by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))(#)(f2*c)).n - (f1*c).n * (h"(#)(f2*(h + c)
- (f2*c))).n by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))(#)(f2*c)).n -
((f1*c)(#)(h"(#)(f2*(h + c)-(f2*c)))).n by SEQ_1:12
.= (h"(#)(f1*(h + c) - (f1*c))(#)(f2*c) - (f1*c)(#)(h"(#)
(f2*(h + c)-(f2*c)))).n
by RFUNCT_2:6;
end;
then A72: h"(#) ((f1/f2)*(h + c) - (f1/f2)*c) =((h"(#)(f1*(h + c) - (f1*c)))
(#)
(f2*c) -
(f1*c)(#)(h"(#)(f2*(h + c)-(f2*c))))/"(f2*(h + c)(#)
(f2*c)) by A70,FUNCT_2:113
;
then lim(h"(#) ((f1/f2)*(h + c) - (f1/f2)*c))
= lim((h"(#)(f1*(h + c) - (f1*c)))(#)(f2*c) - (f1*c)(#)(h"(#)
(f2*(h + c)-(f2*c))))/
lim(f2*(h + c)(#)(f2*c)) by A54,A65,A67,A71,SEQ_2:38
.=(lim((h"(#)(f1*(h + c)-(f1*c)))(#)(f2*c))-lim((f1*c)(#)(h"(#)(f2*(h + c)-
(f2*c)))))/lim(f2*(h + c)(#)(f2*c)) by A68,A69,SEQ_2:26
.=( lim(h"(#)(f1*(h + c)-(f1*c)))*lim(f2*c) -
lim((f1*c) (#) (h"(#)(f2*(h + c)-(f2*c)))) )
/ lim(f2*(h + c)(#)(f2*c)) by A49,A58,SEQ_2:29
.=(Rdiff(f1,x0) * f2.x0 - Rdiff(f2,x0) * f1.x0)/(f2.x0)^2 by A35,A36,A47,A48
,A59,A66,SEQ_2:29;
hence thesis by A54,A65,A67,A71,A72,SEQ_2:37;
end;
hence thesis by A15,A28,Th15;
end;
theorem
f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 &
f2.x0 <> 0 implies f1/f2 is_right_differentiable_in x0 &
Rdiff(f1/f2,x0) = (Rdiff(f1,x0)*f2.x0 - Rdiff(f2,x0)*f1.x0)/(f2.x0)^2
proof
assume A1: f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in
x0
& f2.x0 <> 0;
then A2: f2 is_Rcontinuous_in x0 by Th7;
ex r st r > 0 & [.x0,x0 + r.] c= dom f2 by A1,Def3;
then consider r1 such that A3: r1 > 0 & [.x0,x0 + r1.] c= dom f2 &
for g st g in [.x0,x0 + r1.] holds f2.g <> 0 by A1,A2,Th8;
now
take r1;
thus r1 > 0 by A3;
let g;
assume g in dom f2 & g in [.x0,x0+r1.];
hence f2.g <> 0 by A3;
end;
hence thesis by A1,Lm3;
end;
Lm4:
f is_right_differentiable_in x0 &
(ex r0 st r0 > 0 & for g st g in dom f & g in [.x0 , x0 + r0.] holds f.g <> 0)
implies f^ is_right_differentiable_in x0 &
Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2
proof
assume A1: f is_right_differentiable_in x0;
given r0 such that
A2: r0 > 0 & for g st g in dom f & g in [.x0 ,x0 + r0.] holds f.g <> 0;
consider r2 such that
A3: 0 < r2 & [.x0,x0 + r2.] c= dom f by A1,Def3;
set r3 = min(r0,r2);
A4: 0 < r3 by A2,A3,SQUARE_1:38;
0 <= r3 & 0 + x0 =x0 by A2,A3,SQUARE_1:38;
then A5: x0 <= x0 +r3 by AXIOMS:24;
then A6:x0 in [. x0 , x0 + r3 .] by RCOMP_1:15;
r3 <= r0 by SQUARE_1:35;
then A7: x0 + r3 <= x0 + r0 by REAL_1:55;
then x0 + r3 in { g: x0 <= g & g<= x0 + r0 } by A5;
then A8: x0 + r3 in [.x0,x0 + r0.] by RCOMP_1:def 1;
x0 <= x0 +r0 by A5,A7,AXIOMS:22;
then A9:x0 in [.x0,x0 + r0.] by RCOMP_1:15;
then A10: [.x0,x0 +r3.] c= [.x0,x0 +r0.] by A8,RCOMP_1:16;
r3 <= r2 by SQUARE_1:35;
then A11: x0 + r3 <= x0 + r2 by REAL_1:55;
then x0 + r3 in { g:x0 <= g & g <= x0 + r2 } by A5;
then A12: x0 + r3 in [.x0,x0 +r2.] by RCOMP_1:def 1;
x0 <= x0 + r2 by A5,A11,AXIOMS:22;
then A13:x0 in [.x0,x0 + r2.] by RCOMP_1:15;
then [.x0,x0 + r3.] c= [.x0,x0 + r2.] by A12,RCOMP_1:16;
then A14: [.x0,x0 + r3.] c= dom f by A3,XBOOLE_1:1;
A15: [.x0,x0 + r3.] c= dom(f^)
proof
assume not thesis;
then consider x such that
A16: x in [.x0,x0 + r3.] & not x in dom (f^) by TARSKI:def 3;
reconsider x as Real by A16;
A17: not x in dom f \ f"{0} by A16,RFUNCT_1:def 8;
now per cases by A17,XBOOLE_0:def 4;
suppose not x in dom f;
hence contradiction by A14,A16;
suppose x in f"{0};
then x in dom f & f.x in {0} by FUNCT_1:def 13;
then x in dom f & f.x = 0 by TARSKI:def 1;
hence contradiction by A2,A10,A16;
end;
hence contradiction;
end;
for h,c st rng c = {x0} & rng (h+c) c= dom (f^) &
(for n holds h.n > 0) holds
h"(#)((f^)*(h + c) - (f^)*c) is convergent &
lim(h"(#)((f^)*(h + c) - (f^)*c)) = - Rdiff(f,x0)/(f.x0)^2
proof let h,c;
assume that
A18: rng c = {x0} and
A19: rng (h+c) c= dom (f^) and
A20: for n holds h.n > 0;
A21: rng (h + c) c= dom f\f"{0} by A19,RFUNCT_1:def 8;
A22: h is convergent & lim h = 0 & h is_not_0 by FDIFF_1:def 1;
dom f \ f"{0} c= dom f by XBOOLE_1:36;
then A23: rng (h + c) c= dom f by A21,XBOOLE_1:1;
Rdiff(f,x0) = Rdiff(f,x0);
then A24: h"(#)(f*(h + c) - f*c) is convergent &
lim(h"(#)(f*(h + c) - f*c)) = Rdiff(f,x0) by A1,A18,A20,A23,Th15;
A25: f*(h + c) is_not_0 by A19,RFUNCT_2:26;
A26: for m holds c.m = x0
proof
let m; c.m in rng c by RFUNCT_2:10;
hence c.m = x0 by A18,TARSKI:def 1;
end;
x0 in dom (f^) by A6,A15;
then A27: x0 in (dom f\f"{0}) by RFUNCT_1:def 8;
rng c c= (dom f\f"{0})
proof
let x be set;
assume x in rng c;
hence x in (dom f\f"{0}) by A18,A27,TARSKI:def 1;
end;
then A28: rng c c= dom (f^) by RFUNCT_1:def 8;
then A29: f*c is_not_0 by RFUNCT_2:26;
then A30: (f*(h + c)) (#) (f*c) is_not_0 by A25,SEQ_1:43;
dom (f^) = dom f \ f"{0} by RFUNCT_1:def 8;
then dom (f^) c= dom f by XBOOLE_1:36;
then A31: rng c c= dom f by A28,XBOOLE_1:1;
A32: for g be real number st 0 < g
ex n st for m st n <=m holds abs((f*c).m - f.x0) < g
proof
let g be real number such that A33: 0 < g;
take n = 0;
let m such that n <= m;
abs((f*c).m - f.x0) = abs(f.(c.m) - f.x0) by A31,RFUNCT_2:21
.=abs(f.x0 - f.x0) by A26
.=abs(0) by XCMPLX_1:14
.= 0 by ABSVALUE:def 1;
hence abs((f*c).m - f.x0) < g by A33;
end;
then A34: f*c is convergent by SEQ_2:def 6;
then A35: lim(f*c) = f.x0 by A32,SEQ_2:def 7;
A36: h(#)(h"(#)(f*(h + c) - f*c)) is convergent by A22,A24,SEQ_2:28;
A37: h(#)(h"(#)(f*(h + c) - f*c)) = (f*(h + c) - f*c)
proof
now let n;
A38: h.n <> 0 by A20;
thus (h(#)(h"(#)(f*(h + c) - f*c))).n = ((h(#)h")(#)(f*(h + c) - f*c)).n
by SEQ_1:22
.= (h(#)h").n *(f*(h + c) - f*c).n by SEQ_1:12
.= h.n * (h").n *(f*(h + c) - f*c).n by SEQ_1:12
.= h.n * (h.n)" *(f*(h + c) - f*c).n by SEQ_1:def 8
.= 1*(f*(h + c) - f*c).n by A38,XCMPLX_0:def 7
.= (f*(h + c) - f*c).n;
end;
hence thesis by FUNCT_2:113;
end;
f*c + (f*(h + c) - f*c) = f*(h + c)
proof
now let n;
thus (f*c + (f*(h + c) - f*c)).n = (f*c).n + (f*(h + c) - f*c).n
by SEQ_1:11
.= (f*c).n + ((f*(h + c)).n - (f*c).n) by RFUNCT_2:6
.= (f*(h + c)).n by XCMPLX_1:27;
end;
hence thesis by FUNCT_2:113;
end;
then A39: f*(h +c) is convergent by A34,A36,A37,SEQ_2:19;
lim (h(#)(h"(#)(f*(h + c) - f*c))) = lim h *lim (h"(#)(f*(h + c) - f*c))
by A22,A24,SEQ_2:29
.= 0 by A22;
then A40: 0 = lim (f*(h + c)) - f.x0 by A34,A35,A37,A39,SEQ_2:26;
A41: f*(h + c) (#) (f*c) is convergent by A34,A39,SEQ_2:28;
A42: lim(f*(h + c) (#) (f*c)) = (f.x0)^2
proof
now let n;
thus lim(f*(h + c) (#) (f*c)) = lim(f*(h + c)) *lim(f*c)
by A34,A39,SEQ_2:29
.= f.x0 * f.x0 by A35,A40,XCMPLX_1:15
.=(f.x0)^2 by SQUARE_1:def 3;
end;
hence thesis;
end;
A43: lim(f*(h + c) (#) (f*c))<> 0
proof assume not thesis;
then f.x0 = 0 by A42,SQUARE_1:73;
hence contradiction by A2,A3,A9,A13;
end;
A44:-(h"(#)((f*(h + c)) - (f*c))) is convergent by A24,SEQ_2:23;
now let n;
A45: (f*(h+c)).n <>0 by A25,SEQ_1:7;
A46: (f*c).n <>0 by A29,SEQ_1:7;
thus (h"(#) ((f^)*(h+c) - (f^)*c)).n =
(h").n* ((f^)*(h+c) - (f^)*c).n by SEQ_1:12
.= (h").n* (((f^)*(h+c)).n - ((f^)*c).n) by RFUNCT_2:6
.= (h").n* (((f*(h+c))").n - ((f^)*c).n) by A19,RFUNCT_2:27
.= (h").n* (((f*(h+c))").n - ((f*c)").n) by A28,RFUNCT_2:27
.= (h").n* (((f*(h+c)).n)" - ((f*c)").n) by SEQ_1:def 8
.= (h").n* (((f*(h+c)).n)" - ((f*c).n)") by SEQ_1:def 8
.= (h").n* (1/(f*(h+c)).n - ((f*c).n)") by XCMPLX_1:217
.= (h").n* (1/(f*(h+c)).n - 1/(f*c).n) by XCMPLX_1:217
.= (h").n* ((1*((f*c).n) - 1*((f*(h+c)).n))/((f*(h+c)).n*(f*c).n))
by A45,A46,XCMPLX_1:131
.= (h").n* (((f*c).n - (f*(h+c)).n)/((f*(h+c))(#)(f*c)).n) by SEQ_1:12
.= (h").n* ((-((f*(h+c)).n - (f*c).n))/((f*(h+c))(#)(f*c)).n)
by XCMPLX_1:143
.= (h").n* ((-((f*(h+c) - (f*c)).n))/((f*(h+c))(#)(f*c)).n) by RFUNCT_2:6
.= (h").n*(-(((f*(h+c) - (f*c)).n)/((f*(h+c))(#)(f*c)).n)) by XCMPLX_1:
188
.= -((h").n*(((f*(h+c) - (f*c)).n)/(((f*(h+c))(#)(f*c)).n))) by XCMPLX_1:
175
.= -((h").n*((f*(h+c) - (f*c)).n))/((f*(h+c))(#)(f*c)).n by XCMPLX_1:75
.= -( ((h" (#) ((f*(h+c)) - (f*c))).n) )/((f*(h+c))(#)(f*c)).n by SEQ_1:12
.= -(((h"(#)((f*(h+c)) - (f*c))).n))*(((f*(h+c))(#)
(f*c)).n)" by XCMPLX_0:def 9
.= -((((h"(#)((f*(h+c)) - (f*c))).n))*(((f*(h+c))(#)
(f*c))").n) by SEQ_1:def 8
.= -((((h"(#)((f*(h+c)) - (f*c))))(#)(((f*(h+c))(#)
(f*c))")).n) by SEQ_1:12
.= -(((h")(#)((f*(h+c)) - (f*c)))/"((f*(h+c))(#)(f*c))).n by SEQ_1:def 9
.= (-((h"(#)((f*(h+c)) - (f*c)))/"((f*(h+c))(#)(f*c)))).n by SEQ_1:14
.= ((-(h"(#)((f*(h+c)) - (f*c))))/"((f*(h+c))(#)(f*c))).n by SEQ_1:56;
end;
then A47:h"(#) ((f^)*(h+c) - (f^)*c) = (-(h"(#)((f*(h+c)) - (f*c))))/"((f*(h+c
))(#)
(f*c)) by FUNCT_2:113;
then lim(h"(#) ((f^)*(h + c) - (f^)*c))
= lim(-(h"(#)
((f*(h + c))- (f*c))))/(f.x0)^2 by A30,A41,A42,A43,A44,SEQ_2:38
.=(- Rdiff(f,x0)) /(f.x0)^2 by A24,SEQ_2:24
.=- Rdiff(f,x0) /(f.x0)^2 by XCMPLX_1:188;
hence thesis by A30,A41,A43,A44,A47,SEQ_2:37;
end;
hence thesis by A4,A15,Th15;
end;
theorem
f is_right_differentiable_in x0 & f.x0 <> 0 implies
f^ is_right_differentiable_in x0 & Rdiff(f^,x0) = - Rdiff(f,x0)/(f.x0)^2
proof
assume A1: f is_right_differentiable_in x0 & f.x0 <> 0;
then A2: f is_Rcontinuous_in x0 by Th7;
ex r st r > 0 & [.x0,x0 + r.] c= dom f by A1,Def3;
then consider r1 such that A3: r1 > 0 & [.x0,x0 + r1.] c= dom f &
for g st g in [.x0,x0 + r1.] holds f.g <> 0 by A1,A2,Th8;
now
take r1;
thus r1 > 0 by A3;
let g;
assume g in dom f & g in [.x0,x0+r1.];
hence f.g <> 0 by A3;
end;
hence thesis by A1,Lm4;
end;
theorem
f is_right_differentiable_in x0 & f is_left_differentiable_in x0 &
Rdiff(f,x0) = Ldiff(f,x0) implies
f is_differentiable_in x0 & diff(f,x0)=Rdiff(f,x0) & diff(f,x0)=Ldiff(f,x0)
proof
assume A1: f is_right_differentiable_in x0 & f is_left_differentiable_in x0
& Rdiff(f,x0) = Ldiff(f,x0);
A2: ex N being Neighbourhood of x0 st N c= dom f
proof
consider r1 such that
A3: r1>0 & [.x0-r1,x0.] c= dom f by A1,Def4;
consider r2 such that
A4: r2>0 & [.x0,x0+r2.] c= dom f by A1,Def3;
set r = min(r1,r2);
r > 0 by A3,A4,SQUARE_1:38;
then reconsider N = ].x0 -r,x0+r.[ as Neighbourhood of x0 by RCOMP_1:def 7;
take N;
let x; assume x in N;
then x in { g: x0 - r < g & g < x0 + r} by RCOMP_1:def 2;
then consider g such that
A5: g = x & x0 - r < g & g < x0 + r;
now per cases;
suppose A6: g <= x0;
r <= r1 by SQUARE_1:35;
then x0 - r1 <= x0 - r by REAL_1:92;
then x0 - r1 <= g by A5,AXIOMS:22;
then g in {g1: x0 - r1 <= g1 & g1 <= x0} by A6;
then g in [.x0-r1,x0.] by RCOMP_1:def 1;
hence x in dom f by A3,A5;
suppose A7: g > x0;
r <= r2 by SQUARE_1:35;
then x0 + r <= x0 + r2 by REAL_1:55;
then g <= x0 + r2 by A5,AXIOMS:22;
then g in {g1: x0 <= g1 & g1 <= x0+r2} by A7;
then g in [.x0,x0+r2.] by RCOMP_1:def 1;
hence x in dom f by A4,A5;
end;
hence x in dom f;
end;
for h,c st rng c = {x0} & rng (h + c) c= dom f holds
h"(#)(f*(h + c) - f*c) is convergent & lim (h"(#)
(f*(h + c) - f*c)) = Ldiff(f,x0)
proof let h,c;
assume A8: rng c = {x0} & rng (h + c) c= dom f;
A9: rng c c= dom f
proof
consider S being Neighbourhood of x0 such that A10: S c= dom f by A2;
x0 in S by RCOMP_1:37; hence thesis by A8,A10,ZFMISC_1:37;
end;
now per cases;
suppose ex N be Nat st for n st n >= N holds h.n > 0;
then consider N be Nat such that
A11: for n st n >= N holds h.n > 0;
set h1 = h ^\N;
set c1 = c ^\N;
A12: rng c1 = {x0}
proof
thus rng c1 c= {x0} by A8,RFUNCT_2:7;
let x; assume x in {x0};
then A13: x = x0 by TARSKI:def 1;
A14: c1.0 = c.(0+N) by SEQM_3:def 9
.= c.N;
c.N in rng c by RFUNCT_2:10;
then c1.0 = x by A8,A13,A14,TARSKI:def 1;
hence thesis by RFUNCT_2:10;
end;
A15: h1 + c1 = (h + c)^\N by SEQM_3:37;
then rng (h1 + c1) c= rng (h + c) by RFUNCT_2:7;
then A16: rng (h1 + c1) c= dom f by A8,XBOOLE_1:1;
for n holds h1.n > 0
proof let n;
A17: h1.n = h.(n+N) by SEQM_3:def 9;
0 <= n by NAT_1:18;
then N + 0 <= n + N by REAL_1:55;
hence thesis by A11,A17;
end;
then A18: h1"(#)(f*(h1 + c1) - f*c1) is convergent &
lim (h1"(#)(f*(h1 + c1) - f*c1)) = Rdiff(f,x0) by A1,A12,A16,Th15;
A19: h1"(#)(f*(h1 + c1) - f*c1) = h1"(#)((f*(h+c))^\N - f*c1)
by A8,A15,RFUNCT_2:22
.= h1"(#)((f*(h+c))^\N - (f*c)^\N) by A9,RFUNCT_2:22
.= h1"(#)((f*(h+c) - f*c)^\N) by SEQM_3:39
.= ((h")^\N) (#)((f*(h+c) - f*c)^\N) by SEQM_3:41
.= (h"(#)(f*(h + c) - f*c))^\N by SEQM_3:42;
hence h"(#)(f*(h + c) - f*c) is convergent by A18,SEQ_4:35;
thus lim (h"(#)(f*(h + c) - f*c)) =Ldiff(f,x0) by A1,A18,A19,SEQ_4:36;
suppose A20: for N be Nat ex n st n >= N & h.n <= 0;
now per cases;
suppose ex M be Nat st for m st m >= M holds h.m < 0;
then consider M be Nat such that
A21: for n st n >= M holds h.n < 0;
set h1 = h ^\M;
set c1 = c ^\M;
A22: rng c1 = {x0}
proof
thus rng c1 c= {x0} by A8,RFUNCT_2:7;
let x; assume x in {x0};
then A23: x = x0 by TARSKI:def 1;
A24: c1.0 = c.(0+M) by SEQM_3:def 9
.= c.M;
c.M in rng c by RFUNCT_2:10;
then c1.0 = x by A8,A23,A24,TARSKI:def 1;
hence thesis by RFUNCT_2:10;
end;
A25: h1 + c1 = (h + c)^\M by SEQM_3:37;
then rng (h1 + c1) c= rng (h + c) by RFUNCT_2:7;
then A26: rng (h1 + c1) c= dom f by A8,XBOOLE_1:1;
for n holds h1.n < 0
proof let n;
A27: h1.n = h.(n+M) by SEQM_3:def 9;
0 <= n by NAT_1:18;
then M + 0 <= n + M by REAL_1:55;
hence thesis by A21,A27;
end;
then A28: h1"(#)(f*(h1 + c1) - f*c1) is convergent &
lim (h1"(#)(f*(h1 + c1) - f*c1)) = Ldiff(f,x0) by A1,A22,A26,Th9;
A29: h1"(#)(f*(h1 + c1) - f*c1) = h1"(#)((f*(h+c))^\M - f*c1)
by A8,A25,RFUNCT_2:22
.= h1"(#)((f*(h+c))^\M - (f*c)^\M) by A9,RFUNCT_2:22
.= h1"(#)((f*(h+c) - f*c)^\M) by SEQM_3:39
.= ((h")^\M) (#)((f*(h+c) - f*c)^\M) by SEQM_3:41
.= (h"(#)(f*(h + c) - f*c))^\M by SEQM_3:42;
hence h"(#)(f*(h + c) - f*c) is convergent by A28,SEQ_4:35;
thus lim (h"(#)(f*(h + c) - f*c)) =Ldiff(f,x0) by A28,A29,SEQ_4:36;
suppose A30: for M be Nat ex m st m >= M & h.m >= 0;
A31: h is_not_0 & h is convergent & lim h = 0 by FDIFF_1:def 1;
defpred P[real number] means $1 < 0;
defpred R[real number] means $1 > 0;
A32: for N be Nat ex n st n >= N & P[h.n]
proof
let m; consider n such that A33: n >= m & h.n <= 0 by A20;
take n; thus n >= m by A33;
h.n <> 0 by A31,SEQ_1:7;
hence thesis by A33;
end;
A34: for N be Nat ex n st n >= N & R[h.n]
proof
let m; consider n such that A35: n >= m & h.n >= 0 by A30;
take n; thus n >= m by A35;
h.n <> 0 by A31,SEQ_1:7;
hence thesis by A35;
end;
consider q1 being increasing Seq_of_Nat such that
A36: (for n holds P[(h*q1).n]) &
for n st (for r st r = h.n holds P[r]) ex m st n = q1.m
from ExInc_Seq_of_Nat(A32);
consider q2 being increasing Seq_of_Nat such that
A37: (for n holds R[(h*q2).n]) &
for n st (for r st r = h.n holds R[r]) ex m st n = q2.m
from ExInc_Seq_of_Nat(A34);
set h1 = h*q1;
set h2 = h*q2;
set c1 = c*q1;
set c2 = c*q2;
A38: h1 is_subsequence_of h by SEQM_3:def 10;
then A39: h1 is convergent by A31,SEQ_4:29;
A40: lim h1 = 0 by A31,A38,SEQ_4:30;
h1 is_not_0 by A31,A38,RFUNCT_2:12;
then reconsider h1 as convergent_to_0 Real_Sequence by A39,A40,FDIFF_1:
def 1;
A41: h2 is_subsequence_of h by SEQM_3:def 10;
then A42: h2 is convergent by A31,SEQ_4:29;
A43: lim h2 = 0 by A31,A41,SEQ_4:30;
h2 is_not_0 by A31,A41,RFUNCT_2:12;
then reconsider h2 as convergent_to_0 Real_Sequence by A42,A43,FDIFF_1:
def 1;
A44: c1 is_subsequence_of c by SEQM_3:def 10;
A45: c2 is_subsequence_of c by SEQM_3:def 10;
A46: rng c1 = {x0} by A8,A44,SEQM_3:55;
reconsider c1 as constant Real_Sequence by A44,SEQM_3:55;
(h + c)*q1 is_subsequence_of (h + c) by SEQM_3:def 10;
then rng ((h+c)*q1) c= rng (h+c) by RFUNCT_2:11;
then rng ((h+c)*q1) c= dom f by A8,XBOOLE_1:1;
then rng (h1+c1) c= dom f by RFUNCT_2:13;
then A47: h1"(#)(f*(h1+c1)-f*c1) is convergent &
lim(h1"(#)(f*(h1+c1)-f*c1))=Ldiff(f,x0) by A1,A36,A46,Th9;
A48: rng c2 = {x0} by A8,A45,SEQM_3:55;
reconsider c2 as constant Real_Sequence by A45,SEQM_3:55;
(h + c)*q2 is_subsequence_of (h + c) by SEQM_3:def 10;
then rng ((h+c)*q2) c= rng (h+c) by RFUNCT_2:11;
then rng ((h+c)*q2) c= dom f by A8,XBOOLE_1:1;
then rng (h2+c2) c= dom f by RFUNCT_2:13;
then A49: h2"(#)(f*(h2+c2)-f*c2) is convergent &
lim(h2"(#)(f*(h2+c2)-f*c2))=Ldiff(f,x0) by A1,A37,A48,Th15;
A50: h1"(#)(f*(h1+c1)-f*c1) = h1"(#)(f*((h+c)*q1)-f*c1) by RFUNCT_2:13
.= h1"(#)(f*(h+c)*q1-f*c1) by A8,RFUNCT_2:28
.= ((h")*q1)(#)(f*(h+c)*q1-f*c1) by RFUNCT_2:16
.= ((h")*q1)(#)(f*(h+c)*q1-f*c*q1) by A9,RFUNCT_2:28
.= ((h")*q1)(#)((f*(h+c)-f*c)*q1) by RFUNCT_2:13
.= ((h")(#)(f*(h+c)-f*c))*q1 by RFUNCT_2:13;
A51: h2"(#)(f*(h2+c2)-f*c2) = h2"(#)(f*((h+c)*q2)-f*c2) by RFUNCT_2:13
.= h2"(#)(f*(h+c)*q2-f*c2) by A8,RFUNCT_2:28
.= ((h")*q2)(#)(f*(h+c)*q2-f*c2) by RFUNCT_2:16
.= ((h")*q2)(#)(f*(h+c)*q2-f*c*q2) by A9,RFUNCT_2:28
.= ((h")*q2)(#)((f*(h+c)-f*c)*q2) by RFUNCT_2:13
.= ((h")(#)(f*(h+c)-f*c))*q2 by RFUNCT_2:13;
set s = (h")(#)(f*(h+c)-f*c);
A52: for g1 be real number st 0<g1
ex n st for m st n<=m holds abs(s.m - Ldiff(f,x0))<g1
proof
let g1 be real number; assume
A53: 0 < g1; then consider n1 be Nat such that
A54: for m st n1 <= m holds abs((s*q1).m - Ldiff(f,x0))<g1
by A47,A50,SEQ_2:def 7;
consider n2 be Nat such that
A55: for m st n2 <= m holds abs((s*q2).m - Ldiff(f,x0))<g1
by A49,A51,A53,SEQ_2:def 7;
take n = max(q1.n1,q2.n2);
let m such that A56: n <= m;
A57: n >= q1.n1 & n >= q2.n2 by SQUARE_1:46;
now per cases;
suppose h.m > 0;
then for r st r = h.m holds r > 0; then consider k such that
A58: m = q2.k by A37;
q2.k >= q2.n2 by A56,A57,A58,AXIOMS:22;
then not k < n2 by SEQM_3:7;
then abs((s*q2).k - Ldiff(f,x0))<g1 by A55;
hence abs(s.m - Ldiff(f,x0))<g1 by A58,SEQM_3:31;
suppose A59: h.m <= 0;
h.m <> 0 by A31,SEQ_1:7;
then for r st r = h.m holds r < 0 by A59;
then consider k such that
A60: m = q1.k by A36;
q1.k >= q1.n1 by A56,A57,A60,AXIOMS:22;
then not k < n1 by SEQM_3:7;
then abs((s*q1).k - Ldiff(f,x0))<g1 by A54;
hence abs(s.m - Ldiff(f,x0))<g1 by A60,SEQM_3:31;
end;
hence thesis;
end;
hence s is convergent by SEQ_2:def 6;
hence lim s = Ldiff(f,x0) by A52,SEQ_2:def 7;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1,A2,FDIFF_2:12;
end;
theorem
f is_differentiable_in x0 implies f is_right_differentiable_in x0 &
f is_left_differentiable_in x0 & diff(f,x0) = Rdiff(f,x0)
& diff(f,x0) = Ldiff(f,x0)
proof
assume A1: f is_differentiable_in x0;
A2: diff(f,x0) = diff(f,x0);
consider N be Neighbourhood of x0 such that
A3: N c= dom f by A1,FDIFF_2:11;
consider g1 be real number such that
A4: g1 > 0 & N = ].x0 - g1,x0 + g1.[ by RCOMP_1:def 7;
A5: g1/2 > 0 by A4,REAL_2:127;
A6: g1 > g1/2 by A4,SEQ_2:4;
A7: ex r st r>0 & [.x0,x0+r.] c= dom f
proof
take r = g1/2;
thus r is Real by XREAL_0:def 1;
thus r > 0 by A4,SEQ_2:3;
A8: x0 in ].x0 - g1, x0 + g1 .[ by A4,RCOMP_1:37;
abs((x0 + g1/2) -x0 ) = abs((g1/2 + x0) + -x0 ) by XCMPLX_0:def 8
.= abs(g1/2 +( x0 + -x0) ) by XCMPLX_1:1
.= abs(g1/2 + 0 ) by XCMPLX_0:def 6
.= g1/2 by A5,ABSVALUE:def 1;
then x0 + r in ].x0 -g1,x0 +g1.[ by A6,RCOMP_1:8;
then [.x0 ,x0 +r.] c= ].x0 -g1,x0 +g1.[ by A8,RCOMP_1:17;
hence thesis by A3,A4,XBOOLE_1:1;
end;
A9: for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n>0) holds
h"(#)(f*(h+c) - f*c) is convergent & lim (h"(#)
(f*(h+c) - f*c)) = diff(f,x0)
by A1,A2,FDIFF_2:12;
A10: ex r st 0 < r & [.x0 -r,x0.] c= dom f
proof
take r = g1/2;
thus r is Real by XREAL_0:def 1;
thus r > 0 by A4,SEQ_2:3;
A11: x0 in ].x0 - g1, x0 + g1 .[ by A4,RCOMP_1:37;
abs((x0 - g1/2) -x0 ) = abs((-g1/2 + x0) -x0 ) by XCMPLX_0:def 8
.=abs((-g1/2 + x0) + -x0 ) by XCMPLX_0:def 8
.=abs(-g1/2 +( x0 + -x0) ) by XCMPLX_1:1
.=abs(-g1/2 + 0 ) by XCMPLX_0:def 6
.=abs(g1/2 )by ABSVALUE:17
.=g1/2 by A5,ABSVALUE:def 1;
then x0 - r in ].x0 -g1,x0 +g1.[ by A6,RCOMP_1:8;
then [.x0 -r ,x0 .] c= ].x0 -g1,x0 +g1.[ by A11,RCOMP_1:17;
hence thesis by A3,A4,XBOOLE_1:1;
end;
for h,c st rng c = {x0} & rng (h+c) c= dom f & (for n holds h.n < 0) holds
h"(#)(f*(h+c) - f*c) is convergent & lim(h"(#)(f*(h+c) - f*c)) = diff(f,x0)
by A1,A2,FDIFF_2:12;
hence thesis by A7,A9,A10,Th9,Th15;
end;