:: Real Function Differentiability - Part II
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received January 10, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, FDIFF_1, FUNCT_1, RCOMP_1,
PARTFUN1, ARYTM_1, VALUED_0, SEQ_2, ORDINAL2, CARD_1, RELAT_1, ARYTM_3,
XXREAL_0, COMPLEX1, NAT_1, TARSKI, VALUED_1, FUNCT_2, FUNCOP_1, XXREAL_1,
FCONT_1, SQUARE_1, XBOOLE_0, ORDINAL4, LIMFUNC1, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, FUNCT_1, FUNCT_2, VALUED_0,
VALUED_1, SEQ_1, RELSET_1, COMSEQ_2, SEQ_2, PARTFUN1, PARTFUN2, RFUNCT_1,
RCOMP_1, FCONT_1, FDIFF_1, LIMFUNC1, RECDEF_1;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3,
PROB_1, RCOMP_1, PARTFUN2, RFUNCT_1, RFUNCT_2, FCONT_1, LIMFUNC1,
FDIFF_1, VALUED_1, RECDEF_1, RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1,
NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, SEQM_3, RCOMP_1, RFUNCT_2, FDIFF_1, FCONT_3, VALUED_0,
VALUED_1, FUNCT_2, SEQ_4, SQUARE_1, SEQ_1, SEQ_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, VALUED_1;
equalities XBOOLE_0, SQUARE_1, SUBSET_1, LIMFUNC1, PROB_1, VALUED_1;
expansions TARSKI, XBOOLE_0, FDIFF_1, FUNCT_2;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQ_2, SEQM_3, SEQ_4,
ABSVALUE, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, RFUNCT_2, FCONT_1,
FDIFF_1, SCHEME1, ROLLE, FCONT_3, FUNCT_3, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, XCMPLX_0, XCMPLX_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0,
ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, XREAL_0, NUMBERS;
schemes NAT_1, RECDEF_1, SEQ_1, SCHEME1, FUNCT_2;
begin
reserve x for object;
reserve x0,r,r1,r2,g,g1,g2,p,y0 for Real;
reserve n,m,k,l for Element of NAT;
reserve a,b,d for Real_Sequence;
reserve h,h1,h2 for non-zero 0-convergent Real_Sequence;
reserve c,c1 for constant Real_Sequence;
reserve A for open Subset of REAL;
reserve f,f1,f2 for PartFunc of REAL,REAL;
reserve L for LinearFunc;
reserve R for RestFunc;
registration
let h;
cluster -h -> non-zero convergent;
coherence by SEQ_1:45;
end;
theorem Th1:
a is convergent & b is convergent & lim a = lim b & (for n holds
d.(2*n) = a.n & d.(2*n + 1) = b.n) implies d is convergent & lim d = lim a
proof
assume that
A1: a is convergent and
A2: b is convergent and
A3: lim a = lim b and
A4: for n holds d.(2*n) = a.n & d.(2*n+1) = b.n;
A5: now
let r be Real;
assume
A6: 0<r;
then consider k1 be Nat such that
A7: for m being Nat st k1 <= m holds |.a.m - lim a.| < r by A1,SEQ_2:def 7;
consider k2 be Nat such that
A8: for m being Nat st k2 <= m holds |.b.m - lim b.| < r
by A2,A6,SEQ_2:def 7;
reconsider n = max(2*k1,2*k2+1) as Nat by TARSKI:1;
take n;
let m be Nat;
assume
A9: n<=m;
then
A10: 2*k2 + 1 <= m by XXREAL_0:30;
consider n being Element of NAT such that
A11: m = 2*n or m = 2*n + 1 by SCHEME1:1;
A12: 2*k1 <= m by A9,XXREAL_0:30;
now
per cases by A11;
suppose
A13: m = 2*n;
then
A14: n >= k1 by A12,XREAL_1:68;
|.d.m - lim a.| = |.a.n - lim a.| by A4,A13;
hence |.d.m - lim a.| < r by A7,A14;
end;
suppose
A15: m = 2*n + 1;
A16: now
assume n < k2;
then 2*n < 2*k2 by XREAL_1:68;
hence contradiction by A10,A15,XREAL_1:6;
end;
|.d.m - lim a.| = |.b.n - lim a.| by A4,A15;
hence |.d.m - lim a.| < r by A3,A8,A16;
end;
end;
hence |.d.m - lim a.| < r;
end;
hence d is convergent by SEQ_2:def 6;
hence thesis by A5,SEQ_2:def 7;
end;
theorem Th2:
(for n holds a.n = 2*n) implies a is increasing sequence of NAT
proof
assume
A1: for n holds a.n = 2*n;
A2: a is increasing
proof
let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: 2*n + 0 < 2*n + 2 by XREAL_1:8;
2*n + 2 = 2*(n + 1) .= a.(n + 1) by A1;
hence a.n < a.(n+1) by A1,A4,A3;
end;
A5: now
let x;
assume x in NAT;
then reconsider n = x as Element of NAT;
a.n = 2*n by A1;
hence a.x in NAT;
end;
dom a = NAT by FUNCT_2:def 1;
hence thesis by A2,A5,FUNCT_2:3;
end;
theorem Th3:
(for n holds a.n = 2*n + 1) implies a is increasing sequence of NAT
proof
assume
A1: for n holds a.n = 2*n + 1;
A2: a is increasing
proof
let n be Nat;
A3: n in NAT by ORDINAL1:def 12;
A4: 2*n + 1+0 < 2*n + 1+2 by XREAL_1:8;
2*n + 1+2 = 2*(n + 1) + 1 .= a.(n + 1) by A1;
hence a.n < a.(n+1) by A1,A4,A3;
end;
A5: now
let x;
assume x in dom a;
then reconsider n = x as Element of NAT;
a.n = 2*n+1 by A1;
hence a.x in NAT;
end;
dom a = NAT by FUNCT_2:def 1;
hence thesis by A2,A5,FUNCT_2:3;
end;
theorem Th4:
rng c = {x0} implies c is convergent & lim c = x0 & h + c is
convergent & lim(h + c) = x0
proof
assume
A1: rng c = {x0};
thus c is convergent;
x0 in rng c by A1,TARSKI:def 1;
hence
A2: lim c = x0 by SEQ_4:25;
thus h + c is convergent;
lim h = 0;
hence lim (h + c) = 0 + x0 by A2,SEQ_2:6
.= x0;
end;
theorem Th5:
rng a = {r} & rng b = {r} implies a = b
proof
assume that
A1: rng a = {r} and
A2: rng b = {r};
now
let n;
a.n in rng a by VALUED_0:28;
then
A3: a.n = r by A1,TARSKI:def 1;
b.n in rng b by VALUED_0:28;
hence a.n = b.n by A2,A3,TARSKI:def 1;
end;
hence thesis;
end;
theorem Th6:
a is subsequence of h implies a is 0-convergent non-zero Real_Sequence
proof
assume
A1: a is subsequence of h;
then consider I be increasing sequence of NAT such that
A2: a = h*I by VALUED_0:def 17;
not ex n being Nat st a.n = 0 by A2,SEQ_1:5;
then
A3: a is non-zero by SEQ_1:5;
A4: a is convergent by A1,SEQ_4:16;
lim h = 0;
then lim a = 0 by A1,SEQ_4:17;
hence thesis by A4,A3,FDIFF_1:def 1;
end;
theorem Th7:
(for h,c st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f
holds h"(#)(f/*(h+c) - f/*c) is convergent) implies for h1,h2,c st rng c = {g}
& rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & {g} c= dom f holds lim (h1"
(#)(f/*(h1+c) - f/*c)) = lim(h2"(#)(f/*(h2+c) - f/*c))
proof
assume
A1: for h,c st rng c = {g} & rng (h+c) c= dom f & {g} c= dom f holds h"
(#)(f/*(h+c) - f/*c) is convergent;
let h1,h2,c such that
A2: rng c = {g} and
A3: rng (h1+c) c= dom f and
A4: rng (h2+c) c= dom f and
A5: {g} c= dom f;
deffunc G(Element of NAT) = h2.$1;
deffunc F(Element of NAT) = h1.$1;
consider a such that
A6: for n holds a.(2*n) = F(n) & a.(2*n + 1) = G(n) from SCHEME1:sch 2;
now
let n be Nat;
consider m being Element of NAT such that
A7: n = 2*m or n = 2*m + 1 by SCHEME1:1;
now
per cases by A7;
suppose
n = 2*m;
then a.n = h1.m by A6;
hence a.n <> 0 by SEQ_1:5;
end;
suppose
n = 2*m + 1;
then a.n = h2.m by A6;
hence a.n <> 0 by SEQ_1:5;
end;
end;
hence a.n <> 0;
end;
then
A8: a is non-zero by SEQ_1:5;
A9: lim h1 = 0;
A10: lim h2 = 0;
A11: a is convergent by A6,A9,A10,Th1;
lim a = 0 by A6,A9,A10,Th1;
then reconsider a as 0-convergent non-zero Real_Sequence
by A11,A8,FDIFF_1:def 1;
A12: rng (a + c) c= dom f
proof
let x be object;
assume x in rng (a + c);
then consider n such that
A13: x = (a + c).n by FUNCT_2:113;
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;
A16: (h1 + c).m in rng (h1 + c) by VALUED_0:28;
(a + c).n = a.n + c.n by SEQ_1:7
.= h1.m + c.n by A6,A15
.= h1.m + c.m by VALUED_0:23
.= (h1 + c).m by SEQ_1:7;
hence (a + c).n in dom f by A3,A16;
end;
suppose
A17: n = 2*m + 1;
A18: (h2 + c).m in rng (h2 + c) by VALUED_0:28;
(a + c).n = a.n + c.n by SEQ_1:7
.= h2.m + c.n by A6,A17
.= h2.m + c.m by VALUED_0:23
.= (h2 + c).m by SEQ_1:7;
hence (a + c).n in dom f by A4,A18;
end;
end;
hence thesis by A13;
end;
then
A19: a"(#)(f/*(a+c) - f/*c) is convergent by A1,A2,A5;
deffunc G(Nat) = 2*$1+1;
consider d such that
A20: for n being Nat holds d.n = G(n) from SEQ_1:sch 1;
for n being Element of NAT holds d.n = G(n) by A20;
then reconsider I2 = d as increasing sequence of NAT by Th3;
now
let n;
thus ((a"(#)(f/*(a+c) - f/*c))*I2).n = (a"(#)(f/*(a+c) - f/*c)).(I2.n) by
FUNCT_2:15
.= (a"(#)(f/*(a+c) - f/*c)).(2*n + 1) by A20
.= (a").(2*n + 1) * (f/*(a+c) - f/*c).(2*n + 1) by SEQ_1:8
.= (a").(2*n + 1) * ((f/*(a+c)).(2*n + 1) - (f/*c).(2*n + 1)) by
RFUNCT_2:1
.= (a").(2*n + 1) * (f.((a+c).(2*n+1)) - (f/*c).(2*n+1)) by A12,
FUNCT_2:108
.= (a").(2*n + 1) * (f.(a.(2*n+1) + c.(2*n+1)) - (f/*c).(2*n+1)) by
SEQ_1:7
.= (a").(2*n + 1) * (f.(h2.n + c.(2*n+1)) - (f/*c).(2*n+1)) by A6
.= (a").(2*n + 1) * (f.(h2.n + c.n) - (f/*c).(2*n+1)) by VALUED_0:23
.= (a").(2*n + 1) * (f.((h2 + c).n) - (f/*c).(2*n+1)) by SEQ_1:7
.= (a").(2*n + 1) * ((f/*(h2+c)).n - (f/*c).(2*n+1)) by A4,FUNCT_2:108
.= (a.(2*n + 1))" * ((f/*(h2+c)).n - (f/*c).(2*n+1)) by VALUED_1:10
.= (h2.n)" * ((f/*(h2+c)).n - (f/*c).(2*n+1)) by A6
.= (h2").n * ((f/*(h2+c)).n - (f/*c).(2*n+1)) by VALUED_1:10
.= (h2").n * ((f/*(h2+c)).n - f.(c.(2*n+1))) by A2,A5,FUNCT_2:108
.= (h2").n * ((f/*(h2+c)).n - f.(c.n)) by VALUED_0:23
.= (h2").n * ((f/*(h2+c)).n - (f/*c).n) by A2,A5,FUNCT_2:108
.= (h2").n * (f/*(h2+c) - (f/*c)).n by RFUNCT_2:1
.= ((h2")(#)(f/*(h2+c) - (f/*c))).n by SEQ_1:8;
end;
then
A21: (a"(#)(f/*(a+c) - f/*c))*I2 = h2"(#)(f/*(h2+c) - f/*c);
(a"(#)(f/*(a+c) - f/*c))*I2 is subsequence of a"(#)(f/*(a+c) - f/*c) by
VALUED_0:def 17;
then
A22: lim ((a"(#)(f/*(a+c) - f/*c))*I2) = lim (a"(#) (f/*(a+c) - f/*c)) by A19,
SEQ_4:17;
deffunc F(Nat) = 2*$1;
consider b such that
A23: for n being Nat holds b.n = F(n) from SEQ_1:sch 1;
for n being Element of NAT holds b.n = F(n) by A23;
then reconsider I1 = b as increasing sequence of NAT by Th2;
now
let n;
thus ((a"(#)(f/*(a+c) - f/*c))*I1).n = (a"(#)(f/*(a+c) - f/*c)).(I1.n) by
FUNCT_2:15
.= (a"(#)(f/*(a+c) - f/*c)).(2*n) by A23
.= (a").(2*n) * (f/*(a+c) - f/*c).(2*n) by SEQ_1:8
.= (a").(2*n) * ((f/*(a+c)).(2*n) - (f/*c).(2*n)) by RFUNCT_2:1
.= (a").(2*n) * (f.((a+c).(2*n)) - (f/*c).(2*n)) by A12,FUNCT_2:108
.= (a").(2*n) * (f.(a.(2*n) + c.(2*n)) - (f/*c).(2*n)) by SEQ_1:7
.= (a").(2*n) * (f.(h1.n + c.(2*n)) - (f/*c).(2*n)) by A6
.= (a").(2*n) * (f.(h1.n + c.n) - (f/*c).(2*n)) by VALUED_0:23
.= (a").(2*n) * (f.((h1 + c).n) - (f/*c).(2*n)) by SEQ_1:7
.= (a").(2*n) * ((f/*(h1+c)).n - (f/*c).(2*n)) by A3,FUNCT_2:108
.= (a.(2*n))" * ((f/*(h1+c)).n - (f/*c).(2*n)) by VALUED_1:10
.= (h1.n)" * ((f/*(h1+c)).n - (f/*c).(2*n)) by A6
.= (h1").n * ((f/*(h1+c)).n - (f/*c).(2*n)) by VALUED_1:10
.= (h1").n * ((f/*(h1+c)).n - f.(c.(2*n))) by A2,A5,FUNCT_2:108
.= (h1").n * ((f/*(h1+c)).n - f.(c.n)) by VALUED_0:23
.= (h1").n * ((f/*(h1+c)).n - (f/*c).n) by A2,A5,FUNCT_2:108
.= (h1").n * (f/*(h1+c) - (f/*c)).n by RFUNCT_2:1
.= ((h1")(#)(f/*(h1+c) - (f/*c))).n by SEQ_1:8;
end;
then
A24: (a"(#)(f/*(a+c) - f/*c))*I1 = h1"(#)(f/*(h1+c) - f/*c);
(a"(#)(f/*(a+c) - f/*c))*I1 qua Real_Sequence is subsequence of a"(#)(f
/*(a+c) - f/*c) by VALUED_0:def 17;
hence thesis by A19,A22,A24,A21,SEQ_4:17;
end;
theorem Th8:
(ex N be Neighbourhood of r st N c= dom f) implies ex h,c st rng
c = {r} & rng (h+c) c= dom f & {r} c= dom f
proof
given N be Neighbourhood of r such that
A1: N c= dom f;
reconsider r0 =r as Element of REAL by XREAL_0:def 1;
set a = seq_const r;
consider g be Real such that
A2: 0 < g and
A3: N = ].r - g, r + g.[ by RCOMP_1:def 6;
reconsider a as constant Real_Sequence;
deffunc G(Nat) = g/($1+2);
consider b such that
A4: for n being Nat holds b.n = G(n) from SEQ_1:sch 1;
A5: lim b = 0 by A4,SEQ_4:31;
A6: b is convergent by A4,SEQ_4:31;
now
let n be Nat;
0 < g/(n+2) by A2;
hence 0 <> b.n by A4;
end;
then b is non-zero by SEQ_1:5;
then reconsider b as 0-convergent non-zero Real_Sequence
by A6,A5,FDIFF_1:def 1;
take b,a;
thus rng a = {r}
proof
thus rng a c= {r}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = r by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {r};
then x = r by TARSKI:def 1
.= a.0 by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
thus rng (b+a) c= dom f
proof
let x be object;
assume x in rng (b+a);
then consider n such that
A7: x = (b+a).n by FUNCT_2:113;
0+1 < n + 2 by XREAL_1:8;
then g*1 < g*(n+2) by A2,XREAL_1:97;
then g * (n+2)" < g*(n + 2)*((n + 2)") by XREAL_1:68;
then g * ((n+2)") < g*((n + 2)*(n + 2)");
then g * (n+2)" < g * 1 by XCMPLX_0:def 7;
then g/(n+2) < g by XCMPLX_0:def 9;
then
A8: r + g/(n+2) < r + g by XREAL_1:6;
A9: r - g < r - 0 by A2,XREAL_1:15;
r + 0 < r + g/(n+2) by A2,XREAL_1:8;
then r - g < r + g/(n+2) by A9,XXREAL_0:2;
then
A10: r + g/(n+2) in {g1: r - g < g1 & g1 < r + g} by A8;
x = b.n +a.n by A7,SEQ_1:7
.= g/(n+2) + a.n by A4
.= g/(n+2) + r by SEQ_1:57;
then x in N by A3,A10,RCOMP_1:def 2;
hence thesis by A1;
end;
let x be object;
assume x in {r};
then x = r by TARSKI:def 1;
then x in N by RCOMP_1:16;
hence thesis by A1;
end;
theorem Th9:
rng a c= dom (f2*f1) implies rng a c= dom f1 & rng (f1/*a) c= dom f2
proof
assume
A1: rng a c= dom (f2*f1);
then
A2: f1.:(rng a) c= dom f2 by FUNCT_1:101;
rng a c= dom f1 by A1,FUNCT_1:101;
hence thesis by A2,VALUED_0:30;
end;
scheme
ExIncSeqofNat{ s()->Real_Sequence,P[object] }:
ex q being increasing sequence of NAT st (for n being Nat holds P[(s()*q).n]) &
for n st (for r st r = s().n holds P[r])
ex m st n = q.m
provided
A1: for n ex m st n <= m & P[s().m]
proof
defpred P[Nat,set,set] means for n,m st $2 = n & $3 = m holds n < m & P[s().
m] & for k st n < k & P[s().k] holds m <= k;
defpred R[Nat] means P[s().$1];
ex m1 be Element of NAT st 0 <= m1 & P[s().m1] by A1;
then
A2: ex m be Nat st R[m];
consider M be Nat such that
A3: R[M] & for n be Nat st R[n] holds M <= n from NAT_1:sch 5(A2);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A4: now
let n;
consider m such that
A5: n + 1 <= m and
A6: P[s().m] by A1;
take m;
thus n < m & P[s().m] by A5,A6,NAT_1:13;
end;
A7: for n being Nat
for x be Element of NAT ex y be Element of NAT st P[n,x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred R[Nat] means x < $1 & P[s().$1];
ex m st R[m] by A4;
then
A8: ex m be Nat st R[m];
consider l be Nat such that
A9: R[l] & for k be Nat st R[k] holds l <= k from NAT_1:sch 5(A8);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A9;
end;
consider F be sequence of NAT such that
A10: F.0 = M9 & for n be Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A7);
A11: rng F c= REAL by NUMBERS:19;
A12: rng F c= NAT;
A13: dom F = NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A11,RELSET_1:4;
A14: now
let n;
F.n in rng F by A13,FUNCT_1:def 3;
hence F.n is Element of NAT by A12;
end;
now
let n be Nat;
A15: n in NAT by ORDINAL1:def 12;
A16: F.(n+1) is Element of NAT by A14;
F.n is Element of NAT by A14,A15;
hence F.n < F.(n+1) by A10,A16;
end;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A17: for n st P[s().n] ex m st F.m = n
proof
defpred R[Nat] means P[s().$1] & for m holds F.m <> $1;
assume ex n st R[n];
then
A18: ex n be Nat st R[n];
consider M1 be Nat such that
A19: R[M1] & for n be Nat st R[n] holds M1 <= n from NAT_1:sch 5(A18);
defpred H[Nat] means $1 < M1 & P[s().$1] & ex m st F.m = $1;
A20: ex n being Nat st H[n]
proof
take M;
A21: M <> M1 by A10,A19;
M <= M1 by A3,A19;
hence M < M1 by A21,XXREAL_0:1;
thus P[s().M] by A3;
take 0;
thus thesis by A10;
end;
A22: for n being Nat st H[n] holds n <= M1;
consider X be Nat such that
A23: H[X] & for n being Nat st H[n] holds n <= X from NAT_1:sch 6(A22,
A20);
A24: for k st X < k & k < M1 holds not P[s().k]
proof
given k such that
A25: X < k and
A26: k < M1 and
A27: P[s().k];
now
per cases;
suppose
ex m st F.m = k;
hence contradiction by A23,A25,A26,A27;
end;
suppose
for m holds F.m <> k;
hence contradiction by A19,A26,A27;
end;
end;
hence contradiction;
end;
consider m such that
A28: F.m = X by A23;
M1 in NAT by ORDINAL1:def 12;
then
A29: F.(m+1) <= M1 by A10,A19,A23,A28;
A30: P[s().(F.(m+1))] by A10,A28;
A31: X < F.(m+1) by A10,A28;
now
assume F.(m+1) <> M1;
then F.(m+1) < M1 by A29,XXREAL_0:1;
hence contradiction by A24,A31,A30;
end;
hence contradiction by A19;
end;
take F;
set q = s()*F;
defpred S[Nat] means P[q.$1];
A32: for k being Nat st S[k] holds S[k+1]
proof
let k be Nat;
assume P[q.k];
P[k,F.k,F.(k+1)] by A10;
then P[s().(F.(k+1))];
hence thesis by FUNCT_2:15;
end;
A33: S[0] by A3,A10,FUNCT_2:15;
thus for n being Nat holds S[n] from NAT_1:sch 2(A33,A32);
let n;
assume for r st r = s().n holds P[r];
then consider m such that
A34: F.m = n by A17;
take m;
thus thesis by A34;
end;
theorem
f.x0 <> r & f is_differentiable_in x0 implies ex N be Neighbourhood of
x0 st N c= dom f & for g st g in N holds f.g <> r
by FCONT_3:7,FDIFF_1:24;
Lm1: (ex N be Neighbourhood of x0 st N c= dom f) & (for h,c st rng c = {x0} &
rng (h+c) c= dom f holds h"(#)(f/*(h+c) - f/*c) is convergent) implies f
is_differentiable_in x0 & for h,c st rng c = {x0} & rng (h+c) c= dom f holds
diff(f,x0) = lim (h"(#)(f/*(h+c) - f/*c))
proof
deffunc G(Real) = In(0,REAL);
defpred P[object] means $1 in REAL;
given N be Neighbourhood of x0 such that
A1: N c= dom f;
assume
A2: for h,c st rng c = {x0} & rng (h+c) c= dom f holds h"(#)(f/*(h+c) -
f/*c) is convergent;
then
A3: for h,c holds rng c = {x0} & rng (h+c) c= dom f & {x0} c= dom f implies
h"(#)(f/*(h+c) - f/*c) is convergent;
consider r be Real such that
A4: 0 < r and
A5: N = ].x0 - r,x0 + r.[ by RCOMP_1:def 6;
consider h,c such that
A6: rng c = {x0} and
A7: rng (h+c) c= dom f and
A8: {x0} c= dom f by A1,Th8;
set l = lim (h"(#)(f/*(h+c) - f/*c));
deffunc F(Real) = In(l * $1,REAL);
consider L be PartFunc of REAL,REAL such that
A9: for g being Element of REAL holds g in dom L iff P[g] and
A10: for g being Element of REAL st g in dom L holds L.g = F(g)
from SEQ_1:sch 3;
for g holds g in dom L iff P[g] by A9;
then
A11: dom L = REAL by FDIFF_1:1;
A12: for g holds L.g = l * g
proof let g;
reconsider gg=g as Element of REAL by XREAL_0:def 1;
A13: gg in dom L by A11;
thus L.g = L.gg
.= F(gg) by A13,A10
.= l * gg
.= l * g;
end;
A14: L is total by A11,PARTFUN1:def 2;
deffunc F1(Real) = In($1 + x0,REAL);
consider T be PartFunc of REAL,REAL such that
A15: for g being Element of REAL holds g in dom T iff P[g] and
A16: for g being Element of REAL st g in dom T holds T.g = F1(g)
from SEQ_1:sch 3;
for g holds g in dom T iff P[g] by A15;
then
A17: dom T = REAL by FDIFF_1:1;
deffunc F2(Real) = In((f*T).$1 - f.x0,REAL);
consider T1 be PartFunc of REAL,REAL such that
A18: for g being Element of REAL holds g in dom T1 iff P[g] and
A19: for g being Element of REAL st g in dom T1 holds T1.g = F2(g)
from SEQ_1:sch 3;
deffunc F3(Real) = In((T1 - L).$1,REAL);
for g holds g in dom T1 iff P[g] by A18;
then
A20: dom T1 = REAL by FDIFF_1:1;
then
A21: T1 is total by PARTFUN1:def 2;
reconsider L as LinearFunc by A14,A12,FDIFF_1:def 3;
defpred P[set] means $1 in ].-r,r.[;
consider R be PartFunc of REAL,REAL such that
A22: R is total and
A23: for g being Element of REAL st g in dom R
holds (P[g] implies R.g = F3(g))
& (not P[g] implies R.g = G(g)) from SCHEME1:sch 8;
A24: dom R = REAL by A22,PARTFUN1:def 2;
A25: now
let n;
c.n in {x0} by A6,VALUED_0:28;
hence c.n = x0 by TARSKI:def 1;
end;
now
let h1;
A26: lim h1 = 0;
consider k being Nat such that
A27: for n being Nat st k <= n holds |.h1.n - 0.| < r
by A4,A26,SEQ_2:def 7;
set h2 = h1^\k;
A28: now
let n;
|.h1.(n+k) - 0.| < r by A27,NAT_1:12;
then h1.(n+k) in ].0 - r,0 + r.[ by RCOMP_1:1;
hence h2.n in ].-r,r.[ by NAT_1:def 3;
end;
A29: rng (h2 + c) c= dom f
proof
let x be object;
assume x in rng (h2 + c);
then consider n such that
A30: x = (h2 + c).n by FUNCT_2:113;
h2.n in ].-r,r.[ by A28;
then h2.n in {g: -r < g & g < r} by RCOMP_1:def 2;
then
A31: ex g st g = h2.n & -r < g & g < r;
then
A32: h2.n + x0 < x0 + r by XREAL_1:6;
x0 + -r < h2.n + x0 by A31,XREAL_1:6;
then
A33: h2.n + x0 in {g: x0 - r < g & g < x0 + r} by A32;
x = h2.n + c.n by A30,SEQ_1:7
.= h2.n + x0 by A25;
then x in ].x0 - r,x0 + r.[ by A33,RCOMP_1:def 2;
hence thesis by A1,A5;
end;
set b = h2"(#)(L/*h2);
set a = h2"(#)(T1/*h2);
A34: (h1"(#)(R/*h1))^\k = ((h1")^\k) (#) ((R/*h1)^\k) by SEQM_3:19
.= h2" (#) ((R/*h1)^\k) by SEQM_3:18
.= h2" (#) (R/*h2) by A22,VALUED_0:29;
A35: a - b = h2"(#)(T1/*h2 - L/*h2) by SEQ_1:21
.= h2"(#)((T1-L)/*h2) by A14,A21,RFUNCT_2:13;
A36: now
let n;
A37: h2.n in ].-r,r.[ by A28;
thus (a - b).n = (h2").n * ((T1-L)/*h2).n by A35,SEQ_1:8
.= (h2").n * (T1 - L).(h2.n) by A14,A21,FUNCT_2:115
.= (h2").n * F3(h2.n)
.= (h2").n * R.(h2.n) by A23,A24,A37
.= (h2").n * (R/*h2).n by A22,FUNCT_2:115
.= (h2" (#) (R/*h2)).n by SEQ_1:8;
end;
reconsider ll=l as Element of REAL by XREAL_0:def 1;
A38: now
let n be Nat;
A39: n in NAT by ORDINAL1:def 12;
A40: h2.n <> 0 by SEQ_1:5;
A41: h2.n in dom L by A11,XREAL_0:def 1;
thus b.n = (h2").n * (L/*h2).n by SEQ_1:8
.= (h2").n * L.(h2.n) by A14,A39,FUNCT_2:115
.= (h2").n * F(h2.n) by A10,A41
.= (h2").n * (h2.n) * l
.= (h2.n)" * (h2.n) * l by VALUED_1:10
.= 1 * l by A40,XCMPLX_0:def 7
.= ll;
end;
then
A42: b is constant by VALUED_0:def 18;
now
let n be Element of NAT;
A43: c.n = x0 by A25;
thus a.n = (h2").n * (T1/*h2).n by SEQ_1:8
.= (h2").n * T1.(h2.n) by A21,FUNCT_2:115
.= (h2").n * F2(h2.n) by A19,A20
.= (h2").n * ((f*T).(h2.n) - f.x0)
.= (h2").n * (f.(T.(h2.n)) - f.x0) by A17,FUNCT_1:13
.= (h2").n * (f.(F1(h2.n)) - f.x0) by A17,A16
.= (h2").n * (f.(h2.n + x0) - f.x0)
.= (h2").n * (f.((h2 + c).n) - f.(c.n)) by A43,SEQ_1:7
.= (h2").n * (f.((h2 + c).n) - (f/*c).n) by A6,A8,FUNCT_2:108
.= (h2").n * ((f/*(h2+c)).n - (f/*c).n) by A29,FUNCT_2:108
.= (h2").n * ((f/*(h2+c)) - (f/*c)).n by RFUNCT_2:1
.= (h2" (#) ((f/*(h2+c)) - (f/*c))).n by SEQ_1:8;
end;
then
A44: a = h2" (#) ((f/*(h2+c)) - (f/*c));
then
A45: a is convergent by A2,A6,A29;
then a - b is convergent by A42;
then
A46: h2"(#)(R/*h2) is convergent by A36,FUNCT_2:63;
hence h1"(#)(R/*h1) is convergent by A34,SEQ_4:21;
A47: l = lim a by A3,A6,A7,A8,A29,A44,Th7;
lim b = b.0 by A42,SEQ_4:25
.= l by A38;
then lim (a - b) = l - l by A45,A47,A42,SEQ_2:12
.= 0;
then lim (h2"(#) (R/*h2)) = 0 by A36,FUNCT_2:63;
hence lim (h1"(#)(R/*h1)) = 0 by A46,A34,SEQ_4:22;
end;
then reconsider R as RestFunc by A22,FDIFF_1:def 2;
A48: now
take N;
thus N c= dom f by A1;
take L,R;
1 in REAL by NUMBERS:19;
hence L.1 = F(1) by A10,A11
.= l;
let g1;
assume g1 in N;
then
A49: g1 - x0 in ].-r,r.[ by A5,FCONT_3:2;
reconsider gg1 = g1, xx0= x0 as Element of REAL by XREAL_0:def 1;
thus L.(g1 - x0)+R.(g1 - x0)
= L.(g1 - x0)+F3(g1 - x0) by A23,A24,A49
.= L.(g1-x0)+(T1-L).(g1-x0)
.= L.(gg1 - xx0) + (T1.(g1 - x0) - L.(g1 - x0))
by A14,A21,RFUNCT_1:56
.= L.(gg1 - xx0) + (F2(g1 - x0) - L.(g1 - x0)) by A19,A20
.= (f*T).(gg1 - xx0) - f.x0
.= f.(T.(gg1 - xx0)) - f.x0 by A17,FUNCT_1:13
.= f.(F1(gg1 - xx0)) - f.x0 by A17,A16
.= f.(gg1 - xx0 + xx0) - f.x0
.= f.g1 - f.x0;
end;
thus f is_differentiable_in x0
by A48;
then
A50: diff(f,x0) = l by A48,FDIFF_1:def 5;
let h1,c1;
assume that
A51: rng c1 = {x0} and
A52: rng (h1 + c1) c= dom f;
c1 = c by A6,A51,Th5;
hence thesis by A3,A6,A7,A8,A50,A52,Th7;
end;
theorem Th11:
f is_differentiable_in x0 iff (ex N be Neighbourhood of x0 st N
c= dom f) & for h,c st rng c = {x0} & rng (h + c) c= dom f holds h"(#)(f/*(h+c)
- f/*c) is convergent
proof
thus f is_differentiable_in x0 implies (ex N be Neighbourhood of x0 st N c=
dom f) & for h,c st rng c = {x0} & rng (h + c) c= dom f holds h"(#)(f/*(h+c) -
f/*c) is convergent
proof
assume
A1: f is_differentiable_in x0;
then consider N be Neighbourhood of x0 such that
A2: N c= dom f and
ex L be LinearFunc, R be RestFunc st
for g st g in N holds f.g - f.x0 = L.(g -
x0) + R.(g - x0);
thus ex N be Neighbourhood of x0 st N c= dom f by A2;
let h,c such that
A3: rng c = {x0} and
A4: rng (h + c) c= dom f;
A5: lim h = 0;
consider r be Real such that
A6: 0 < r and
A7: N = ].x0 - r,x0 + r.[ by RCOMP_1:def 6;
consider k being Nat such that
A8: for n being Nat st k <= n holds |.h.n - 0.| < r by A5,A6,SEQ_2:def 7;
set h1 = h^\k;
rng (h1 + c) c= N
proof
let x be object;
assume x in rng (h1 + c);
then consider n such that
A9: x = (h1 + c).n by FUNCT_2:113;
c.n in rng c by VALUED_0:28;
then c.n = x0 by A3,TARSKI:def 1;
then
A10: x = h1.n + x0 by A9,SEQ_1:7
.= h.(n+k) + x0 by NAT_1:def 3;
|.h.(n+k) - 0.| < r by A8,NAT_1:12;
then h.(n+k) in ].0 - r, 0 + r.[ by RCOMP_1:1;
then h.(n+k) in {g: -r < g & g < r} by RCOMP_1:def 2;
then
A11: ex g st g = h.(n+k) & -r < g & g < r;
then
A12: h.(n+k) + x0 < x0 + r by XREAL_1:6;
x0 + -r < h.(n+k) + x0 by A11,XREAL_1:6;
then h.(n+k) + x0 in {g: x0 - r < g & g < x0 + r} by A12;
hence thesis by A7,A10,RCOMP_1:def 2;
end;
then
A13: h1"(#)(f/*(h1+c) - f/*c) is convergent by A1,A2,A3,FDIFF_1:12;
A14: {x0} c= dom f
proof
let x be object;
assume x in {x0};
then
A15: x = x0 by TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence thesis by A2,A15;
end;
c^\k = c by VALUED_0:26;
then h1"(#)(f/*(h1+c) - f/*c) = h1"(#)(f/*((h+c)^\k) - f/*(c^\k)) by
SEQM_3:15
.= h1"(#)(((f/*(h+c))^\k) - f/*(c^\k)) by A4,VALUED_0:27
.= h1"(#)(((f/*(h+c))^\k) - ((f/*c)^\k)) by A3,A14,VALUED_0:27
.= h1"(#)((f/*(h+c) - (f/*c))^\k) by SEQM_3:17
.= ((h")^\k)(#)((f/*(h+c) - (f/*c))^\k) by SEQM_3:18
.= ((h")(#)(f/*(h+c) - (f/*c)))^\k by SEQM_3:19;
hence thesis by A13,SEQ_4:21;
end;
assume that
A16: ex N be Neighbourhood of x0 st N c= dom f and
A17: for h,c st rng c = {x0} & rng (h + c) c= dom f holds h"(#)(f/*(h+c)
- f/*c) is convergent;
thus thesis by A16,A17,Lm1;
end;
theorem Th12:
f is_differentiable_in x0 & diff(f,x0) = g iff
(ex N be Neighbourhood of x0 st N c= dom f) &
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)) = g
proof
thus f is_differentiable_in x0 & diff(f,x0) = g implies (ex N be
Neighbourhood of x0 st N c= dom f) & 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))
= g
proof
assume that
A1: f is_differentiable_in x0 and
A2: diff(f,x0) = g;
thus ex N be Neighbourhood of x0 st N c= dom f by A1;
A3: for h,c st rng c = {x0} & rng (h + c) c= dom f holds h"(#)(f/*(h+c) -
f /*c) is convergent by A1,Th11;
ex N be Neighbourhood of x0 st N c= dom f by A1;
hence thesis by A2,A3,Lm1;
end;
assume that
A4: ex N be Neighbourhood of x0 st N c= dom f and
A5: 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)) = g;
A6: for h,c holds rng c = {x0} & rng (h + c) c= dom f implies h"(#)(f/*(h+c)
- f/*c) is convergent by A5;
hence f is_differentiable_in x0 by A4,Lm1;
consider h,c such that
A7: rng c = {x0} and
A8: rng (h+c) c= dom f and
{x0} c= dom f by A4,Th8;
lim (h"(#)(f/*(h+c) - f/*c)) = g by A5,A7,A8;
hence thesis by A4,A6,A7,A8,Lm1;
end;
Lm2: (ex N be Neighbourhood of x0 st N c= dom (f2*f1)) & f1
is_differentiable_in x0 & f2 is_differentiable_in f1.x0 implies f2*f1
is_differentiable_in x0 & diff(f2*f1,x0) = diff(f2,f1.x0)*diff(f1,x0)
proof
given N be Neighbourhood of x0 such that
A1: N c= dom (f2*f1);
assume that
A2: f1 is_differentiable_in x0 and
A3: f2 is_differentiable_in f1.x0;
for h,c st rng c = {x0} & rng (h + c) c= dom (f2*f1) holds h"(#)((f2*f1)
/*(h+c) - (f2*f1)/*c) is convergent & lim (h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c))
= diff(f2,f1.x0)*diff(f1,x0)
proof
let h,c;
assume that
A4: rng c = {x0} and
A5: rng (h + c) c= dom (f2*f1);
A6: rng (h + c) c= dom f1 by A5,Th9;
set a = f1/*c;
A7: now
let n;
c.n in rng c by VALUED_0:28;
hence c.n = x0 by A4,TARSKI:def 1;
end;
A8: rng c c= dom (f2*f1)
proof
let x be object;
assume x in rng c;
then
A9: ex n st c.n = x by FUNCT_2:113;
x0 in N by RCOMP_1:16;
then x0 in dom (f2*f1) by A1;
hence thesis by A7,A9;
end;
set d = f1/*(h+c) - f1/*c;
A10: lim h = 0;
lim c = c.0 by SEQ_4:25;
then lim c = x0 by A7;
then
A11: lim (h + c) = 0 + x0 by A10,SEQ_2:6
.= x0;
A12: f1 is_continuous_in x0 by A2,FDIFF_1:24;
then
A13: f1/*(h+c) is convergent by A6,A11,FCONT_1:def 1;
A14: f1.x0 = lim (f1/*(h+c)) by A6,A11,A12,FCONT_1:def 1;
A15: rng (f1/*(h+c)) c= dom f2 by A5,Th9;
A16: rng c c= dom f1
proof
let x be object;
assume x in rng c;
then
A17: x = x0 by A4,TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence thesis by A1,A17,FUNCT_1:11;
end;
A18: rng a = { f1.x0 }
proof
thus rng a c= { f1.x0 }
proof
let x be object;
assume x in rng a;
then consider n such that
A19: a.n = x by FUNCT_2:113;
c.n = x0 by A7;
then x = f1.x0 by A16,A19,FUNCT_2:108;
hence thesis by TARSKI:def 1;
end;
let x be object;
A20: a.0 in rng a by VALUED_0:28;
assume x in {f1.x0};
then
A21: x = f1.x0 by TARSKI:def 1;
c.0 = x0 by A7;
hence thesis by A16,A21,A20,FUNCT_2:108;
end;
A22: rng a c= dom f2
proof
let x be object;
assume x in rng a;
then
A23: x = f1.x0 by A18,TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence thesis by A1,A23,FUNCT_1:11;
end;
A24: now
let n be Nat;
a.n in rng a by VALUED_0:28;
then
A25: a.n = f1.x0 by A18,TARSKI:def 1;
a.(n+1) in rng a by VALUED_0:28;
hence a.n = a.(n+1) by A18,A25,TARSKI:def 1;
end;
then a is constant by VALUED_0:25;
then
A26: d is convergent by A13;
reconsider a as constant Real_Sequence by A24,VALUED_0:25;
a.0 in rng a by VALUED_0:28;
then a.0 = f1.x0 by A18,TARSKI:def 1;
then lim a = f1.x0 by SEQ_4:25;
then
A27: lim d = f1.x0 - f1.x0 by A13,A14,SEQ_2:12
.= 0;
h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c) is convergent & lim (h"(#)((f2*f1)
/*(h+c) - (f2*f1)/*c)) = diff(f2,f1.x0)*diff(f1,x0)
proof
per cases;
suppose
ex k st for n st k <= n holds (f1/*(h+c)).n <> f1.x0;
then consider k such that
A28: for n st k <= n holds (f1/*(h+c)).n <> f1.x0;
now
given n being Nat such that
A29: (d^\k).n = 0;
0 = d.(n + k) by A29,NAT_1:def 3
.= (f1/*(h+c)).(n+k) - (f1/*c).(n+k) by RFUNCT_2:1
.= (f1/*(h+c)).(n+k) - f1.(c.(n+k)) by A16,FUNCT_2:108
.= (f1/*(h+c)).(n+k) - f1.x0 by A7;
hence contradiction by A28,NAT_1:12;
end;
then
A30: d^\k is non-zero by SEQ_1:5;
set c1 = c^\k;
set h1 = h^\k;
set a1 = a^\k;
set s = h1"(#)(f1/*(h1 + c1) - f1/*c1);
A31: now
let n;
thus (d + a).n = d.n + a.n by SEQ_1:7
.= (f1/*(h+c)).n - a.n + a.n by RFUNCT_2:1
.= (f1/*(h+c)).n;
end;
lim (d^\k) = 0 by A26,A27,SEQ_4:20;
then reconsider d1 = d^\k as 0-convergent non-zero Real_Sequence
by A26,A30,FDIFF_1:def 1;
set t = d1"(#)(f2/*(d1 + a1) - f2/*a1);
d1 + a1 = (d + a)^\k by SEQM_3:15;
then
A32: d1 + a1 = (f1/*(h+c))^\k by A31,FUNCT_2:63;
rng ((f1/*(h+c))^\k) c= rng (f1/*(h+c)) by VALUED_0:21;
then
A33: rng (d1 + a1) c= dom f2 by A15,A32;
A34: rng a1 = {f1.x0} by A18,VALUED_0:26;
then
A35: lim t = diff(f2,f1.x0) by A3,A33,Th12;
diff(f2,f1.x0) = diff(f2,f1.x0);
then
A36: t is convergent by A3,A34,A33,Th12;
rng ((h + c)^\k) c= rng (h + c) by VALUED_0:21;
then rng ((h + c)^\k) c= dom f1 by A6;
then
A37: rng (h1 + c1) c= dom f1 by SEQM_3:15;
A38: rng c1 = {x0} by A4,VALUED_0:26;
diff(f1,x0) = diff(f1,x0);
then
A39: s is convergent by A2,A38,A37,Th12;
A40: t(#)s = d1"(#)(f2/*(d1+a1) - f2/*a1) (#) ((f1/*((h+c)^\k) - f1/*
c1) (#)h1") by SEQM_3:15
.= d1"(#)(f2/*(d1+a1) - f2/*a1) (#) (((f1/*(h+c))^\k - f1/*c1)(#)
h1") by A6,VALUED_0:27
.= d1"(#)(f2/*(d1+a1) - f2/*a1) (#) (((f1/*(h+c))^\k - (f1/*c)^\k)
(#)h1") by A16,VALUED_0:27
.= ((f2/*(d1+a1) - f2/*a1)/"d1) (#) (d1(#)h1") by SEQM_3:17
.= ((f2/*(d1+a1) - f2/*a1)/"d1) (#) d1(#)h1" by SEQ_1:14
.= (f2/*(d1+a1) - f2/*a1) (#) h1" by SEQ_1:37
.= ((f2/*(f1/*(h+c)))^\k - f2/*a1) (#) h1" by A15,A32,VALUED_0:27
.= (((f2*f1)/*(h+c))^\k - f2/*a1) (#) h1" by A5,VALUED_0:31
.= (((f2*f1)/*(h+c))^\k - ((f2/*a)^\k)) (#) h1" by A22,VALUED_0:27
.= (((f2*f1)/*(h+c))^\k - (((f2*f1)/*c)^\k)) (#) h1" by A8,
VALUED_0:31
.= (((f2*f1)/*(h+c) - (f2*f1)/*c)^\k) (#) h1" by SEQM_3:17
.= (((f2*f1)/*(h+c) - (f2*f1)/*c)^\k) (#) ((h")^\k) by SEQM_3:18
.= (h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c))^\k by SEQM_3:19;
then
A41: (h"(#) ((f2*f1)/*(h+c) - (f2*f1)/*c))^\k is convergent by A39,A36;
hence h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c) is convergent by SEQ_4:21;
lim s = diff(f1,x0) by A2,A38,A37,Th12;
then lim ((h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c))^\k) = diff(f2,f1.x0) *
diff(f1,x0 ) by A40,A39,A36,A35,SEQ_2:15;
hence thesis by A41,SEQ_4:22;
end;
suppose
A42: for k ex n st k <= n & (f1/*(h+c)).n = f1.x0;
defpred P[object] means $1 = f1.x0;
A43: for k ex n st k <= n & P[(f1/*(h+c)).n] by A42;
consider I1 be increasing sequence of NAT such that
A44: for n being Nat holds P[(f1/*(h+c)*I1).n] and
for n st for r st r = (f1/*(h+c)).n holds P[r] ex m st n = I1.m
from ExIncSeqofNat(A43);
(h*I1) is subsequence of h by VALUED_0:def 17;
then reconsider h1 = h*I1 as 0-convergent non-zero Real_Sequence
by Th6;
set c1 = c*I1;
A45: c1 is subsequence of c by VALUED_0:def 17;
then
A46: c1 = c by VALUED_0:26;
A47: rng c1 = {x0} by A4,A45,VALUED_0:26;
reconsider c1 as constant Real_Sequence;
A48: now
let g be Real such that
A49: 0 < g;
reconsider n = 0 as Nat;
take n;
let m be Nat such that
n <= m;
A50: m in NAT by ORDINAL1:def 12;
|.(h1"(#)(f1/*(h1+c1) - f1/*c1)).m - 0.| = |.(h1").m *(f1/*(
h1+c1) - f1/*c1).m.| by SEQ_1:8
.= |.(h1").m *((f1/*(h1+c1)).m - (f1/*c1).m).| by RFUNCT_2:1
.= |.(h1").m *((f1/*(h1+c1)).m - f1.(c.m)).| by A16,A46,A50,
FUNCT_2:108
.= |.(h1").m *((f1/*(h1+c1)).m - f1.x0).| by A7,A50
.= |.(h1").m *((f1/*((h+c)*I1)).m - f1.x0).| by RFUNCT_2:2
.= |.(h1").m *((f1/*(h+c)*I1).m - f1.x0).| by A6,FUNCT_2:110
.= |.(h1").m *(f1.x0 - f1.x0).| by A44
.= 0 by ABSVALUE:2;
hence |.(h1"(#)(f1/*(h1+c1) - f1/*c1)).m - 0.| < g by A49;
end;
(h + c)*I1 is subsequence of (h + c) by VALUED_0:def 17;
then rng ((h + c)*I1) c= rng (h + c) by VALUED_0:21;
then rng ((h + c)*I1) c= dom f1 by A6;
then
A51: rng (h1 + c1) c= dom f1 by RFUNCT_2:2;
then
A52: lim (h1"(#)(f1/*(h1+c1) - f1/*c1)) = diff(f1,x0) by A2,A47,Th12;
diff(f1,x0) = diff(f1,x0);
then h1"(#)(f1/*(h1+c1) - f1/*c1) is convergent by A2,A47,A51,Th12;
then
A53: diff(f1,x0) = 0 by A52,A48,SEQ_2:def 7;
now
per cases;
suppose
ex k st for n st k <= n holds (f1/*(h+c)).n = f1.x0;
then consider k such that
A54: for n st k <= n holds (f1/*(h+c)).n = f1.x0;
A55: now
let g be Real such that
A56: 0 < g;
reconsider n = k as Nat;
take n;
let m be Nat;
A57: m in NAT by ORDINAL1:def 12;
assume n <= m;
then
A58: (f1/*(h+c)).m = f1.x0 by A54,A57;
|.(h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c)).m - diff(f2,f1.x0
)*diff(f1, x0 ) .| = |.(h").m * ((f2*f1)/*(h+c) - (f2*f1)/*c).m.| by A53,
SEQ_1:8
.= |.(h").m * (((f2*f1)/*(h+c)).m - ((f2*f1)/*c).m).| by
RFUNCT_2:1
.= |.(h").m * ((f2/*(f1/*(h+c))).m - ((f2*f1)/*c).m).| by A5,
VALUED_0:31
.= |.(h").m * (f2.((f1/*(h+c)).m) - ((f2*f1)/*c).m).| by A15,
FUNCT_2:108,A57
.= |.(h").m * (f2.(f1.x0) - (f2/*(f1/*c)).m).| by A8,A58,
VALUED_0:31
.= |.(h").m * (f2.(f1.x0) - f2.((f1/*c).m)).| by A22,
FUNCT_2:108,A57
.= |.(h").m * (f2.(f1.x0) - f2.(f1.(c.m))).| by A16,
FUNCT_2:108,A57
.= |.(h").m * (f2.(f1.x0) - f2.(f1.x0)).| by A7,A57
.= 0 by ABSVALUE:2;
hence
|.(h"(#) ((f2*f1)/*(h+c) - (f2*f1)/*c)).m - diff(f2,f1.x0
)*diff(f1,x0).|<g by A56;
end;
hence h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c) is convergent by
SEQ_2:def 6;
hence lim (h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c)) = diff(f2,f1.x0)*
diff(f1,x0) by A55,SEQ_2:def 7;
end;
suppose
A59: for k ex n st k <= n & (f1/*(h+c)).n <> f1.x0;
defpred P[object] means $1 <> f1.x0;
A60: for k ex n st k <= n & P[(f1/*(h+c)).n] by A59;
consider I2 be increasing sequence of NAT such that
A61: for n being Nat holds P[(f1/*(h+c)*I2).n] and
A62: for n st for r st r = (f1/*(h+c)).n holds P[r] ex m st n
= I2.m from ExIncSeqofNat(A60);
now
given n being Nat such that
A63: (d*I2).n = 0;
A64: n in NAT by ORDINAL1:def 12;
then 0 = d.(I2.n) by A63,FUNCT_2:15
.= (f1/*(h+c)).(I2.n) - (f1/*c).(I2.n) by RFUNCT_2:1
.= (f1/*(h+c)).(I2.n) - f1.(c.(I2.n)) by A16,FUNCT_2:108
.= (f1/*(h+c)).(I2.n) - f1.x0 by A7
.= (f1/*(h+c)*I2).n - f1.x0 by FUNCT_2:15,A64;
hence contradiction by A61;
end;
then
A65: (d*I2) is non-zero by SEQ_1:5;
(h*I2) is subsequence of h by VALUED_0:def 17;
then reconsider h2 = h*I2 as 0-convergent non-zero
Real_Sequence by Th6;
set a1 = a*I2;
set c2 = c*I2;
reconsider c2 as constant Real_Sequence;
set s = h2"(#)(f1/*(h2+c2) - f1/*c2);
A66: d*I2 is subsequence of d by VALUED_0:def 17;
then
A67: d*I2 is convergent by A26,SEQ_4:16;
lim (d*I2) = 0 by A26,A27,A66,SEQ_4:17;
then reconsider d1 = d*I2 as 0-convergent non-zero
Real_Sequence by A67,A65,FDIFF_1:def 1;
set t = d1"(#)(f2/*(d1+a1) - f2/*a1);
a1 is subsequence of a by VALUED_0:def 17;
then
A68: rng a1 = {f1.x0} by A18,VALUED_0:26;
A69: now
let n;
thus (d + a).n = d.n + a.n by SEQ_1:7
.= (f1/*(h+c)).n - a.n + a.n by RFUNCT_2:1
.= (f1/*(h+c)).n;
end;
d1 + a1 = (d + a)*I2 by RFUNCT_2:2;
then
A70: d1 + a1 = f1/*(h+c)*I2 by A69,FUNCT_2:63;
A71: t(#)s = d1"(#)(f2/*(d1+a1) - f2/*a1) (#) ((f1/*((h + c)*I2)
- f1/*c2)(#)h2") by RFUNCT_2:2
.= d1"(#)(f2/*(d1+a1) - f2/*a1) (#) ((f1/*(h+c)*I2 - f1/*c2)
(#)h2") by A6,FUNCT_2:110
.= d1"(#)(f2/*(d1+a1) - f2/*a1) (#) ((f1/*(h+c)*I2 - f1/*c*I2)
(#)h2") by A16,FUNCT_2:110
.= ((f2/*(d1+a1) - f2/*a1)/"d1) (#) (d1(#)h2") by RFUNCT_2:2
.= ((f2/*(d1+a1) - f2/*a1)/"d1) (#) d1(#)h2" by SEQ_1:14
.= (f2/*(d1+a1) - f2/*a1) (#) h2" by SEQ_1:37
.= (f2/*(f1/*(h+c))*I2 - f2/*a1) (#) h2" by A15,A70,FUNCT_2:110
.= ((f2*f1)/*(h+c)*I2 - f2/*a1) (#) h2" by A5,VALUED_0:31
.= (((f2*f1)/*(h+c))*I2 - (f2/*a*I2)) (#) h2" by A22,FUNCT_2:110
.= (((f2*f1)/*(h+c))*I2 - (((f2*f1)/*c)*I2)) (#) h2" by A8,
VALUED_0:31
.= (((f2*f1)/*(h+c) - (f2*f1)/*c)*I2) (#) h2" by RFUNCT_2:2
.= (((f2*f1)/*(h+c) - (f2*f1)/*c)*I2) (#) ((h")*I2) by RFUNCT_2:5
.= (h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c))*I2 by RFUNCT_2:2;
reconsider a1 as constant Real_Sequence;
f1/*(h+c)*I2 is subsequence of f1/*(h+c) by VALUED_0:def 17;
then rng (f1/*(h+c)*I2) c= rng (f1/*(h+c)) by VALUED_0:21;
then
A72: rng (d1 + a1) c= dom f2 by A15,A70;
(h + c)*I2 is subsequence of (h + c) by VALUED_0:def 17;
then rng ((h + c)*I2) c= rng (h + c) by VALUED_0:21;
then rng ((h + c)*I2) c= dom f1 by A6;
then
A73: rng (h2 + c2) c= dom f1 by RFUNCT_2:2;
c2 is subsequence of c by VALUED_0:def 17;
then
A74: rng c2 = {x0} by A4,VALUED_0:26;
then
A75: lim s = diff(f1,x0) by A2,A73,Th12;
diff(f1,x0) = diff(f1,x0);
then
A76: s is convergent by A2,A74,A73,Th12;
diff(f2,f1.x0) = diff(f2,f1.x0);
then
A77: t is convergent by A3,A68,A72,Th12;
then
A78: (h"(#) ((f2*f1)/*(h+c) - (f2*f1)/*c))*I2 is convergent by A71,A76;
lim t = diff(f2,f1.x0) by A3,A68,A72,Th12;
then
A79: lim ((h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c))*I2) = diff(f2,f1.
x0) * diff(f1,x0) by A71,A76,A75,A77,SEQ_2:15;
A80: now
set DF = diff(f2,f1.x0) * diff(f1,x0);
let g be Real such that
A81: 0 < g;
consider k being Nat such that
A82: for m being Nat st k <= m holds |.((h"(#)((f2*f1)/*(h+c)-(f2*
f1)/*c))*I2).m - DF.|<g by A78,A79,A81,SEQ_2:def 7;
A83: k in NAT by ORDINAL1:def 12;
reconsider n = I2.k as Nat;
take n;
let m be Nat such that
A84: n <= m;
A85: m in NAT by ORDINAL1:def 12;
now
per cases;
suppose
A86: (f1/*(h+c)).m = f1.x0;
|.(h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c)).m - DF.| =
|.(h").m * (((f2*f1)/*(h+c) - (f2*f1)/*c).m).| by A53,SEQ_1:8
.= |.(h").m * (((f2*f1)/*(h+c)).m - ((f2*f1)/*c).m).|
by RFUNCT_2:1
.= |.(h").m*(((f2*f1)/*(h+c)).m -(f2/*(f1/*c)).m).| by A8,
VALUED_0:31
.= |.(h").m*(((f2*f1)/*(h+c)).m -f2.((f1/*c).m)).| by A22,
FUNCT_2:108,A85
.= |.(h").m*(((f2*f1)/*(h+c)).m -f2.(f1.(c.m))).| by A16,
FUNCT_2:108,A85
.= |.(h").m * (((f2*f1)/*(h+c)).m - f2.(f1.x0)).|
by A7,A85
.= |.(h").m *((f2/*(f1/*(h+c))).m - f2.(f1.x0)).| by A5,
VALUED_0:31
.= |.(h").m*(f2.(f1.x0) - f2.(f1.x0)).| by A15,A86,
FUNCT_2:108,A85
.= 0 by ABSVALUE:2;
hence
|.(h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c)).m - diff(f2,f1
.x0)*diff(f1,x0).|<g by A81;
end;
suppose
(f1/*(h+c)).m <> f1.x0;
then for r1 holds (f1/*(h+c)).m=r1 implies r1<>f1.x0;
then consider l such that
A87: m = I2.l by A62,A85;
dom I2 = NAT by FUNCT_2:def 1;
then l >= k by A84,A87,VALUED_0:def 13,A83;
then |.((h"(#)((f2*f1)/*(h+c)-(f2*f1)/*c))*I2).l - DF.| <
g by A82;
hence |.(h"(#)((f2*f1)/*(h+c)-(f2*f1)/*c)).m - DF.| < g by
A87,FUNCT_2:15;
end;
end;
hence
|.(h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c)).m - diff(f2,f1.x0)
*diff(f1,x0).|<g;
end;
hence h"(#)((f2*f1)/*(h+c) - (f2*f1)/*c) is convergent by
SEQ_2:def 6;
hence lim (h"(#) ((f2*f1)/*(h+c) - (f2*f1)/*c)) = diff(f2,f1.x0)*
diff(f1,x0) by A80,SEQ_2:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by A1,Th12;
end;
theorem Th13:
f1 is_differentiable_in x0 & f2 is_differentiable_in f1.x0
implies f2*f1 is_differentiable_in x0 & diff(f2*f1,x0) = diff(f2,f1.x0)*diff(f1
,x0)
proof
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in f1.x0;
consider N2 be Neighbourhood of f1.x0 such that
A3: N2 c= dom f2 by A2;
f1 is_continuous_in x0 by A1,FDIFF_1:24;
then consider N3 be Neighbourhood of x0 such that
A4: f1.:N3 c= N2 by FCONT_1:5;
consider N1 be Neighbourhood of x0 such that
A5: N1 c= dom f1 by A1;
consider N be Neighbourhood of x0 such that
A6: N c= N1 and
A7: N c= N3 by RCOMP_1:17;
N c= dom (f2*f1)
proof
let x be object;
assume
A8: x in N;
then reconsider x9 = x as Real;
A9: x in N1 by A6,A8;
then f1.x9 in f1.:N3 by A5,A7,A8,FUNCT_1:def 6;
then f1.x9 in N2 by A4;
hence thesis by A5,A3,A9,FUNCT_1:11;
end;
hence thesis by A1,A2,Lm2;
end;
theorem Th14:
f2.x0 <> 0 & f1 is_differentiable_in x0 & f2
is_differentiable_in x0 implies f1/f2 is_differentiable_in x0 & diff(f1/f2,x0)
= (diff(f1,x0) * f2.x0 - diff(f2,x0) * f1.x0)/(f2.x0)^2
proof
assume that
A1: f2.x0 <> 0 and
A2: f1 is_differentiable_in x0 and
A3: f2 is_differentiable_in x0;
consider N1 be Neighbourhood of x0 such that
A4: N1 c= dom f1 by A2;
consider N3 be Neighbourhood of x0 such that
A5: N3 c= dom f2 and
A6: for g st g in N3 holds f2.g <> 0 by A1,A3,FCONT_3:7,FDIFF_1:24;
consider N be Neighbourhood of x0 such that
A7: N c= N1 and
A8: N c= N3 by RCOMP_1:17;
A9: N c= dom f2 \ f2"{0}
proof
let x be object;
assume
A10: x in N;
then reconsider x9 = x as Real;
f2.x9 <> 0 by A6,A8,A10;
then not f2.x9 in {0} by TARSKI:def 1;
then
A11: not x9 in f2"{0} by FUNCT_1:def 7;
x9 in N3 by A8,A10;
hence thesis by A5,A11,XBOOLE_0:def 5;
end;
A12: f2 is_continuous_in x0 by A3,FDIFF_1:24;
N c= dom f1 by A4,A7;
then
A13: N c= dom f1 /\ (dom f2 \ f2"{0}) by A9,XBOOLE_1:19;
A14: for h,c st rng c = {x0} & rng (h + c) c= dom (f1/f2) holds h"(#)((f1/f2
)/*(h+c) - (f1/f2)/*c) is convergent & lim (h"(#)((f1/f2)/*(h+c) - (f1/f2)/*c))
= (diff(f1,x0) * f2.x0 - diff(f2,x0) * f1.x0)/((f2.x0)^2)
proof
dom (f2^) = dom f2 \ f2"{0} by RFUNCT_1:def 2;
then
A15: dom (f2^) c= dom f2 by XBOOLE_1:36;
let h,c;
assume that
A16: rng c = {x0} and
A17: rng (h + c) c= dom (f1/f2);
A18: rng (h + c) c= dom f1 /\ (dom f2 \ f2"{0}) by A17,RFUNCT_1:def 1;
dom f1 /\ (dom f2 \ f2"{0}) c= dom f2 \ f2"{0} by XBOOLE_1:17;
then
A19: rng (h + c) c= dom f2 \ f2"{0} by A18;
then
A20: rng (h + c) c= dom (f2^) by RFUNCT_1:def 2;
then
A21: f2/*(h+c) is non-zero by RFUNCT_2:11;
A22: lim c = x0 by A16,Th4;
set u2 = f2/*c;
set u1 = f1/*c;
set v2 = f2/*(h+c);
set h2 = h" (#)(v2 - u2);
set v1 = f1/*(h+c);
set h1 = h" (#)(v1 - u1);
A23: f1 is_continuous_in x0 by A2,FDIFF_1:24;
A24: rng c c= dom f1 /\ dom (f2^)
proof
let x be object;
assume x in rng c;
then
A25: x = x0 by A16,TARSKI:def 1;
x0 in N by RCOMP_1:16;
then x in dom f1 /\ (dom f2 \ f2"{0}) by A13,A25;
hence thesis by RFUNCT_1:def 2;
end;
A26: dom f1 /\ dom (f2^) c= dom (f2^) by XBOOLE_1:17;
then
A27: f2/*c is non-zero by A24,RFUNCT_2:11,XBOOLE_1:1;
dom f1 /\ (dom f2 \ f2"{0}) c= dom f1 by XBOOLE_1:17;
then
A28: rng (h + c) c= dom f1 by A18;
then
A29: rng (h + c) c= dom f1 /\ dom (f2^) by A20,XBOOLE_1:19;
A30: h"(#) ((f1/f2)/*(h+c) - (f1/f2)/*c)=h"(#)((f1(#) (f2^))/*(h + c) - (
f1/f2)/*c) by RFUNCT_1:31
.= h"(#)((f1(#)(f2^))/*(h + c) - (f1(#)(f2^))/*c) by RFUNCT_1:31
.= h"(#)((f1/*(h+c))(#)((f2^)/*(h + c)) - (f1(#) (f2^))/*c) by A29,
RFUNCT_2:8
.= h"(#)((f1/*(h+c))/"(f2/*(h + c)) - (f1(#)(f2^))/*c) by A20,RFUNCT_2:12
.= h"(#)((f1/*(h+c))/"(f2/*(h + c)) - (f1/*c)(#) ((f2^)/*c)) by A24,
RFUNCT_2:8
.= h" (#) ((f1/*(h+c))/"(f2/*(h + c)) - (f1/*c)/"(f2/*c)) by A24,A26,
RFUNCT_2:12,XBOOLE_1:1
.= h" (#) (((f1/*(h+c))(#)(f2/*c) - (f1/*c) (#) (f2/*(h + c)))/"((f2/*
(h+c))(#) (f2/*c))) by A21,A27,SEQ_1:50
.= (h" (#) ((f1/*(h+c))(#)(f2/*c) - (f1/*c)(#)(f2/*(h + c))))/"((f2/*(
h+c))(#) (f2/*c)) by SEQ_1:41;
rng c c= dom (f2^) by A24,A26;
then
A31: rng c c= dom f2 by A15;
then
A32: f2/*c is convergent by A12,A22,FCONT_1:def 1;
dom f1 /\ dom (f2^) c= dom f1 by XBOOLE_1:17;
then
A33: rng c c= dom f1 by A24;
then
A34: lim(f1/*c) = f1.x0 by A22,A23,FCONT_1:def 1;
dom f2 \ f2"{0} c= dom f2 by XBOOLE_1:36;
then
A35: rng (h + c) c= dom f2 by A19;
diff(f2,x0) = diff(f2,x0);
then
A36: h2 is convergent by A3,A16,A35,Th12;
A37: f1/*c is convergent by A33,A22,A23,FCONT_1:def 1;
then
A38: u1(#)h2 is convergent by A36;
lim h2 = diff(f2,x0) by A3,A16,A35,Th12;
then
A39: lim (u1(#)h2) = diff(f2,x0) * f1.x0 by A36,A37,A34,SEQ_2:15;
set w1 = (f2/*(h+c)) (#) (f2/*c);
A40: lim(h + c) = x0 by A16,Th4;
A41: f2/*(h+c) is convergent by A12,A35,A40,FCONT_1:def 1;
then
A42: w1 is convergent by A32;
f2/*(h+c) is non-zero by A20,RFUNCT_2:11;
then
A43: w1 is non-zero by A27,SEQ_1:35;
A44: lim(f2/*c) = f2.x0 by A12,A31,A22,FCONT_1:def 1;
diff(f1,x0) = diff(f1,x0);
then
A45: h1 is convergent by A2,A16,A28,Th12;
then
A46: h1(#)u2 is convergent by A32;
lim (f2/*(h+c)) = f2.x0 by A12,A35,A40,FCONT_1:def 1;
then
A47: lim w1 = (f2.x0)^2 by A41,A32,A44,SEQ_2:15;
now
let n;
thus (h" (#) (v1(#)u2 - u1(#)v2)).n = (h").n * (v1(#)u2 - u1(#)v2).n by
SEQ_1:8
.= (h").n * ((v1(#)u2).n - (u1(#)v2).n) by RFUNCT_2:1
.= (h").n * (v1.n *u2.n - (u1(#)v2).n) by SEQ_1:8
.= (h").n * ((v1.n - u1.n) *u2.n + (u1.n * u2.n) - u1.n * v2.n) by
SEQ_1:8
.= (h").n * (v1.n - u1.n) *u2.n - u1.n* ((h").n * (v2.n - u2.n))
.= (h").n * (v1 - u1).n * u2.n - u1.n* ((h").n * (v2.n - u2.n)) by
RFUNCT_2:1
.= (h").n * (v1 - u1).n * u2.n - u1.n* ((h").n * (v2 - u2).n) by
RFUNCT_2:1
.= (h" (#) (v1 - u1)).n * u2.n - u1.n* ((h").n * (v2 - u2).n) by
SEQ_1:8
.= (h" (#)(v1 - u1)).n * u2.n - u1.n* (h" (#) (v2 - u2)).n by SEQ_1:8
.= (h" (#)(v1 - u1) (#) u2).n - u1.n* (h" (#) (v2 - u2)).n by SEQ_1:8
.= (h" (#)(v1 - u1) (#) u2).n - (u1 (#) (h" (#) (v2 - u2))).n by
SEQ_1:8
.= (h" (#)(v1 - u1) (#) u2 - u1 (#) (h" (#) (v2 - u2))).n by RFUNCT_2:1
;
end;
then
A48: h" (#) (v1(#)u2 - u1(#)v2) = h"(#)(v1 - u1)(#)u2 - u1(#)(h"(#) (v2 -
u2));
then
A49: h" (#) (v1(#)u2 - u1(#)v2) is convergent by A46,A38;
hence h"(#)((f1/f2)/*(h+c) - (f1/f2)/*c) is convergent by A1,A30,A42,A47
,A43,SEQ_2:23;
lim h1 = diff(f1,x0) by A2,A16,A28,Th12;
then lim (h1(#)u2) = diff(f1,x0) * f2.x0 by A32,A44,A45,SEQ_2:15;
then
lim (h" (#) (v1(#)u2 - u1(#) v2)) = diff(f1,x0) * f2.x0 - diff(f2,x0)
* f1.x0 by A48,A46,A38,A39,SEQ_2:12;
hence thesis by A1,A30,A42,A47,A49,A43,SEQ_2:24;
end;
N c= dom (f1/f2) by A13,RFUNCT_1:def 1;
hence thesis by A14,Th12;
end;
reconsider jj =1 as Element of REAL by NUMBERS:19;
theorem Th15:
f.x0 <> 0 & f is_differentiable_in x0 implies
f^ is_differentiable_in x0 & diff(f^,x0) = - diff(f,x0)/(f.x0)^2
proof
reconsider f1 = dom f --> jj as PartFunc of dom f, REAL by FUNCOP_1:45;
reconsider f1 as PartFunc of REAL, REAL;
assume that
A1: f.x0 <> 0 and
A2: f is_differentiable_in x0;
consider N be Neighbourhood of x0 such that
A3: N c= dom f by A2;
A4: x0 in N by RCOMP_1:16;
A5: dom f1 = dom f by FUNCOP_1:13;
A6: rng f1 = {1}
proof
thus rng f1 c= {1} by FUNCOP_1:13;
let x be object;
A7: x0 in N by RCOMP_1:16;
assume x in {1};
then x = 1 by TARSKI:def 1;
then f1.x0 = x by A3,A7,FUNCOP_1:7;
hence thesis by A5,A3,A7,FUNCT_1:def 3;
end;
then
A8: f1 is_differentiable_on N by A5,A3,FDIFF_1:11;
then
A9: f1 is_differentiable_in x0 by A4,FDIFF_1:9;
0 = (f1`|N).x0 by A5,A3,A6,FDIFF_1:11,RCOMP_1:16
.= diff(f1,x0) by A8,A4,FDIFF_1:def 7;
then
diff(f1/f,x0) = (0 * f.x0 - diff(f,x0) * f1.x0)/((f.x0)^2) by A1,A2,A9,Th14;
then
A10: diff(f1/f,x0) = (- diff(f,x0) * f1.x0)/((f.x0)^2)
.= (- diff(f,x0) * 1)/((f.x0)^2) by A3,A4,FUNCOP_1:7
.= - diff(f,x0)/((f.x0)^2) by XCMPLX_1:187;
A11: dom (f1/f) = dom f1 /\ (dom f \ f"{0}) by RFUNCT_1:def 1
.= dom f \ f"{0} by A5,XBOOLE_1:28,36
.= dom (f^) by RFUNCT_1:def 2;
A12: dom f \ f"{0} c= dom f1 by A5,XBOOLE_1:36;
A13: now
A14: dom f \ f"{0} = dom (f^) by RFUNCT_1:def 2;
let r be Element of REAL such that
A15: r in dom (f1/f);
thus (f1/f).r = f1.r * (f.r)" by A15,RFUNCT_1:def 1
.= 1 * (f.r)" by A5,A12,A11,A15,A14,FUNCOP_1:7
.= (f^).r by A11,A15,RFUNCT_1:def 2;
end;
f1/f is_differentiable_in x0 by A1,A2,A9,Th14;
hence thesis by A10,A11,A13,PARTFUN1:5;
end;
theorem
for A being Subset of REAL holds
f is_differentiable_on A implies
f|A is_differentiable_on A & f`|A = (f|A) `| A
proof
let A be Subset of REAL;
assume
A1: f is_differentiable_on A;
then A c= dom f;
then A c= dom f /\ A by XBOOLE_1:19;
then
A2: A c= dom (f|A) by RELAT_1:61;
now
let x0;
assume x0 in A;
then f|A is_differentiable_in x0 by A1;
hence (f|A)|A is_differentiable_in x0 by RELAT_1:72;
end;
hence
A3: f|A is_differentiable_on A by A2;
then
A4: dom((f|A)`|A) = A by FDIFF_1:def 7;
a5: A is open by A1,FDIFF_1:10;
A5: now
let x0 be Element of REAL;
assume
A6: x0 in A;
then consider N2 being Neighbourhood of x0 such that
A7: N2 c= A by a5,RCOMP_1:18;
A8: f|A is_differentiable_in x0 by A1,A6;
A9: f is_differentiable_in x0 by a5,A1,A6,FDIFF_1:9;
then consider N1 being Neighbourhood of x0 such that
A10: N1 c= dom f and
A11: ex L,R st for r st r in N1 holds f.r - f.x0 = L.(r - x0) + R.(r -
x0);
consider L,R such that
A12: for r st r in N1 holds f.r - f.x0 = L.(r - x0) + R.(r - x0) by A11;
consider N being Neighbourhood of x0 such that
A13: N c= N1 and
A14: N c= N2 by RCOMP_1:17;
A15: N c= A by A7,A14;
then
A16: N c= dom (f|A) by A2;
A17: now
let r be Real;
assume
A18: r in N;
then
A19: r in A by A15;
thus (f|A).r - (f|A).x0 = (f|A).r - f.x0 by A2,A6,FUNCT_1:47
.= f.r - f.x0 by A2,A19,FUNCT_1:47
.= L.(r-x0) + R.(r-x0) by A12,A13,A18;
end;
thus (f`|A).x0 = diff(f,x0) by A1,A6,FDIFF_1:def 7
.= L.1 by A9,A10,A12,FDIFF_1:def 5
.= diff(f|A,x0) by A8,A16,A17,FDIFF_1:def 5
.= ((f|A)`|A).x0 by A3,A6,FDIFF_1:def 7;
end;
dom (f`|A) = A by A1,FDIFF_1:def 7;
hence thesis by A4,A5,PARTFUN1:5;
end;
theorem
f1 is_differentiable_on A & f2 is_differentiable_on A implies
f1 + f2 is_differentiable_on A & (f1 + f2)`|A = f1`|A + f2`|A
proof
assume that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A;
A3: A c= dom f2 by A2;
A c= dom f1 by A1;
then A c= dom f1 /\ dom f2 by A3,XBOOLE_1:19;
then
A4: A c= dom (f1 + f2) by VALUED_1:def 1;
then f1 + f2 is_differentiable_on A by A1,A2,FDIFF_1:18;
then
A5: dom ((f1 + f2)`|A) = A by FDIFF_1:def 7;
A6: dom (f2`|A) = A by A2,FDIFF_1:def 7;
dom (f1`|A) = A by A1,FDIFF_1:def 7;
then dom (f1`|A) /\ dom (f2`|A) = A by A6;
then
A7: dom ((f1`|A) + (f2`|A)) = A by VALUED_1:def 1;
now
let x0 be Element of REAL;
assume
A8: x0 in A;
hence ((f1 + f2)`|A).x0 = diff(f1,x0) + diff(f2,x0) by A1,A2,A4,FDIFF_1:18
.= (f1`|A).x0 + diff(f2,x0) by A1,A8,FDIFF_1:def 7
.= (f1`|A).x0 + (f2`|A).x0 by A2,A8,FDIFF_1:def 7
.= ((f1`|A) + (f2`|A)).x0 by A7,A8,VALUED_1:def 1;
end;
hence thesis by A1,A2,A4,A5,A7,FDIFF_1:18,PARTFUN1:5;
end;
theorem
f1 is_differentiable_on A & f2 is_differentiable_on A implies
f1 - f2 is_differentiable_on A & (f1 - f2)`|A = f1`|A - f2`|A
proof
assume that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A;
A3: A c= dom f2 by A2;
A c= dom f1 by A1;
then A c= dom f1 /\ dom f2 by A3,XBOOLE_1:19;
then
A4: A c= dom (f1 - f2) by VALUED_1:12;
then f1 - f2 is_differentiable_on A by A1,A2,FDIFF_1:19;
then
A5: dom ((f1 - f2)`|A) = A by FDIFF_1:def 7;
A6: dom (f2`|A) = A by A2,FDIFF_1:def 7;
dom (f1`|A) = A by A1,FDIFF_1:def 7;
then dom (f1`|A) /\ dom (f2`|A) = A by A6;
then
A7: dom ((f1`|A) - (f2`|A)) = A by VALUED_1:12;
now
let x0 be Element of REAL;
assume
A8: x0 in A;
hence ((f1 - f2)`|A).x0 = diff(f1,x0) - diff(f2,x0) by A1,A2,A4,FDIFF_1:19
.= (f1`|A).x0 - diff(f2,x0) by A1,A8,FDIFF_1:def 7
.= (f1`|A).x0 - (f2`|A).x0 by A2,A8,FDIFF_1:def 7
.= ((f1`|A) - (f2`|A)).x0 by A7,A8,VALUED_1:13;
end;
hence thesis by A1,A2,A4,A5,A7,FDIFF_1:19,PARTFUN1:5;
end;
theorem
f is_differentiable_on A implies
r(#)f is_differentiable_on A & (r(#)f)`|A = r(#)(f`|A)
proof
assume
A1: f is_differentiable_on A;
then A c= dom f;
then
A2: A c= dom (r(#)f) by VALUED_1:def 5;
then r(#)f is_differentiable_on A by A1,FDIFF_1:20;
then
A3: dom ((r(#)f)`|A) = A by FDIFF_1:def 7;
dom (f`|A) = A by A1,FDIFF_1:def 7;
then
A4: dom (r(#)(f`|A)) = A by VALUED_1:def 5;
now
let x0 be Element of REAL;
assume
A5: x0 in A;
hence ((r(#)f)`|A).x0 = r * diff(f,x0) by A1,A2,FDIFF_1:20
.= r * ((f`|A).x0) by A1,A5,FDIFF_1:def 7
.= (r(#)(f`|A)).x0 by A4,A5,VALUED_1:def 5;
end;
hence thesis by A1,A2,A3,A4,FDIFF_1:20,PARTFUN1:5;
end;
theorem
f1 is_differentiable_on A & f2 is_differentiable_on A implies
f1 (#) f2 is_differentiable_on A & (f1(#)f2)`|A = (f1`|A)(#)f2 + f1(#)(f2`|A)
proof
assume that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A;
A3: A c= dom f1 by A1;
A4: A c= dom f2 by A2;
then A c= dom f1 /\ dom f2 by A3,XBOOLE_1:19;
then
A5: A c= dom (f1(#)f2) by VALUED_1:def 4;
then f1(#)f2 is_differentiable_on A by A1,A2,FDIFF_1:21;
then
A6: dom ((f1(#)f2)`|A) = A by FDIFF_1:def 7;
dom (f2`|A) = A by A2,FDIFF_1:def 7;
then dom f1 /\ dom (f2`|A) = A by A3,XBOOLE_1:28;
then
A7: dom (f1(#)(f2`|A)) = A by VALUED_1:def 4;
dom (f1`|A) = A by A1,FDIFF_1:def 7;
then dom (f1`|A) /\ dom f2 = A by A4,XBOOLE_1:28;
then dom ((f1`|A)(#)f2) = A by VALUED_1:def 4;
then dom ((f1`|A)(#)f2) /\ dom (f1(#)(f2`|A)) = A by A7;
then
A8: dom (((f1`|A)(#)f2) + (f1(#)(f2`|A))) = A by VALUED_1:def 1;
now
let x0 be Element of REAL;
assume
A9: x0 in A;
hence
((f1(#) f2)`|A).x0 = diff(f1,x0)*(f2.x0) + (f1.x0)*diff(f2,x0) by A1,A2,A5,
FDIFF_1:21
.= (f1`|A).x0*f2.x0 + (f1.x0)*diff(f2,x0) by A1,A9,FDIFF_1:def 7
.= (f1`|A).x0*f2.x0 + (f1.x0)*(f2`|A).x0 by A2,A9,FDIFF_1:def 7
.= ((f1`|A)(#)f2).x0 + (f1.x0)*(f2`|A).x0 by VALUED_1:5
.= ((f1`|A)(#)f2).x0 + (f1(#)(f2`|A)).x0 by VALUED_1:5
.= (((f1`|A)(#)f2) + (f1(#)(f2`|A))).x0 by A8,A9,VALUED_1:def 1;
end;
hence thesis by A1,A2,A5,A6,A8,FDIFF_1:21,PARTFUN1:5;
end;
Lm3: (f(#)f)"{0} = f"{0}
proof
thus (f(#)f)"{0} c= f"{0}
proof
let x be object;
assume
A1: x in (f(#)f)"{0};
then reconsider x9 = x as Real;
(f (#) f).x9 in {0} by A1,FUNCT_1:def 7;
then 0 = (f (#) f).x9 by TARSKI:def 1
.= f.x9 * f.x9 by VALUED_1:5;
then f.x9 = 0;
then
A2: f.x9 in {0} by TARSKI:def 1;
x9 in dom (f (#) f) by A1,FUNCT_1:def 7;
then x9 in dom f /\ dom f by VALUED_1:def 4;
hence thesis by A2,FUNCT_1:def 7;
end;
let x be object;
assume
A3: x in f"{0};
then reconsider x9 = x as Real;
f.x9 in {0} by A3,FUNCT_1:def 7;
then 0 = f.x9 by TARSKI:def 1;
then f.x9 * f.x9 = 0;
then (f (#) f).x9 = 0 by VALUED_1:5;
then
A4: (f (#) f).x9 in {0} by TARSKI:def 1;
x9 in dom f /\ dom f by A3,FUNCT_1:def 7;
then x9 in dom (f (#) f) by VALUED_1:def 4;
hence thesis by A4,FUNCT_1:def 7;
end;
theorem
f1 is_differentiable_on A & f2 is_differentiable_on A &
(for x0 st x0 in A holds f2.x0 <> 0) implies
f1/f2 is_differentiable_on A &
(f1/f2)`|A = (f1`|A (#) f2 - f2`|A (#) f1)/(f2 (#) f2)
proof
assume that
A1: f1 is_differentiable_on A and
A2: f2 is_differentiable_on A and
A3: for x0 st x0 in A holds f2.x0 <> 0;
A4: A c= dom f1 by A1;
A5: A c= dom f2 by A2;
A6: A c= dom f2 \ f2"{0}
proof
let x be object;
assume
A7: x in A;
then reconsider x9 = x as Real;
assume not x in dom f2 \ f2"{0};
then not x in dom f2 or x in f2"{0} by XBOOLE_0:def 5;
then f2.x9 in {0} by A5,A7,FUNCT_1:def 7;
then f2.x9 = 0 by TARSKI:def 1;
hence contradiction by A3,A7;
end;
then A c= dom f1 /\ (dom f2 \ f2"{0}) by A4,XBOOLE_1:19;
then
A8: A c= dom (f1/f2) by RFUNCT_1:def 1;
A9: now
let x0;
assume
A10: x0 in A;
hence
A11: f2. x0 <> 0 by A3;
thus
A12: f1 is_differentiable_in x0 by A1,A10,FDIFF_1:9;
thus f2 is_differentiable_in x0 by A2,A10,FDIFF_1:9;
hence f1/f2 is_differentiable_in x0 by A11,A12,Th14;
end;
then for x0 holds x0 in A implies f1/f2 is_differentiable_in x0;
hence
A13: f1/f2 is_differentiable_on A by A8,FDIFF_1:9;
then
A14: A = dom ((f1/f2)`|A) by FDIFF_1:def 7;
A15: now
let x0 be Element of REAL;
assume
A16: x0 in dom ((f1/f2)`|A);
then
A17: f1 is_differentiable_in x0 by A9,A14;
dom (f2`|A) = A by A2,FDIFF_1:def 7;
then x0 in dom (f2`|A) /\ dom f1 by A4,A14,A16,XBOOLE_0:def 4;
then
A18: x0 in dom ((f2`|A)(#)f1) by VALUED_1:def 4;
dom (f1`|A) = A by A1,FDIFF_1:def 7;
then x0 in dom (f1`|A) /\ dom f2 by A5,A14,A16,XBOOLE_0:def 4;
then x0 in dom ((f1`|A)(#)f2) by VALUED_1:def 4;
then x0 in dom ((f1`|A)(#)f2) /\ dom ((f2`|A)(#)f1) by A18,XBOOLE_0:def 4;
then
A19: x0 in dom ((f1`|A)(#)f2 - (f2`|A)(#)f1) by VALUED_1:12;
A20: f2.x0 <> 0 by A9,A14,A16;
then f2.x0 * f2.x0 <> 0;
then (f2 (#) f2).x0 <> 0 by VALUED_1:5;
then not (f2 (#) f2).x0 in {0} by TARSKI:def 1;
then
A21: not x0 in (f2 (#) f2)"{0} by FUNCT_1:def 7;
x0 in dom f2 /\ dom f2 by A5,A14,A16;
then x0 in dom (f2 (#) f2) by VALUED_1:def 4;
then x0 in dom (f2 (#) f2) \ (f2 (#) f2)"{0} by A21,XBOOLE_0:def 5;
then
x0 in dom ((f1`|A)(#)f2 - (f2`|A)(#)f1) /\ (dom (f2 (#) f2) \ (f2 (#)
f2)"{0}) by A19,XBOOLE_0:def 4;
then
A22: x0 in dom (((f1`|A)(#)f2 - (f2`|A)(#)f1)/(f2 (#) f2)) by RFUNCT_1:def 1;
A23: f2 is_differentiable_in x0 by A9,A14,A16;
thus ((f1/f2)`|A).x0 = diff(f1/f2,x0) by A13,A14,A16,FDIFF_1:def 7
.= (diff(f1,x0) * f2.x0 - diff(f2,x0) * f1.x0)/(f2.x0)^2 by A20,A17,A23
,Th14
.= ((f1`|A).x0 * f2.x0 - diff(f2,x0) * f1.x0)/(f2.x0)^2 by A1,A14,A16,
FDIFF_1:def 7
.= ((f1`|A).x0 * f2.x0 - (f2`|A).x0 * f1.x0)/(f2.x0)^2 by A2,A14,A16,
FDIFF_1:def 7
.= (((f1`|A) (#) f2).x0 - (f2`|A).x0 * f1.x0)/(f2.x0)^2 by VALUED_1:5
.= (((f1`|A) (#) f2).x0 - ((f2`|A) (#) f1).x0)/(f2.x0)^2 by VALUED_1:5
.= ((f1`|A) (#) f2 - (f2`|A) (#) f1).x0/(f2.x0 * f2.x0) by A19,
VALUED_1:13
.= ((f1`|A) (#) f2 - (f2`|A) (#) f1).x0/(f2 (#) f2).x0 by VALUED_1:5
.= ((f1`|A) (#) f2 - (f2`|A) (#) f1).x0 * ((f2 (#) f2).x0)" by
XCMPLX_0:def 9
.= (((f1`|A) (#) f2 - (f2`|A) (#) f1)/(f2 (#) f2)).x0 by A22,
RFUNCT_1:def 1;
end;
dom ((f1`|A (#) f2 - f2`|A (#) f1)/(f2 (#) f2)) = dom (f1`|A (#) f2 -
f2`|A (#) f1) /\ (dom (f2 (#) f2) \ (f2 (#) f2)"{0}) by RFUNCT_1:def 1
.= dom (f1`|A (#) f2) /\ dom (f2`|A (#) f1) /\ (dom (f2 (#) f2) \ (f2
(#) f2)"{0}) by VALUED_1:12
.= dom (f1`|A) /\ dom f2 /\ dom (f2`|A (#) f1) /\ (dom (f2 (#) f2) \ (f2
(#) f2)"{0}) by VALUED_1:def 4
.= A /\ dom f2 /\ dom (f2`|A (#) f1) /\ (dom (f2 (#) f2) \ (f2 (#) f2)"{
0}) by A1,FDIFF_1:def 7
.= A /\ dom (f2`|A (#) f1) /\ (dom (f2 (#) f2) \ (f2 (#) f2)"{0}) by A5,
XBOOLE_1:28
.= A /\ (dom (f2`|A) /\ dom f1) /\ (dom (f2 (#) f2) \ (f2 (#) f2)"{0})
by VALUED_1:def 4
.= A /\ (A /\ dom f1) /\ (dom (f2 (#) f2) \ (f2 (#) f2)"{0}) by A2,
FDIFF_1:def 7
.= A /\ A /\ (dom (f2 (#) f2) \ (f2 (#) f2)"{0}) by A4,XBOOLE_1:28
.= A /\ (dom f2 /\ dom f2 \ (f2 (#) f2)"{0}) by VALUED_1:def 4
.= A /\ (dom f2 \ f2"{0}) by Lm3
.= dom ((f1/f2)`|A) by A6,A14,XBOOLE_1:28;
hence thesis by A15,PARTFUN1:5;
end;
theorem
f is_differentiable_on A & (for x0 st x0 in A holds f.x0 <> 0) implies
f^ is_differentiable_on A & (f^)`|A = - (f`|A)/ (f (#) f)
proof
assume that
A1: f is_differentiable_on A and
A2: for x0 st x0 in A holds f.x0 <> 0;
A3: now
let x0;
assume
A4: x0 in A;
hence
A5: f. x0 <> 0 by A2;
thus f is_differentiable_in x0 by A1,A4,FDIFF_1:9;
hence f^ is_differentiable_in x0 by A5,Th15;
end;
then
A6: for x0 holds x0 in A implies f^ is_differentiable_in x0;
A7: A c= dom f by A1;
A8: A c= dom f \ f"{0}
proof
let x be object;
assume
A9: x in A;
then reconsider x9 = x as Real;
assume not x in dom f \ f"{0};
then not x in dom f or x in f"{0} by XBOOLE_0:def 5;
then f.x9 in {0} by A7,A9,FUNCT_1:def 7;
then f.x9 = 0 by TARSKI:def 1;
hence contradiction by A2,A9;
end;
then A c= dom (f^) by RFUNCT_1:def 2;
hence
A10: f^ is_differentiable_on A by A6,FDIFF_1:9;
then
A11: A = dom ((f^)`|A) by FDIFF_1:def 7;
A12: now
let x0 be Element of REAL;
A13: dom (f`|A) = A by A1,FDIFF_1:def 7;
assume
A14: x0 in dom ((f^)`|A);
then
A15: f is_differentiable_in x0 by A3,A11;
A16: f.x0 <> 0 by A3,A11,A14;
then f.x0 * f.x0 <> 0;
then (f (#) f).x0 <> 0 by VALUED_1:5;
then not (f (#) f).x0 in {0} by TARSKI:def 1;
then
A17: not x0 in (f (#) f)"{0} by FUNCT_1:def 7;
x0 in dom f /\ dom f by A7,A11,A14;
then x0 in dom (f (#) f) by VALUED_1:def 4;
then x0 in dom (f (#) f) \ (f (#) f)"{0} by A17,XBOOLE_0:def 5;
then x0 in dom (f`|A) /\ (dom (f (#) f) \ (f (#) f)"{0}) by A11,A14,A13,
XBOOLE_0:def 4;
then
A18: x0 in dom ((f`|A)/(f (#) f)) by RFUNCT_1:def 1;
thus ((f^)`|A).x0 = diff(f^,x0) by A10,A11,A14,FDIFF_1:def 7
.= - diff(f,x0)/(f.x0)^2 by A16,A15,Th15
.= - (f`|A).x0/(f.x0 * f.x0) by A1,A11,A14,FDIFF_1:def 7
.= - (f`|A).x0/(f (#) f).x0 by VALUED_1:5
.= - (f`|A).x0 * ((f (#) f).x0)" by XCMPLX_0:def 9
.= - ((f`|A)/(f (#) f)).x0 by A18,RFUNCT_1:def 1
.= (- (f`|A)/(f (#) f)).x0 by VALUED_1:8;
end;
dom (- (f`|A)/(f (#) f)) = dom ((f`|A)/(f (#) f)) by VALUED_1:8
.= dom (f`|A) /\ (dom (f (#) f) \ (f (#) f)"{0}) by RFUNCT_1:def 1
.= A /\ (dom (f (#) f) \ (f (#) f)"{0}) by A1,FDIFF_1:def 7
.= A /\ (dom f /\ dom f \ (f (#) f)"{0}) by VALUED_1:def 4
.= A /\ (dom f \ f"{0}) by Lm3
.= dom ((f^)`|A) by A8,A11,XBOOLE_1:28;
hence thesis by A12,PARTFUN1:5;
end;
theorem
f1 is_differentiable_on A & (f1.:A) is open Subset of REAL &
f2 is_differentiable_on (f1.:A) implies
f2*f1 is_differentiable_on A & (f2*f1)`|A = ((f2`|(f1.:A))*f1) (#) (f1`|A)
proof
assume that
A1: f1 is_differentiable_on A and
A2: (f1.:A) is open Subset of REAL and
A3: f2 is_differentiable_on (f1.:A);
A4: A c= dom f1 by A1;
A5: now
let x0;
assume
A6: x0 in A;
hence
A7: f1 is_differentiable_in x0 by A1,FDIFF_1:9;
thus x0 in dom f1 by A4,A6;
thus f1.x0 in f1.:A by A4,A6,FUNCT_1:def 6;
hence f2 is_differentiable_in f1.x0 by A2,A3,FDIFF_1:9;
hence f2*f1 is_differentiable_in x0 by A7,Th13;
end;
f1.:A c= dom f2 by A3;
then
A8: A c= dom (f2*f1) by A4,FUNCT_3:3;
for x0 holds x0 in A implies f2*f1 is_differentiable_in x0 by A5;
hence
A9: f2*f1 is_differentiable_on A by A8,FDIFF_1:9;
then
A10: dom ((f2*f1)`|A) = A by FDIFF_1:def 7;
A11: now
let x0 be Element of REAL;
assume
A12: x0 in dom ((f2*f1)`|A);
then
A13: f1 is_differentiable_in x0 by A5,A10;
A14: x0 in dom f1 by A5,A10,A12;
A15: f1.x0 in f1.:A by A5,A10,A12;
A16: f2 is_differentiable_in f1.x0 by A5,A10,A12;
thus ((f2*f1)`|A).x0 = diff(f2*f1,x0) by A9,A10,A12,FDIFF_1:def 7
.= diff(f2,f1.x0) * diff(f1,x0) by A13,A16,Th13
.= diff(f2,f1.x0) * (f1`|A).x0 by A1,A10,A12,FDIFF_1:def 7
.= (f2`|(f1.:A)).(f1.x0) * (f1`|A).x0 by A3,A15,FDIFF_1:def 7
.= ((f2`|(f1.:A))*f1).x0 * (f1`|A).x0 by A14,FUNCT_1:13
.= (((f2`|(f1.:A))*f1) (#) (f1`|A)).x0 by VALUED_1:5;
end;
dom (f2`|(f1.:A)) = f1.:A by A3,FDIFF_1:def 7;
then A c= dom ((f2`|(f1.:A))*f1) by A4,FUNCT_1:101;
then dom ((f2*f1)`|A) = dom ((f2`|(f1.:A))*f1) /\ A by A10,XBOOLE_1:28
.= dom ((f2`|(f1.:A))*f1) /\ dom (f1`|A) by A1,FDIFF_1:def 7
.= dom (((f2`|(f1.:A))*f1) (#) (f1`|A)) by VALUED_1:def 4;
hence thesis by A11,PARTFUN1:5;
end;
theorem Th24:
A c= dom f & (for r,p st r in A & p in A holds |.f.r - f.p.| <= (r - p)^2)
implies f is_differentiable_on A &
for x0 st x0 in A holds diff(f,x0) = 0
proof
assume that
A1: A c= dom f and
A2: for r,p st r in A & p in A holds |.f.r - f.p.| <= (r - p)^2;
A3: now
let x0;
assume x0 in A;
then consider N be Neighbourhood of x0 such that
A4: N c= A by RCOMP_1:18;
A5: N c= dom f by A1,A4;
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)) = 0
proof
set a = seq_const 0;
let h,c;
assume that
A6: rng c = {x0} and
A7: rng (h + c) c= dom f;
A8: lim (h + c) = x0 by A6,Th4;
consider r be Real such that
A9: 0 < r and
A10: N = ].x0 - r, x0 + r.[ by RCOMP_1:def 6;
consider n being Nat such that
A11: for m being Nat st n <= m holds |.(h + c).m - x0.| < r
by A8,A9,SEQ_2:def 7;
set hc = (h + c)^\n;
A12: rng hc c= A
proof
let x be object;
assume x in rng hc;
then consider m such that
A13: x = hc.m by FUNCT_2:113;
x = (h + c).(m+n) by A13,NAT_1:def 3;
then |.hc.m - x0.| < r by A11,A13,NAT_1:12;
then x in N by A10,A13,RCOMP_1:1;
hence thesis by A4;
end;
A14: rng c c= dom f
proof
let x be object;
assume x in rng c;
then
A15: x = x0 by A6,TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence thesis by A5,A15;
end;
set fn = (h"(#)(f/*(h+c) - f/*c))^\n;
set h1 = h^\n;
set c1 = c^\n;
A16: rng c1 c= A
proof
A17: rng c1 c= rng c by VALUED_0:21;
let x be object;
assume x in rng c1;
then
A18: x = x0 by A6,A17,TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence thesis by A4,A18;
end;
A19: abs(h1) is non-zero by SEQ_1:53;
A20: for m being Nat holds a.m <= abs(fn).m & abs(fn).m <= |.h1.|.m
proof
let m be Nat;
A21: m in NAT by ORDINAL1:def 12;
A22: c1.m in rng c1 by VALUED_0:28;
hc.m in rng hc by VALUED_0:28;
then |.f.(hc.m) - f.(c1.m).| <= (hc.m - c1.m)^2 by A2,A12,A16,A22;
then
A23: |.f.(hc.m) - f.(c1.m).| <= |.hc.m - c1.m.|^2 by COMPLEX1:75;
A24: (abs(h1).m)" * |.(f/*(h+c) - (f/*c))^\n.|.m = (abs(h1)").m * abs
((f/*(h+c) - f/*c)^\n).m by VALUED_1:10
.= (abs(h1)" (#) abs((f/*(h+c) - f/*c)^\n)).m by SEQ_1:8
.= (abs(h1") (#) abs((f/*(h+c) - f/*c)^\n)).m by SEQ_1:54
.= |.h1" (#) ((f/*(h+c) - f/*c)^\n).|.m by SEQ_1:52
.= |.(h")^\n (#) ((f/*(h+c) - f/*c)^\n).|.m by SEQM_3:18
.= |.(h"(#)(f/*(h+c) - f/*c))^\n.|.m by SEQM_3:19;
0 <= |. fn.m .| by COMPLEX1:46;
then a.m <= |. fn.m .|;
hence a.m <= abs(fn).m by SEQ_1:12;
A25: |.hc.m - c1.m.|^2 = |.(h1 + c1).m - c1.m.|^2 by SEQM_3:15
.= |.h1.m + c1.m - c1.m.|^2 by SEQ_1:7
.= (abs(h1).m)^2 by SEQ_1:12
.= abs(h1).m * abs(h1).m;
0 <= |.h1.m.| by COMPLEX1:46;
then
A26: 0 <= abs(h1).m by SEQ_1:12;
A27: abs(h1).m <> 0 by A19,SEQ_1:5;
A28: abs(h1).m * abs(h1).m * (abs(h1).m)" = abs(h1).m * (abs(h1).m * (
abs(h1).m)")
.= abs(h1).m * 1 by A27,XCMPLX_0:def 7
.= abs(h1).m;
|.f.(hc.m) - f.(c1.m).| = |.(f/*hc).m - f.(c1.m).| by A1,A12,
FUNCT_2:108,XBOOLE_1:1,A21
.= |.(f/*hc).m - (f/*c1).m.| by A1,A16,FUNCT_2:108,XBOOLE_1:1,A21
.= |.((f/*hc) - (f/*c1)).m.| by RFUNCT_2:1
.= |.(f/*hc) - (f/*c1).|.m by SEQ_1:12
.= |.(f/*(h+c))^\n - (f/*c1).|.m by A7,VALUED_0:27
.= |.(f/*(h+c))^\n - ((f/*c)^\n).|.m by A14,VALUED_0:27
.= |.(f/*(h+c) - (f/*c))^\n.|.m by SEQM_3:17;
hence thesis by A23,A25,A26,A28,A24,XREAL_1:64;
end;
lim h1 = 0;
then
A29: lim abs(h1) = |.0.| by SEQ_4:14
.= 0 by ABSVALUE:2;
A30: lim a = a.0 by SEQ_4:26
.= 0;
then
A31: lim abs(fn) = 0 by A29,A20,SEQ_2:20;
A32: abs(fn) is convergent by A30,A29,A20,SEQ_2:19;
then
A33: fn is convergent by A31,SEQ_4:15;
hence h"(#)(f/*(h+c) - f/*c) is convergent by SEQ_4:21;
lim fn = 0 by A32,A31,SEQ_4:15;
hence thesis by A33,SEQ_4:22;
end;
hence f is_differentiable_in x0 & diff(f,x0) = 0 by A5,Th12;
end;
then for x0 holds x0 in A implies f is_differentiable_in x0;
hence f is_differentiable_on A by A1,FDIFF_1:9;
let x0;
assume x0 in A;
hence thesis by A3;
end;
theorem Th25:
(for r1,r2 st r1 in ].p,g.[ & r2 in ].p,g.[ holds
|.f.r1 - f.r2.| <= (r1 - r2)^2) & ].p,g.[ c= dom f
implies f is_differentiable_on ].p,g.[ & f|].p,g.[ is constant
proof
assume that
A1: for r1,r2 st r1 in ].p,g.[ & r2 in ].p,g.[ holds |.f.r1-f.r2.|<=(r1
-r2)^2 and
A2: ].p,g.[ c= dom f;
thus
A3: f is_differentiable_on ].p,g.[ by A1,A2,Th24;
for x0 st x0 in ].p,g.[ holds diff(f,x0)=0 by A1,A2,Th24;
hence thesis by A3,ROLLE:7;
end;
theorem
left_open_halfline(r) c= dom f &
(for r1,r2 st r1 in left_open_halfline(r) &
r2 in left_open_halfline(r) holds |.f.r1 - f.r2.| <= (r1 - r2)^2)
implies f is_differentiable_on left_open_halfline(r) &
f|left_open_halfline r is constant
proof
assume that
A1: left_open_halfline(r) c= dom f and
A2: for r1,r2 st r1 in left_open_halfline(r) & r2 in left_open_halfline(
r) holds |.f.r1 - f.r2.| <= (r1 - r2)^2;
now
let r1,r2 be Element of REAL;
assume that
A3: r1 in left_open_halfline(r) /\ dom f and
A4: r2 in left_open_halfline(r) /\ dom f;
set rr = min(r1,r2);
A5: ].rr - 1, r.[ c= left_open_halfline(r) by XXREAL_1:263;
then
A6: for g1,g2 st g1 in ].rr - 1, r.[ & g2 in ].rr - 1, r.[ holds |.f.g1
- f.g2.| <= (g1 - g2)^2 by A2;
r2 in left_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: p < r} by XXREAL_1:229;
then
A7: ex g2 st g2 = r2 & g2 < r;
rr - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
then r2 in {g2: rr - 1 < g2 & g2 < r} by A7;
then
A8: r2 in ].rr - 1, r.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A9: r2 in ].rr - 1, r.[ /\ dom f by A8,XBOOLE_0:def 4;
r1 in left_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: g < r} by XXREAL_1:229;
then
A10: ex g1 st g1 = r1 & g1 < r;
rr - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
then r1 in {g1: rr - 1 < g1 & g1 < r} by A10;
then
A11: r1 in ].rr - 1, r.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then
A12: r1 in ].rr - 1, r.[ /\ dom f by A11,XBOOLE_0:def 4;
].rr - 1, r.[ c= dom f by A1,A5;
then f|].rr-1,r.[ is constant by A6,Th25;
hence f.r1 = f.r2 by A12,A9,PARTFUN2:58;
end;
hence thesis by A1,A2,Th24,PARTFUN2:58;
end;
theorem
right_open_halfline(r) c= dom f & (for r1,r2 st r1 in
right_open_halfline(r) & r2 in right_open_halfline(r) holds |.f.r1 - f.r2.| <=
(r1 - r2)^2) implies f is_differentiable_on right_open_halfline(r) & f|
right_open_halfline r is constant
proof
assume that
A1: right_open_halfline(r) c= dom f and
A2: for r1,r2 st r1 in right_open_halfline(r) & r2 in
right_open_halfline(r) holds |.f.r1 - f.r2.| <= (r1 - r2)^2;
now
let r1,r2 be Element of REAL;
assume that
A3: r1 in right_open_halfline(r) /\ dom f and
A4: r2 in right_open_halfline(r) /\ dom f;
set rr = max(r1,r2);
A5: ].r, rr + 1.[ c= right_open_halfline(r) by XXREAL_1:247;
then
A6: for g1,g2 st g1 in ].r, rr + 1 .[ & g2 in ].r, rr + 1.[ holds |.f.
g1 - f.g2.| <= (g1 - g2)^2 by A2;
r2 in right_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: r < p} by XXREAL_1:230;
then
A7: ex g2 st g2 = r2 & r < g2;
r2 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
then r2 in {g2: r < g2 & g2 < rr + 1} by A7;
then
A8: r2 in ].r, rr + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A9: r2 in ].r, rr + 1.[ /\ dom f by A8,XBOOLE_0:def 4;
r1 in right_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: r < g} by XXREAL_1:230;
then
A10: ex g1 st g1 = r1 & r < g1;
r1 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
then r1 in {g1: r < g1 & g1 < rr + 1} by A10;
then
A11: r1 in ].r, rr + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then
A12: r1 in ].r, rr + 1.[ /\ dom f by A11,XBOOLE_0:def 4;
].r, rr + 1 .[ c= dom f by A1,A5;
then f|].r,rr+1.[ is constant by A6,Th25;
hence f.r1 = f.r2 by A12,A9,PARTFUN2:58;
end;
hence thesis by A1,A2,Th24,PARTFUN2:58;
end;
theorem
f is total & (for r1,r2 holds |.f.r1 - f.r2.| <= (r1 - r2)^2) implies
f is_differentiable_on [#](REAL) & f|[#]REAL is constant
proof
assume that
A1: f is total and
A2: for r1,r2 holds |.f.r1 - f.r2.| <= (r1 - r2)^2;
A3: dom f = [#] REAL by A1,PARTFUN1:def 2;
A4: now
let r1,r2 be Element of REAL;
assume that
A5: r1 in [#](REAL) /\ dom f and
A6: r2 in [#] (REAL) /\ dom f;
set rx = max(r1,r2);
set rn = min(r1,r2);
A7: r1 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
A8: r2 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
then r2 in {g2: rn - 1 < g2 & g2 < rx + 1} by A8;
then
A9: r2 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r2 in dom f by A6,XBOOLE_0:def 4;
then
A10: r2 in ].rn - 1, rx + 1.[ /\ dom f by A9,XBOOLE_0:def 4;
rn - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
then r1 in {g1: rn - 1 < g1 & g1 < rx + 1} by A7;
then
A11: r1 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r1 in dom f by A5,XBOOLE_0:def 4;
then
A12: r1 in ].rn - 1, rx + 1.[ /\ dom f by A11,XBOOLE_0:def 4;
for g1,g2 holds g1 in ].rn - 1, rx + 1 .[ & g2 in ].rn - 1, rx + 1.[
implies |.f.g1 - f.g2.| <= (g1 - g2)^2 by A2;
then f|].rn-1,rx+1.[ is constant by A3,Th25;
hence f.r1 = f.r2 by A12,A10,PARTFUN2:58;
end;
for r1,r2 holds r1 in [#] REAL & r2 in [#] REAL implies |.f.r1 - f.r2.|
<= (r1 - r2)^2 by A2;
hence thesis by A3,A4,Th24,PARTFUN2:58;
end;
theorem Th29:
left_open_halfline(r) c= dom f & f is_differentiable_on
left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds 0 < diff(f
,x0)) implies f|left_open_halfline r is increasing & f|left_open_halfline(r) is
one-to-one
proof
assume
left_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on left_open_halfline(r) and
A2: for x0 st x0 in left_open_halfline(r) holds 0 < diff(f,x0);
now
let r1,r2;
assume that
A3: r1 in left_open_halfline(r) /\ dom f and
A4: r2 in left_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = min(r1,r2);
A6: rr - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
r2 in left_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: p < r} by XXREAL_1:229;
then ex g2 st g2 = r2 & g2 < r;
then r2 in {g2: rr - 1 < g2 & g2 < r} by A6;
then
A7: r2 in ].rr - 1, r.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].rr - 1, r.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].rr - 1, r.[ by A1,FDIFF_1:26,XXREAL_1:263;
].rr - 1, r.[ c= left_open_halfline(r) by XXREAL_1:263;
then for g1 st g1 in ].rr - 1, r.[ holds 0 < diff(f,g1) by A2;
then
A10: f|].rr-1,r.[ is increasing by A9,ROLLE:9;
A11: rr - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
r1 in left_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: g < r} by XXREAL_1:229;
then ex g1 st g1 = r1 & g1 < r;
then r1 in {g1: rr - 1 < g1 & g1 < r} by A11;
then
A12: r1 in ].rr - 1, r.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].rr - 1, r.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r1 < f.r2 by A5,A10,A8,RFUNCT_2:20;
end;
hence f|left_open_halfline r is increasing by RFUNCT_2:20;
hence thesis by FCONT_3:8;
end;
theorem Th30:
left_open_halfline(r) c= dom f & f is_differentiable_on
left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds diff(f,x0)
< 0) implies f|left_open_halfline r is decreasing & f|left_open_halfline(r) is
one-to-one
proof
assume
left_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on left_open_halfline(r) and
A2: for x0 st x0 in left_open_halfline(r) holds diff(f,x0) < 0;
now
let r1,r2;
assume that
A3: r1 in left_open_halfline(r) /\ dom f and
A4: r2 in left_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = min(r1,r2);
A6: rr - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
r2 in left_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: p < r} by XXREAL_1:229;
then ex g2 st g2 = r2 & g2 < r;
then r2 in {g2: rr - 1 < g2 & g2 < r} by A6;
then
A7: r2 in ].rr - 1, r.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].rr - 1, r.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].rr - 1, r.[ by A1,FDIFF_1:26,XXREAL_1:263;
].rr - 1, r.[ c= left_open_halfline(r) by XXREAL_1:263;
then for g1 st g1 in ].rr - 1, r.[ holds diff(f,g1) < 0 by A2;
then
A10: f|].rr-1,r.[ is decreasing by A9,ROLLE:10;
A11: rr - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
r1 in left_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: g < r} by XXREAL_1:229;
then ex g1 st g1 = r1 & g1 < r;
then r1 in {g1: rr - 1 < g1 & g1 < r} by A11;
then
A12: r1 in ].rr - 1, r.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].rr - 1, r.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r2 < f.r1 by A5,A10,A8,RFUNCT_2:21;
end;
hence f|left_open_halfline r is decreasing by RFUNCT_2:21;
hence thesis by FCONT_3:8;
end;
theorem
left_open_halfline(r) c= dom f & f is_differentiable_on
left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds 0 <= diff(
f,x0)) implies f|left_open_halfline r is non-decreasing
proof
assume
left_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on left_open_halfline(r) and
A2: for x0 st x0 in left_open_halfline(r) holds 0 <= diff(f,x0);
now
let r1,r2;
assume that
A3: r1 in left_open_halfline(r) /\ dom f and
A4: r2 in left_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = min(r1,r2);
A6: rr - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
r2 in left_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: p < r} by XXREAL_1:229;
then ex g2 st g2 = r2 & g2 < r;
then r2 in {g2: rr - 1 < g2 & g2 < r} by A6;
then
A7: r2 in ].rr - 1, r.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].rr - 1, r.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].rr - 1, r.[ by A1,FDIFF_1:26,XXREAL_1:263;
].rr - 1, r.[ c= left_open_halfline(r) by XXREAL_1:263;
then for g1 st g1 in ].rr - 1, r.[ holds 0 <= diff(f,g1) by A2;
then
A10: f|].rr-1,r.[ is non-decreasing by A9,ROLLE:11;
A11: rr - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
r1 in left_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: g < r} by XXREAL_1:229;
then ex g1 st g1 = r1 & g1 < r;
then r1 in {g1: rr - 1 < g1 & g1 < r} by A11;
then
A12: r1 in ].rr - 1, r.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].rr - 1, r.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r1 <= f.r2 by A5,A10,A8,RFUNCT_2:22;
end;
hence thesis by RFUNCT_2:22;
end;
theorem
left_open_halfline(r) c= dom f & f is_differentiable_on
left_open_halfline(r) & (for x0 st x0 in left_open_halfline(r) holds diff(f,x0)
<= 0) implies f|left_open_halfline r is non-increasing
proof
assume
left_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on left_open_halfline(r) and
A2: for x0 st x0 in left_open_halfline(r) holds diff(f,x0) <= 0;
now
let r1,r2;
assume that
A3: r1 in left_open_halfline(r) /\ dom f and
A4: r2 in left_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = min(r1,r2);
A6: rr - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
r2 in left_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: p < r} by XXREAL_1:229;
then ex g2 st g2 = r2 & g2 < r;
then r2 in {g2: rr - 1 < g2 & g2 < r} by A6;
then
A7: r2 in ].rr - 1, r.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].rr - 1, r.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].rr - 1, r.[ by A1,FDIFF_1:26,XXREAL_1:263;
].rr - 1, r.[ c= left_open_halfline(r) by XXREAL_1:263;
then for g1 st g1 in ].rr - 1, r.[ holds diff(f,g1) <= 0 by A2;
then
A10: f|].rr-1,r.[ is non-increasing by A9,ROLLE:12;
A11: rr - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
r1 in left_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: g < r} by XXREAL_1:229;
then ex g1 st g1 = r1 & g1 < r;
then r1 in {g1: rr - 1 < g1 & g1 < r} by A11;
then
A12: r1 in ].rr - 1, r.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].rr - 1, r.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r2 <= f.r1 by A5,A10,A8,RFUNCT_2:23;
end;
hence thesis by RFUNCT_2:23;
end;
theorem Th33:
right_open_halfline(r) c= dom f & f is_differentiable_on
right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds 0 < diff
(f,x0)) implies f|right_open_halfline r is increasing & f|right_open_halfline(r
) is one-to-one
proof
assume
right_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on right_open_halfline(r) and
A2: for x0 st x0 in right_open_halfline(r) holds 0 < diff(f,x0);
now
let r1,r2;
assume that
A3: r1 in right_open_halfline(r) /\ dom f and
A4: r2 in right_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = max(r1,r2);
A6: r2 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r2 in right_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: r < p} by XXREAL_1:230;
then ex g2 st g2 = r2 & r < g2;
then r2 in {g2: r < g2 & g2 < rr + 1} by A6;
then
A7: r2 in ].r, rr + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].r, rr + 1.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].r, rr + 1.[ by A1,FDIFF_1:26,XXREAL_1:247;
].r, rr + 1.[ c= right_open_halfline(r) by XXREAL_1:247;
then for g1 st g1 in ].r, rr + 1.[ holds 0 < diff(f,g1) by A2;
then
A10: f|].r,rr+1.[ is increasing by A9,ROLLE:9;
A11: r1 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r1 in right_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: r < g} by XXREAL_1:230;
then ex g1 st g1 = r1 & r < g1;
then r1 in {g1: r < g1 & g1 < rr + 1} by A11;
then
A12: r1 in ].r, rr + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].r, rr + 1.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r1 < f.r2 by A5,A10,A8,RFUNCT_2:20;
end;
hence f|right_open_halfline r is increasing by RFUNCT_2:20;
hence thesis by FCONT_3:8;
end;
theorem Th34:
right_open_halfline(r) c= dom f & f is_differentiable_on
right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds diff(f,
x0) < 0) implies f|right_open_halfline r is decreasing & f|right_open_halfline(
r) is one-to-one
proof
assume
right_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on right_open_halfline(r) and
A2: for x0 st x0 in right_open_halfline(r) holds diff(f,x0) < 0;
now
let r1,r2;
assume that
A3: r1 in right_open_halfline(r) /\ dom f and
A4: r2 in right_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = max(r1,r2);
A6: r2 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r2 in right_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: r < p} by XXREAL_1:230;
then ex g2 st g2 = r2 & r < g2;
then r2 in {g2: r < g2 & g2 < rr + 1} by A6;
then
A7: r2 in ].r, rr + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].r, rr + 1.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].r, rr + 1.[ by A1,FDIFF_1:26,XXREAL_1:247;
].r, rr + 1.[ c= right_open_halfline(r) by XXREAL_1:247;
then for g1 st g1 in ].r, rr + 1.[ holds diff(f,g1) < 0 by A2;
then
A10: f|].r,rr+1.[ is decreasing by A9,ROLLE:10;
A11: r1 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r1 in right_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: r < g} by XXREAL_1:230;
then ex g1 st g1 = r1 & r < g1;
then r1 in {g1: r < g1 & g1 < rr + 1} by A11;
then
A12: r1 in ].r, rr + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].r, rr + 1.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r2 < f.r1 by A5,A10,A8,RFUNCT_2:21;
end;
hence f|right_open_halfline r is decreasing by RFUNCT_2:21;
hence thesis by FCONT_3:8;
end;
theorem
right_open_halfline(r) c= dom f & f is_differentiable_on
right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds 0 <=
diff(f,x0)) implies f|right_open_halfline r is non-decreasing
proof
assume
right_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on right_open_halfline(r) and
A2: for x0 st x0 in right_open_halfline(r) holds 0 <= diff(f,x0);
now
let r1,r2;
assume that
A3: r1 in right_open_halfline(r) /\ dom f and
A4: r2 in right_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = max(r1,r2);
A6: r2 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r2 in right_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: r < p} by XXREAL_1:230;
then ex g2 st g2 = r2 & r < g2;
then r2 in {g2: r < g2 & g2 < rr + 1} by A6;
then
A7: r2 in ].r, rr + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].r, rr + 1.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].r, rr + 1.[ by A1,FDIFF_1:26,XXREAL_1:247;
].r, rr + 1.[ c= right_open_halfline(r) by XXREAL_1:247;
then for g1 st g1 in ].r, rr + 1.[ holds 0 <= diff(f,g1) by A2;
then
A10: f|].r,rr+1.[ is non-decreasing by A9,ROLLE:11;
A11: r1 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r1 in right_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: r < g} by XXREAL_1:230;
then ex g1 st g1 = r1 & r < g1;
then r1 in {g1: r < g1 & g1 < rr + 1} by A11;
then
A12: r1 in ].r, rr + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].r, rr + 1.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r1 <= f.r2 by A5,A10,A8,RFUNCT_2:22;
end;
hence thesis by RFUNCT_2:22;
end;
theorem
right_open_halfline(r) c= dom f & f is_differentiable_on
right_open_halfline(r) & (for x0 st x0 in right_open_halfline(r) holds diff(f,
x0) <= 0) implies f|right_open_halfline r is non-increasing
proof
assume
right_open_halfline(r) c= dom f;
assume that
A1: f is_differentiable_on right_open_halfline(r) and
A2: for x0 st x0 in right_open_halfline(r) holds diff(f,x0) <= 0;
now
let r1,r2;
assume that
A3: r1 in right_open_halfline(r) /\ dom f and
A4: r2 in right_open_halfline(r) /\ dom f and
A5: r1 < r2;
set rr = max(r1,r2);
A6: r2 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r2 in right_open_halfline(r) by A4,XBOOLE_0:def 4;
then r2 in {p: r < p} by XXREAL_1:230;
then ex g2 st g2 = r2 & r < g2;
then r2 in {g2: r < g2 & g2 < rr + 1} by A6;
then
A7: r2 in ].r, rr + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].r, rr + 1.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: f is_differentiable_on ].r, rr + 1.[ by A1,FDIFF_1:26,XXREAL_1:247;
].r, rr + 1.[ c= right_open_halfline(r) by XXREAL_1:247;
then for g1 st g1 in ].r, rr + 1.[ holds diff(f,g1) <= 0 by A2;
then
A10: f|].r,rr+1.[ is non-increasing by A9,ROLLE:12;
A11: r1 + 0 < rr + 1 by XREAL_1:8,XXREAL_0:25;
r1 in right_open_halfline(r) by A3,XBOOLE_0:def 4;
then r1 in {g: r < g} by XXREAL_1:230;
then ex g1 st g1 = r1 & r < g1;
then r1 in {g1: r < g1 & g1 < rr + 1} by A11;
then
A12: r1 in ].r, rr + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].r, rr + 1.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r2 <= f.r1 by A5,A10,A8,RFUNCT_2:23;
end;
hence thesis by RFUNCT_2:23;
end;
theorem Th37:
[#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0
holds 0 < diff(f,x0)) implies f|[#]REAL is increasing & f is one-to-one
proof
assume
[#](REAL) c= dom f;
assume that
A1: f is_differentiable_on [#](REAL) and
A2: for x0 holds 0 < diff(f,x0);
A3: now
let r1,r2;
assume that
A4: r1 in [#](REAL) /\ dom f and
A5: r2 in [#](REAL) /\ dom f and
A6: r1 < r2;
set rx = max(r1,r2);
set rn = min(r1,r2);
A7: r2 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
then r2 in {g2: rn - 1 < g2 & g2 < rx + 1} by A7;
then
A8: r2 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r2 in dom f by A5,XBOOLE_0:def 4;
then
A9: r2 in ].rn - 1, rx + 1.[ /\ dom f by A8,XBOOLE_0:def 4;
A10: for g1 holds g1 in ].rn - 1, rx + 1 .[ implies 0 < diff(f,g1) by A2;
f is_differentiable_on ].rn - 1, rx + 1.[ by A1,FDIFF_1:26;
then
A11: f|].rn-1,rx+1.[ is increasing by A10,ROLLE:9;
A12: r1 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
then r1 in {g1: rn - 1 < g1 & g1 < rx + 1} by A12;
then
A13: r1 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r1 in dom f by A4,XBOOLE_0:def 4;
then r1 in ].rn - 1, rx + 1.[ /\ dom f by A13,XBOOLE_0:def 4;
hence f.r1 < f.r2 by A6,A11,A9,RFUNCT_2:20;
end;
hence f|[#]REAL is increasing by RFUNCT_2:20;
now
given r1,r2 being Element of REAL such that
A14: r1 in dom f and
A15: r2 in dom f and
A16: f.r1 = f.r2 and
A17: r1 <> r2;
A18: r2 in [#](REAL) /\ dom f by A15,XBOOLE_0:def 4;
A19: r1 in [#](REAL) /\ dom f by A14,XBOOLE_0:def 4;
now
per cases by A17,XXREAL_0:1;
suppose
r1 < r2;
hence contradiction by A3,A16,A19,A18;
end;
suppose
r2 < r1;
hence contradiction by A3,A16,A19,A18;
end;
end;
hence contradiction;
end;
hence thesis by PARTFUN1:8;
end;
theorem Th38:
[#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0
holds diff(f,x0) < 0) implies f|[#]REAL is decreasing & f is one-to-one
proof
assume
[#](REAL) c= dom f;
assume that
A1: f is_differentiable_on [#](REAL) and
A2: for x0 holds diff(f,x0) < 0;
A3: now
let r1,r2;
assume that
A4: r1 in [#](REAL) /\ dom f and
A5: r2 in [#](REAL) /\ dom f and
A6: r1 < r2;
set rx = max(r1,r2);
set rn = min(r1,r2);
A7: r2 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
then r2 in {g2: rn - 1 < g2 & g2 < rx + 1} by A7;
then
A8: r2 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r2 in dom f by A5,XBOOLE_0:def 4;
then
A9: r2 in ].rn - 1, rx + 1.[ /\ dom f by A8,XBOOLE_0:def 4;
A10: for g1 holds g1 in ].rn - 1, rx + 1 .[ implies diff(f,g1) < 0 by A2;
f is_differentiable_on ].rn - 1, rx + 1.[ by A1,FDIFF_1:26;
then
A11: f|].rn-1,rx+1.[ is decreasing by A10,ROLLE:10;
A12: r1 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
then r1 in {g1: rn - 1 < g1 & g1 < rx + 1} by A12;
then
A13: r1 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r1 in dom f by A4,XBOOLE_0:def 4;
then r1 in ].rn - 1, rx + 1.[ /\ dom f by A13,XBOOLE_0:def 4;
hence f.r2 < f.r1 by A6,A11,A9,RFUNCT_2:21;
end;
hence f|[#]REAL is decreasing by RFUNCT_2:21;
now
given r1,r2 being Element of REAL such that
A14: r1 in dom f and
A15: r2 in dom f and
A16: f.r1 = f.r2 and
A17: r1 <> r2;
A18: r2 in [#](REAL) /\ dom f by A15,XBOOLE_0:def 4;
A19: r1 in [#](REAL) /\ dom f by A14,XBOOLE_0:def 4;
now
per cases by A17,XXREAL_0:1;
suppose
r1 < r2;
hence contradiction by A3,A16,A19,A18;
end;
suppose
r2 < r1;
hence contradiction by A3,A16,A19,A18;
end;
end;
hence contradiction;
end;
hence thesis by PARTFUN1:8;
end;
theorem
[#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0 holds
0 <= diff(f,x0)) implies f|[#]REAL is non-decreasing
proof
assume
[#](REAL) c= dom f;
assume that
A1: f is_differentiable_on [#](REAL) and
A2: for x0 holds 0 <= diff(f,x0);
now
let r1,r2;
assume that
A3: r1 in [#](REAL) /\ dom f and
A4: r2 in [#](REAL) /\ dom f and
A5: r1 < r2;
set rx = max(r1,r2);
set rn = min(r1,r2);
A6: r2 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
then r2 in {g2: rn - 1 < g2 & g2 < rx + 1} by A6;
then
A7: r2 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].rn - 1, rx + 1.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: for g1 holds g1 in ].rn - 1, rx + 1 .[ implies 0 <= diff(f,g1) by A2;
f is_differentiable_on ].rn - 1, rx + 1.[ by A1,FDIFF_1:26;
then
A10: f|].rn-1,rx+1.[ is non-decreasing by A9,ROLLE:11;
A11: r1 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
then r1 in {g1: rn - 1 < g1 & g1 < rx + 1} by A11;
then
A12: r1 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].rn - 1, rx + 1.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r1 <= f.r2 by A5,A10,A8,RFUNCT_2:22;
end;
hence thesis by RFUNCT_2:22;
end;
theorem
[#](REAL) c= dom f & f is_differentiable_on [#](REAL) & (for x0 holds
diff(f,x0) <= 0) implies f|[#]REAL is non-increasing
proof
assume
[#](REAL) c= dom f;
assume that
A1: f is_differentiable_on [#](REAL) and
A2: for x0 holds diff(f,x0) <= 0;
now
let r1,r2;
assume that
A3: r1 in [#](REAL) /\ dom f and
A4: r2 in [#](REAL) /\ dom f and
A5: r1 < r2;
set rx = max(r1,r2);
set rn = min(r1,r2);
A6: r2 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r2 - 0 by XREAL_1:15,XXREAL_0:17;
then r2 in {g2: rn - 1 < g2 & g2 < rx + 1} by A6;
then
A7: r2 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r2 in dom f by A4,XBOOLE_0:def 4;
then
A8: r2 in ].rn - 1, rx + 1.[ /\ dom f by A7,XBOOLE_0:def 4;
A9: for g1 holds g1 in ].rn - 1, rx + 1 .[ implies diff(f,g1) <= 0 by A2;
f is_differentiable_on ].rn - 1, rx + 1.[ by A1,FDIFF_1:26;
then
A10: f|].rn-1,rx+1.[ is non-increasing by A9,ROLLE:12;
A11: r1 + 0 < rx + 1 by XREAL_1:8,XXREAL_0:25;
rn - 1 < r1 - 0 by XREAL_1:15,XXREAL_0:17;
then r1 in {g1: rn - 1 < g1 & g1 < rx + 1} by A11;
then
A12: r1 in ].rn - 1, rx + 1.[ by RCOMP_1:def 2;
r1 in dom f by A3,XBOOLE_0:def 4;
then r1 in ].rn - 1, rx + 1.[ /\ dom f by A12,XBOOLE_0:def 4;
hence f.r2 <= f.r1 by A5,A10,A8,RFUNCT_2:23;
end;
hence thesis by RFUNCT_2:23;
end;
theorem Th41:
].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ((for x0 st
x0 in ].p,g.[ holds 0 < diff(f,x0)) or for x0 st x0 in ].p,g.[ holds diff(f,x0)
< 0) implies rng (f|].p,g.[) is open
proof
assume
A1: ].p,g.[ c= dom f;
assume that
A2: f is_differentiable_on ].p,g.[ and
A3: (for x0 st x0 in ].p,g.[ holds 0 < diff(f,x0)) or for x0 st x0 in ].
p,g.[ holds diff(f,x0) < 0;
A4: f|].p,g.[ is continuous by A2,FDIFF_1:25;
now
per cases by A3;
suppose
for x0 st x0 in ].p,g.[ holds 0 < diff(f,x0);
then f|].p,g.[ is increasing by A2,ROLLE:9;
hence thesis by A1,A4,FCONT_3:23;
end;
suppose
for x0 st x0 in ].p,g.[ holds diff(f,x0) < 0;
then f|].p,g.[ is decreasing by A2,ROLLE:10;
hence thesis by A1,A4,FCONT_3:23;
end;
end;
hence thesis;
end;
theorem Th42:
left_open_halfline(p) c= dom f & f is_differentiable_on
left_open_halfline(p) & ((for x0 st x0 in left_open_halfline(p) holds 0 < diff(
f,x0)) or for x0 st x0 in left_open_halfline(p) holds diff(f,x0) < 0) implies
rng (f|left_open_halfline(p)) is open
proof
set L = left_open_halfline(p);
assume
A1: L c= dom f;
assume that
A2: f is_differentiable_on L and
A3: (for x0 st x0 in L holds 0 < diff(f,x0)) or for x0 st x0 in L holds
diff(f,x0) < 0;
A4: f|L is continuous by A2,FDIFF_1:25;
now
per cases by A3;
suppose
for x0 st x0 in left_open_halfline(p) holds 0 < diff(f,x0);
then f|left_open_halfline p is increasing by A2,Th29;
hence thesis by A1,A4,FCONT_3:24;
end;
suppose
for x0 st x0 in left_open_halfline(p) holds diff(f,x0) < 0;
then f|left_open_halfline p is decreasing by A2,Th30;
hence thesis by A1,A4,FCONT_3:24;
end;
end;
hence thesis;
end;
theorem Th43:
right_open_halfline(p) c= dom f& f is_differentiable_on
right_open_halfline(p) & ((for x0 st x0 in right_open_halfline(p) holds 0 <
diff(f,x0)) or for x0 st x0 in right_open_halfline(p) holds diff(f,x0) < 0)
implies rng (f|right_open_halfline(p)) is open
proof
set l = right_open_halfline(p);
assume
A1: l c= dom f;
assume that
A2: f is_differentiable_on l and
A3: (for x0 st x0 in l holds 0 < diff(f,x0)) or for x0 st x0 in l holds
diff(f,x0) < 0;
A4: f|l is continuous by A2,FDIFF_1:25;
now
per cases by A3;
suppose
for x0 st x0 in right_open_halfline(p) holds 0 < diff(f,x0);
then f|right_open_halfline p is increasing by A2,Th33;
hence thesis by A1,A4,FCONT_3:25;
end;
suppose
for x0 st x0 in right_open_halfline(p) holds diff(f,x0) < 0;
then f|right_open_halfline p is decreasing by A2,Th34;
hence thesis by A1,A4,FCONT_3:25;
end;
end;
hence thesis;
end;
theorem Th44:
[#](REAL) c= dom f & f is_differentiable_on [#](REAL) & ((for x0
holds 0 < diff(f,x0)) or for x0 holds diff(f,x0) < 0) implies rng f is open
proof
assume
A1: [#](REAL) c= dom f;
assume that
A2: f is_differentiable_on [#](REAL) and
A3: (for x0 holds 0 < diff(f,x0)) or for x0 holds diff(f,x0) < 0;
A4: f|[#]REAL is continuous by A2,FDIFF_1:25;
now
per cases by A3;
suppose
for x0 holds 0 < diff(f,x0);
then f|[#]REAL is increasing by A2,Th37;
hence thesis by A1,A4,FCONT_3:26;
end;
suppose
for x0 holds diff(f,x0) < 0;
then f|[#]REAL is decreasing by A2,Th38;
hence thesis by A1,A4,FCONT_3:26;
end;
end;
hence thesis;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st [#]REAL c= dom f & f
is_differentiable_on [#](REAL ) & ((for x0 holds 0 < diff(f,x0)) or for x0
holds diff(f,x0) < 0) holds f is one-to-one & f" is_differentiable_on dom (f")
& for x0 st x0 in dom (f") holds diff(f",x0) = 1/diff(f,(f").x0)
proof
let f be one-to-one PartFunc of REAL,REAL;
assume that
[#]REAL c= dom f and
A1: f is_differentiable_on [#](REAL) and
A2: (for x0 holds 0 < diff(f,x0)) or for x0 holds diff(f,x0) < 0;
A3: rng f is open by A1,A2,Th44;
thus f is one-to-one;
A4: dom (f") = rng f by FUNCT_1:33;
A5: rng (f") = dom f by FUNCT_1:33;
A6: for y0 being Element of REAL st y0 in dom (f")
holds f" is_differentiable_in y0 &
diff(f",y0) = 1/diff(f,(f").y0)
proof
let y0 be Element of REAL;
assume
A7: y0 in dom (f");
then consider x0 being Element of REAL such that
A8: x0 in dom f and
A9: y0 = f.x0 by A4,PARTFUN1:3;
A10: for h,c st rng c = {y0} & rng (h + c) c= dom (f") holds h"(#)((f")/*(
h+c) - (f")/*c) is convergent & lim (h"(#)((f")/*(h+c) - (f")/*c)) = 1/diff(f,(
f").y0)
proof
reconsider fy = (f").y0 as Element of REAL by XREAL_0:def 1;
set a = seq_const (f").y0;
let h,c such that
A11: rng c = {y0} and
A12: rng (h + c) c= dom (f");
A13: lim (h + c) = y0 by A11,Th4;
reconsider a as constant Real_Sequence;
defpred P[Element of NAT,Real] means for r1,r2 be Real st
r1=(h + c).$1 & r2 = a.$1 holds r1 = f.(r2 + $2);
A14: for n ex r be Element of REAL st P[n,r]
proof
let n;
(h + c).n in rng (h + c) by VALUED_0:28;
then consider g being Element of REAL such that
g in dom f and
A15: (h + c).n = f.g by A4,A12,PARTFUN1:3;
take r = g - x0;
let r1,r2 be Real;
assume that
A16: r1 = (h + c).n and
A17: r2 = a.n;
a.n = (f").(f.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
hence r1 = f.(r2 + r) by A15,A16,A17;
end;
consider b such that
A18: for n holds P[n,b.n] from FUNCT_2:sch 3(A14);
A19: now
let n;
c.n in rng c by VALUED_0:28;
hence c.n = f.x0 by A9,A11,TARSKI:def 1;
end;
now
given n being Nat such that
A20: b.n = 0;
A21: n in NAT by ORDINAL1:def 12;
A22: (h + c).n = h.n + c.n by SEQ_1:7
.= h.n + f.x0 by A19,A21;
f.(a.n + b.n) = f.((f").(f.x0)) by A9,A20,SEQ_1:57
.= f.x0 by A8,FUNCT_1:34;
then h.n + f.x0 = f.x0 by A18,A22,A21;
hence contradiction by SEQ_1:5;
end;
then
A23: b is non-zero by SEQ_1:5;
A24: [#](REAL) c= dom f by A1;
then dom f = REAL;
then
A25: f is total by PARTFUN1:def 2;
A26: y0 in dom(f"|rng f) by A4,A7,RELAT_1:69;
f|[#]REAL is increasing or f|[#]REAL is decreasing by A1,A2,Th37,Th38;
then f"|rng f is continuous by A25,FCONT_3:22;
then (f")|dom(f") is_continuous_in y0 by A4,A26,FCONT_1:def 2;
then
A27: f" is_continuous_in y0 by RELAT_1:68;
A28: now
let n;
A29: b.n + a.n in [#] REAL;
thus (((f")/*(h+c)) - a).n = ((f")/*(h+c)).n - a.n by RFUNCT_2:1
.= (f").((h + c).n) - a.n by A12,FUNCT_2:108
.= (f").(f.(b.n + a.n)) - a.n by A18
.= b.n + a.n - a.n by A24,A29,FUNCT_1:34
.= b.n;
end;
A30: (f")/*(h+c) is convergent by A12,A13,A27,FCONT_1:def 1;
then ((f")/*(h+c)) - a is convergent;
then
A31: b is convergent by A28,FUNCT_2:63;
A32: lim a = a.0 by SEQ_4:26
.= (f").y0 by SEQ_1:57;
(f").y0 = lim ((f")/*(h+c)) by A12,A13,A27,FCONT_1:def 1;
then lim (((f")/*(h+c)) - a) = (f").y0 - (f").y0 by A30,A32,SEQ_2:12
.= 0;
then
A33: lim b = 0 by A28,FUNCT_2:63;
A34: rng (b + a) c= dom f
by A24;
reconsider b as 0-convergent non-zero Real_Sequence by A23,A31,A33,
FDIFF_1:def 1;
A35: b" is non-zero by SEQ_1:33;
A36: rng a = {(f").y0}
proof
thus rng a c= {(f").y0}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = (f").y0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {(f").y0};
then x = (f").y0 by TARSKI:def 1;
then a.0 = x by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
A37: rng a c= dom f
proof
let x be object;
assume x in rng a;
then x = (f").y0 by A36,TARSKI:def 1;
hence thesis by A5,A7,FUNCT_1:def 3;
end;
now
let n;
c.n in rng c by VALUED_0:28;
then
A38: c.n = y0 by A11,TARSKI:def 1;
thus (f/*a).n = f.(a.n) by A37,FUNCT_2:108
.= f.((f").y0) by SEQ_1:57
.= c.n by A4,A7,A38,FUNCT_1:35;
end;
then
A39: f/*a = c;
now
let n;
(h + c).n = f.(a.n + b.n) by A18;
then h.n + c.n = f.(a.n + b.n) by SEQ_1:7;
hence h.n = f.(b.n + a.n) - (f/*a).n by A39
.= f.((b + a).n) - (f/*a).n by SEQ_1:7
.= (f/*(b+a)).n - (f/*a).n by A34,FUNCT_2:108
.= (f/*(b+a) - f/*a).n by RFUNCT_2:1;
end;
then
A40: h = f/*(b+a) - f/*a;
then f/*(b+a) - f/*a is non-zero;
then
A41: b"(#)(f/*(b+a) - f/*a) is non-zero by A35,SEQ_1:35;
A42: rng c c= dom (f")
by A7,A11,TARSKI:def 1;
now
let n;
A43: a.n + b.n in [#] REAL;
c.n in rng c by VALUED_0:28;
then
A44: c.n = y0 by A11,TARSKI:def 1;
thus (h"(#)((f")/*(h+c) - (f")/*c)).n = (h").n * ((f")/*(h+c) - (f")/*
c).n by SEQ_1:8
.= (h").n * (((f")/*(h+c)).n - ((f")/*c).n) by RFUNCT_2:1
.= (h").n * ((f").((h + c).n) - ((f")/*c).n) by A12,FUNCT_2:108
.= (h").n * ((f").(f.(a.n + b.n)) - ((f")/*c).n) by A18
.= (h").n * (a.n + b.n - ((f")/*c).n) by A24,A43,FUNCT_1:34
.= (h").n * (a.n + b.n - (f").(c.n)) by A42,FUNCT_2:108
.= (h").n * (a.n + b.n - a.n) by A44,SEQ_1:57
.= (h" (#) (b"")).n by SEQ_1:8
.= ((b" (#) (f/*(b+a) - f/*a))").n by A40,SEQ_1:36;
end;
then
A45: h"(#)((f")/*(h+c) - (f")/*c) = (b"(#) (f/*(b+a) - f/*a))";
A46: f is_differentiable_in fy by A1,FDIFF_1:9;
then
A47: lim (b"(#)(f/*(b+a) - f/*a)) = diff(f,(f").y0) by A36,A34,Th12;
diff(f,(f").y0) = diff(f,(f").y0);
then
A48: b"(#)(f/*(b+a) - f/*a) is convergent by A36,A34,A46,Th12;
A49: 0 <> diff(f,(f").y0) by A2;
hence h"(#)((f")/*(h+c) - (f")/*c) is convergent by A45,A41,A48,A47,
SEQ_2:21;
thus lim (h"(#)((f")/*(h+c) - (f")/*c)) = diff(f,(f").y0)" by A45,A41,A48
,A47,A49,SEQ_2:22
.= 1/diff(f,(f").y0) by XCMPLX_1:215;
end;
ex N being Neighbourhood of y0 st N c= dom (f") by A3,A4,A7,RCOMP_1:18;
hence thesis by A10,Th12;
end;
then for y0 holds y0 in dom (f") implies f" is_differentiable_in
y0;
hence f" is_differentiable_on dom (f") by A3,A4,FDIFF_1:9;
let x0;
assume x0 in dom (f");
hence thesis by A6;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st left_open_halfline(p) c=
dom f & f is_differentiable_on left_open_halfline(p) & ((for x0 st x0 in
left_open_halfline(p) holds 0 < diff(f,x0)) or for x0 st x0 in
left_open_halfline(p) holds diff(f,x0) < 0) holds f|left_open_halfline(p) is
one-to-one & (f|left_open_halfline(p))" is_differentiable_on dom ((f|
left_open_halfline(p))") & for x0 st x0 in dom ((f|left_open_halfline(p))")
holds diff((f|left_open_halfline(p))",x0) = 1/diff(f,((f|left_open_halfline(p))
").x0)
proof
let f be one-to-one PartFunc of REAL,REAL;
set l = left_open_halfline(p);
assume that
l c= dom f and
A1: f is_differentiable_on l and
A2: (for x0 st x0 in l holds 0 < diff(f,x0)) or for x0 st x0 in l holds
diff(f,x0) < 0;
A3: rng (f|l) is open by A1,A2,Th42;
set f1 = f|l;
thus f1 is one-to-one;
A4: dom (f1") = rng f1 by FUNCT_1:33;
A5: rng (f1") = dom f1 by FUNCT_1:33;
A6: for y0 being Element of REAL st y0 in dom (f1")
holds f1" is_differentiable_in y0 &
diff(f1",y0) = 1/diff(f,(f1").y0)
proof
let y0 be Element of REAL;
assume
A7: y0 in dom (f1");
then consider x0 being Element of REAL such that
A8: x0 in dom f1 and
A9: y0 = f1.x0 by A4,PARTFUN1:3;
A10: for h,c st rng c = {y0} & rng (h + c) c= dom (f1") holds h"(#)((f1")
/*(h+c) - (f1")/*c) is convergent & lim (h"(#)((f1")/*(h+c) - (f1")/*c)) = 1/
diff(f,(f1").y0)
proof
A11: l c= dom f by A1;
f|l is increasing or f|l is decreasing by A1,A2,Th29,Th30;
then f1"|(f.:l) is continuous by A11,FCONT_3:18;
then
A12: f1"|rng f1 is continuous by RELAT_1:115;
y0 in dom(f1"|rng f1) by A4,A7,RELAT_1:69;
then (f1")|rng f1 is_continuous_in y0 by A12,FCONT_1:def 2;
then
A13: f1" is_continuous_in y0 by A4,RELAT_1:68;
reconsider fy = (f1").y0 as Element of REAL by XREAL_0:def 1;
set a = seq_const (f1").y0;
let h,c such that
A14: rng c = {y0} and
A15: rng (h + c) c= dom (f1");
A16: lim (h + c) = y0 by A14,Th4;
reconsider a as constant Real_Sequence;
defpred P[Element of NAT, Real] means for r1,r2 be Real st
r1=(h + c).$1 & r2 = a.$1 holds r1 = f.(r2 + $2) & r2 + $2 in dom f & r2 + $2
in dom (f|l);
A17: for n ex r be Element of REAL st P[n,r]
proof
let n;
(h + c).n in rng (h + c) by VALUED_0:28;
then consider g being Element of REAL such that
A18: g in dom f1 and
A19: (h + c).n = f1.g by A4,A15,PARTFUN1:3;
take r = g - x0;
let r1,r2 be Real;
assume that
A20: r1 = (h + c).n and
A21: r2 = a.n;
A22: a.n = (f1").(f1.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
hence r1 = f.(r2 + r) by A18,A19,A20,A21,FUNCT_1:47;
g in dom f /\ l by A18,RELAT_1:61;
hence thesis by A18,A22,A21,XBOOLE_0:def 4;
end;
consider b such that
A23: for n holds P[n,b.n] from FUNCT_2:sch 3(A17);
A24: now
let n;
A25: (h + c).n = (h + c).n;
then
A26: a.n + b.n in dom f1 by A23;
thus (((f1")/*(h+c)) - a).n = ((f1")/*(h+c)).n - a.n by RFUNCT_2:1
.= (f1").((h + c).n) - a.n by A15,FUNCT_2:108
.= (f1").(f.(a.n + b.n)) - a.n by A23
.= (f1").(f1.(a.n + b.n)) - a.n by A23,A25,FUNCT_1:47
.= a.n + b.n - a.n by A26,FUNCT_1:34
.= b.n;
end;
A27: (f1")/*(h+c) is convergent by A15,A16,A13,FCONT_1:def 1;
then ((f1")/*(h+c)) - a is convergent;
then
A28: b is convergent by A24,FUNCT_2:63;
A29: lim a = a.0 by SEQ_4:26
.= (f1").y0 by SEQ_1:57;
(f1").y0 = lim ((f1")/*(h+c)) by A15,A16,A13,FCONT_1:def 1;
then lim (((f1")/*(h+c)) - a) = (f1").y0 - (f1").y0 by A27,A29,SEQ_2:12
.= 0;
then
A30: lim b = 0 by A24,FUNCT_2:63;
A31: rng (b + a) c= dom f
proof
let x be object;
assume x in rng (b + a);
then consider n such that
A32: x = (b + a).n by FUNCT_2:113;
A33: (h+c).n = (h+c).n;
x = a.n + b.n by A32,SEQ_1:7;
hence thesis by A23,A33;
end;
(f1").y0 in dom f1 by A5,A7,FUNCT_1:def 3;
then (f1").y0 in dom f /\ l by RELAT_1:61;
then
A34: (f1").y0 in l by XBOOLE_0:def 4;
then
A35: f is_differentiable_in (f1").y0 by A1,FDIFF_1:9;
A36: now
let n;
c.n in rng c by VALUED_0:28;
hence c.n = f1.x0 by A9,A14,TARSKI:def 1;
end;
A37: 0 <> diff(f,(f1").y0) by A2,A34;
now
given n being Nat such that
A38: b.n = 0;
A39: n in NAT by ORDINAL1:def 12;
a.n = (f1").(f1.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
then
A40: f.(a.n + b.n) = f1.x0 by A8,A38,FUNCT_1:47;
(h + c).n = h.n + c.n by SEQ_1:7
.= h.n + f1.x0 by A36,A39;
then h.n + f1.x0 = f1.x0 by A23,A40,A39;
hence contradiction by SEQ_1:5;
end;
then b is non-zero by SEQ_1:5;
then reconsider b as 0-convergent non-zero Real_Sequence by A28,A30,
FDIFF_1:def 1;
A41: b" is non-zero by SEQ_1:33;
A42: rng a = {(f1").y0}
proof
thus rng a c= {(f1").y0}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = (f1").y0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {(f1").y0};
then x = (f1").y0 by TARSKI:def 1;
then a.0 = x by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
A43: rng a c= dom f
proof
let x be object;
assume x in rng a;
then x = (f1").y0 by A42,TARSKI:def 1;
then x = x0 by A8,A9,FUNCT_1:34;
then x in dom f /\ l by A8,RELAT_1:61;
hence thesis by XBOOLE_0:def 4;
end;
now
let n;
A44: (f1").y0 in rng (f1") by A7,FUNCT_1:def 3;
c.n in rng c by VALUED_0:28;
then
A45: c.n = y0 by A14,TARSKI:def 1;
thus (f/*a).n = f.(a.n) by A43,FUNCT_2:108
.= f.((f1").y0) by SEQ_1:57
.= f1.((f1").y0) by A5,A44,FUNCT_1:47
.= c.n by A4,A7,A45,FUNCT_1:35;
end;
then
A46: f/*a = c;
now
let n;
(h + c).n = f.(a.n + b.n) by A23;
then h.n + c.n = f.(a.n + b.n) by SEQ_1:7;
hence h.n = f.(b.n + a.n) - (f/*a).n by A46
.= f.((b + a).n) - (f/*a).n by SEQ_1:7
.= (f/*(b+a)).n - (f/*a).n by A31,FUNCT_2:108
.= (f/*(b+a) - f/*a).n by RFUNCT_2:1;
end;
then
A47: h = f/*(b+a) - f/*a;
then f/*(b+a) - f/*a is non-zero;
then
A48: b"(#)(f/*(b+a) - f/*a) is non-zero by A41,SEQ_1:35;
A49: rng c c= dom (f1")
by A7,A14,TARSKI:def 1;
now
let n;
A50: (h + c).n = (h + c).n;
then
A51: a.n + b.n in dom f1 by A23;
c.n in rng c by VALUED_0:28;
then
A52: c.n = y0 by A14,TARSKI:def 1;
thus (h"(#)((f1")/*(h+c) - (f1")/*c)).n = (h").n * ((f1")/*(h+c) - (f1
")/*c).n by SEQ_1:8
.= (h").n * (((f1")/*(h+c)).n - ((f1")/*c).n) by RFUNCT_2:1
.= (h").n * ((f1").((h + c).n) - ((f1")/*c).n) by A15,FUNCT_2:108
.= (h").n * ((f1").(f.(a.n + b.n)) - ((f1")/*c).n) by A23
.= (h").n * ((f1").(f1.(a.n + b.n)) - ((f1")/*c).n) by A23,A50,
FUNCT_1:47
.= (h").n * (a.n + b.n - ((f1")/*c).n) by A51,FUNCT_1:34
.= (h").n * (a.n + b.n - (f1").(c.n)) by A49,FUNCT_2:108
.= (h").n * (a.n + b.n - a.n) by A52,SEQ_1:57
.= (h" (#) (b"")).n by SEQ_1:8
.= ((b" (#) (f/*(b+a) - f/*a))").n by A47,SEQ_1:36;
end;
then
A53: h"(#)((f1")/*(h+c) - (f1")/*c) = (b"(#) (f/*(b+a) - f/*a))";
diff(f,(f1").y0) = diff(f,(f1"). y0);
then
A54: b"(#)(f/*(b+a) - f/*a) is convergent by A42,A31,A35,Th12;
A55: lim (b"(#)(f/*(b+a) - f/*a)) = diff(f,(f1").y0) by A42,A31,A35,Th12;
hence h"(#) ((f1")/*(h+c) - (f1")/*c) is convergent by A53,A48,A54,A37,
SEQ_2:21;
thus lim (h"(#)((f1")/*(h+c) - (f1")/*c)) = diff(f,(f1").y0)" by A53,A48
,A54,A55,A37,SEQ_2:22
.= 1/diff(f,(f1").y0) by XCMPLX_1:215;
end;
ex N being Neighbourhood of y0 st N c= dom (f1") by A3,A4,A7,RCOMP_1:18;
hence thesis by A10,Th12;
end;
then for y0 holds y0 in dom (f1") implies f1" is_differentiable_in y0;
hence f1" is_differentiable_on dom (f1") by A3,A4,FDIFF_1:9;
let x0;
assume x0 in dom (f1");
hence thesis by A6;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st right_open_halfline(p) c=
dom f & f is_differentiable_on right_open_halfline(p) & ((for x0 st x0 in
right_open_halfline(p) holds 0 < diff(f,x0)) or for x0 st x0 in
right_open_halfline(p) holds diff(f,x0) < 0) holds f|right_open_halfline(p) is
one-to-one & (f|right_open_halfline(p))" is_differentiable_on dom ((f|
right_open_halfline(p))") & for x0 st x0 in dom ((f|right_open_halfline(p))")
holds diff((f|right_open_halfline(p))",x0) = 1/diff(f,((f|right_open_halfline(p
))").x0)
proof
let f be one-to-one PartFunc of REAL,REAL;
set l = right_open_halfline(p);
assume that
l c= dom f and
A1: f is_differentiable_on l and
A2: (for x0 st x0 in l holds 0 < diff(f,x0)) or for x0 st x0 in l holds
diff(f,x0) < 0;
A3: rng (f|l) is open by A1,A2,Th43;
set f1 = f|l;
thus f1 is one-to-one;
A4: dom (f1") = rng f1 by FUNCT_1:33;
A5: rng (f1") = dom f1 by FUNCT_1:33;
A6: for y0 being Element of REAL st y0 in dom (f1")
holds f1" is_differentiable_in y0 &
diff(f1",y0) = 1/diff(f,(f1").y0)
proof
let y0 be Element of REAL;
assume
A7: y0 in dom (f1");
then consider x0 being Element of REAL such that
A8: x0 in dom f1 and
A9: y0 = f1.x0 by A4,PARTFUN1:3;
A10: for h,c st rng c = {y0} & rng (h + c) c= dom (f1") holds h"(#)((f1")
/*(h+c) - (f1")/*c) is convergent & lim (h"(#)((f1")/*(h+c) - (f1")/*c)) = 1/
diff(f,(f1").y0)
proof
A11: l c= dom f by A1;
f|l is increasing or f|l is decreasing by A1,A2,Th33,Th34;
then f1"|(f.:l) is continuous by A11,FCONT_3:19;
then
A12: f1"|rng f1 is continuous by RELAT_1:115;
y0 in dom((f1")|rng f1) by A4,A7,RELAT_1:69;
then (f1")|rng f1 is_continuous_in y0 by A12,FCONT_1:def 2;
then
A13: f1" is_continuous_in y0 by A4,RELAT_1:68;
reconsider fy = (f1").y0 as Element of REAL by XREAL_0:def 1;
set a = seq_const (f1").y0;
let h,c such that
A14: rng c = {y0} and
A15: rng (h + c) c= dom (f1");
A16: lim (h + c) = y0 by A14,Th4;
reconsider a as constant Real_Sequence;
defpred P[Element of NAT, Real] means for r1,r2 be Real st
r1=(h + c).$1 & r2 = a.$1 holds r1 = f.(r2 + $2) & r2 + $2 in dom f & r2 + $2
in dom (f|l);
A17: for n ex r be Element of REAL st P[n,r]
proof
let n;
(h + c).n in rng (h + c) by VALUED_0:28;
then consider g being Element of REAL such that
A18: g in dom f1 and
A19: (h + c).n = f1.g by A4,A15,PARTFUN1:3;
take r = g - x0;
let r1,r2 be Real;
assume that
A20: r1 = (h + c).n and
A21: r2 = a.n;
A22: a.n = (f1").(f1.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
hence r1 = f.(r2 + r) by A18,A19,A20,A21,FUNCT_1:47;
g in dom f /\ l by A18,RELAT_1:61;
hence thesis by A18,A22,A21,XBOOLE_0:def 4;
end;
consider b such that
A23: for n holds P[n,b.n] from FUNCT_2:sch 3(A17);
A24: now
let n;
A25: (h + c).n = (h + c).n;
then
A26: a.n + b.n in dom f1 by A23;
thus (((f1")/*(h+c)) - a).n = ((f1")/*(h+c)).n - a.n by RFUNCT_2:1
.= (f1").((h + c).n) - a.n by A15,FUNCT_2:108
.= (f1").(f.(a.n + b.n)) - a.n by A23
.= (f1").(f1.(a.n + b.n)) - a.n by A23,A25,FUNCT_1:47
.= a.n + b.n - a.n by A26,FUNCT_1:34
.= b.n;
end;
A27: (f1")/*(h+c) is convergent by A15,A16,A13,FCONT_1:def 1;
then ((f1")/*(h+c)) - a is convergent;
then
A28: b is convergent by A24,FUNCT_2:63;
A29: lim a = a.0 by SEQ_4:26
.= (f1").y0 by SEQ_1:57;
(f1").y0 = lim ((f1")/*(h+c)) by A15,A16,A13,FCONT_1:def 1;
then lim (((f1")/*(h+c)) - a) = (f1").y0 - (f1").y0 by A27,A29,SEQ_2:12
.= 0;
then
A30: lim b = 0 by A24,FUNCT_2:63;
A31: rng (b + a) c= dom f
proof
let x be object;
assume x in rng (b + a);
then consider n such that
A32: x = (b + a).n by FUNCT_2:113;
A33: (h+c).n = (h+c).n;
x = a.n + b.n by A32,SEQ_1:7;
hence thesis by A23,A33;
end;
(f1").y0 in dom f1 by A5,A7,FUNCT_1:def 3;
then (f1").y0 in dom f /\ l by RELAT_1:61;
then
A34: (f1").y0 in l by XBOOLE_0:def 4;
then
A35: f is_differentiable_in (f1").y0 by A1,FDIFF_1:9;
A36: now
let n;
c.n in rng c by VALUED_0:28;
hence c.n = f1.x0 by A9,A14,TARSKI:def 1;
end;
A37: 0 <> diff(f,(f1").y0) by A2,A34;
now
given n being Nat such that
A38: b.n = 0;
A39: n in NAT by ORDINAL1:def 12;
a.n = (f1").(f1.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
then
A40: f.(a.n + b.n) = f1.x0 by A8,A38,FUNCT_1:47;
(h + c).n = h.n + c.n by SEQ_1:7
.= h.n + f1.x0 by A36,A39;
then h.n + f1.x0 = f1.x0 by A23,A40,A39;
hence contradiction by SEQ_1:5;
end;
then b is non-zero by SEQ_1:5;
then reconsider b as 0-convergent non-zero Real_Sequence by A28,A30,
FDIFF_1:def 1;
A41: b" is non-zero by SEQ_1:33;
A42: rng a = {(f1").y0}
proof
thus rng a c= {(f1").y0}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = (f1").y0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {(f1").y0};
then x = (f1").y0 by TARSKI:def 1;
then a.0 = x by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
A43: rng a c= dom f
proof
let x be object;
assume x in rng a;
then x = (f1").y0 by A42,TARSKI:def 1;
then x = x0 by A8,A9,FUNCT_1:34;
then x in dom f /\ l by A8,RELAT_1:61;
hence thesis by XBOOLE_0:def 4;
end;
now
let n;
A44: (f1").y0 in rng (f1") by A7,FUNCT_1:def 3;
c.n in rng c by VALUED_0:28;
then
A45: c.n = y0 by A14,TARSKI:def 1;
thus (f/*a).n = f.(a.n) by A43,FUNCT_2:108
.= f.((f1").y0) by SEQ_1:57
.= f1.((f1").y0) by A5,A44,FUNCT_1:47
.= c.n by A4,A7,A45,FUNCT_1:35;
end;
then
A46: f/*a = c;
now
let n;
(h + c).n = f.(a.n + b.n) by A23;
then h.n + c.n = f.(a.n + b.n) by SEQ_1:7;
hence h.n = f.(b.n + a.n) - (f/*a).n by A46
.= f.((b + a).n) - (f/*a).n by SEQ_1:7
.= (f/*(b+a)).n - (f/*a).n by A31,FUNCT_2:108
.= (f/*(b+a) - f/*a).n by RFUNCT_2:1;
end;
then
A47: h = f/*(b+a) - f/*a;
then f/*(b+a) - f/*a is non-zero;
then
A48: b"(#)(f/*(b+a) - f/*a) is non-zero by A41,SEQ_1:35;
A49: rng c c= dom (f1")
by A7,A14,TARSKI:def 1;
now
let n;
A50: (h + c).n = (h + c).n;
then
A51: a.n + b.n in dom f1 by A23;
c.n in rng c by VALUED_0:28;
then
A52: c.n = y0 by A14,TARSKI:def 1;
thus (h"(#)((f1")/*(h+c) - (f1")/*c)).n = (h").n * ((f1")/*(h+c) - (f1
")/*c).n by SEQ_1:8
.= (h").n * (((f1")/*(h+c)).n - ((f1")/*c).n) by RFUNCT_2:1
.= (h").n * ((f1").((h + c).n) - ((f1")/*c).n) by A15,FUNCT_2:108
.= (h").n * ((f1").(f.(a.n + b.n)) - ((f1")/*c).n) by A23
.= (h").n * ((f1").(f1.(a.n + b.n)) - ((f1")/*c).n) by A23,A50,
FUNCT_1:47
.= (h").n * (a.n + b.n - ((f1")/*c).n) by A51,FUNCT_1:34
.= (h").n * (a.n + b.n - (f1").(c.n)) by A49,FUNCT_2:108
.= (h").n * (a.n + b.n - a.n) by A52,SEQ_1:57
.= (h" (#) (b"")).n by SEQ_1:8
.= ((b" (#) (f/*(b+a) - f/*a))").n by A47,SEQ_1:36;
end;
then
A53: h"(#)((f1")/*(h+c) - (f1")/*c) = (b"(#) (f/*(b+a) - f/*a))";
diff(f,(f1").y0) = diff(f,(f1"). y0);
then
A54: b"(#)(f/*(b+a) - f/*a) is convergent by A42,A31,A35,Th12;
A55: lim (b"(#)(f/*(b+a) - f/*a)) = diff(f,(f1").y0) by A42,A31,A35,Th12;
hence h"(#) ((f1")/*(h+c) - (f1")/*c) is convergent by A53,A48,A54,A37,
SEQ_2:21;
thus lim (h"(#)((f1")/*(h+c) - (f1")/*c)) = diff(f,(f1").y0)" by A53,A48
,A54,A55,A37,SEQ_2:22
.= 1/diff(f,(f1").y0) by XCMPLX_1:215;
end;
ex N being Neighbourhood of y0 st N c= dom (f1") by A3,A4,A7,RCOMP_1:18;
hence thesis by A10,Th12;
end;
then for y0 holds y0 in dom (f1") implies f1" is_differentiable_in y0;
hence f1" is_differentiable_on dom (f1") by A3,A4,FDIFF_1:9;
let x0;
assume x0 in dom (f1");
hence thesis by A6;
end;
theorem
for f be one-to-one PartFunc of REAL,REAL st ].p,g.[ c= dom f & f
is_differentiable_on ].p,g.[ & ((for x0 st x0 in ].p,g.[ holds 0 < diff(f,x0))
or for x0 st x0 in ].p,g.[ holds diff(f,x0) < 0) holds f|].p,g.[ is one-to-one
& (f|].p,g.[)" is_differentiable_on dom ((f|].p,g.[)") & for x0 st x0 in dom ((
f|].p,g.[)") holds diff((f|].p,g.[)",x0) = 1/diff(f,((f|].p,g.[)").x0)
proof
let f be one-to-one PartFunc of REAL,REAL;
set l = ].p,g.[;
assume that
l c= dom f and
A1: f is_differentiable_on l and
A2: (for x0 st x0 in l holds 0 < diff(f,x0)) or for x0 st x0 in l holds
diff(f,x0) < 0;
A3: rng (f|l) is open by A1,A2,Th41;
set f1 = f|l;
thus f1 is one-to-one;
A4: dom (f1") = rng f1 by FUNCT_1:33;
A5: rng (f1") = dom f1 by FUNCT_1:33;
A6: for y0 being Element of REAL st y0 in dom (f1")
holds f1" is_differentiable_in y0 &
diff(f1",y0) = 1/diff(f,(f1").y0)
proof
let y0 be Element of REAL;
assume
A7: y0 in dom (f1");
then consider x0 being Element of REAL such that
A8: x0 in dom f1 and
A9: y0 = f1.x0 by A4,PARTFUN1:3;
A10: for h,c st rng c = {y0} & rng (h + c) c= dom (f1") holds h"(#)((f1")
/*(h+c) - (f1")/*c) is convergent & lim (h"(#)((f1")/*(h+c) - (f1")/*c)) = 1/
diff(f,(f1").y0)
proof
A11: f|l is increasing or f|l is decreasing
proof
per cases by A2;
suppose
for x0 st x0 in l holds 0 < diff(f,x0);
hence thesis by A1,ROLLE:9;
end;
suppose
for x0 st x0 in l holds diff(f,x0) < 0;
hence thesis by A1,ROLLE:10;
end;
end;
l c= dom f by A1;
then f1"|(f.:l) is continuous by A11,FCONT_3:17;
then
A12: f1"|rng f1 is continuous by RELAT_1:115;
y0 in dom(f1"|rng f1) by A4,A7,RELAT_1:69;
then (f1")|rng f1 is_continuous_in y0 by A12,FCONT_1:def 2;
then
A13: f1" is_continuous_in y0 by A4,RELAT_1:68;
reconsider fy =(f1").y0 as Element of REAL by XREAL_0:def 1;
set a = seq_const (f1").y0;
let h,c such that
A14: rng c = {y0} and
A15: rng (h + c) c= dom (f1");
A16: lim (h + c) = y0 by A14,Th4;
reconsider a as constant Real_Sequence;
defpred P[Element of NAT,Real] means for r1,r2 be Real st
r1=(h + c).$1 & r2 = a.$1 holds r1 = f.(r2 + $2) & r2 + $2 in dom f & r2 + $2
in dom (f|l);
A17: for n ex r be Element of REAL st P[n,r]
proof
let n;
(h + c).n in rng (h + c) by VALUED_0:28;
then consider g being Element of REAL such that
A18: g in dom f1 and
A19: (h + c).n = f1.g by A4,A15,PARTFUN1:3;
take r = g - x0;
let r1,r2 be Real;
assume that
A20: r1 = (h + c).n and
A21: r2 = a.n;
A22: a.n = (f1").(f1.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
hence r1 = f.(r2 + r) by A18,A19,A20,A21,FUNCT_1:47;
g in dom f /\ l by A18,RELAT_1:61;
hence thesis by A18,A22,A21,XBOOLE_0:def 4;
end;
consider b such that
A23: for n holds P[n,b.n] from FUNCT_2:sch 3(A17);
A24: now
let n;
A25: (h + c).n = (h + c).n;
then
A26: a.n + b.n in dom f1 by A23;
thus (((f1")/*(h+c)) - a).n = ((f1")/*(h+c)).n - a.n by RFUNCT_2:1
.= (f1").((h + c).n) - a.n by A15,FUNCT_2:108
.= (f1").(f.(a.n + b.n)) - a.n by A23
.= (f1").(f1.(a.n + b.n)) - a.n by A23,A25,FUNCT_1:47
.= a.n + b.n - a.n by A26,FUNCT_1:34
.= b.n;
end;
A27: (f1")/*(h+c) is convergent by A15,A16,A13,FCONT_1:def 1;
then ((f1")/*(h+c)) - a is convergent;
then
A28: b is convergent by A24,FUNCT_2:63;
A29: lim a = a.0 by SEQ_4:26
.= (f1").y0 by SEQ_1:57;
(f1").y0 = lim ((f1")/*(h+c)) by A15,A16,A13,FCONT_1:def 1;
then lim (((f1")/*(h+c)) - a) = (f1").y0 - (f1").y0 by A27,A29,SEQ_2:12
.= 0;
then
A30: lim b = 0 by A24,FUNCT_2:63;
A31: rng (b + a) c= dom f
proof
let x be object;
assume x in rng (b + a);
then consider n such that
A32: x = (b + a).n by FUNCT_2:113;
A33: (h+c).n = (h+c).n;
x = a.n + b.n by A32,SEQ_1:7;
hence thesis by A23,A33;
end;
(f1").y0 in dom f1 by A5,A7,FUNCT_1:def 3;
then (f1").y0 in dom f /\ l by RELAT_1:61;
then
A34: (f1").y0 in l by XBOOLE_0:def 4;
then
A35: f is_differentiable_in (f1").y0 by A1,FDIFF_1:9;
A36: now
let n;
c.n in rng c by VALUED_0:28;
hence c.n = f1.x0 by A9,A14,TARSKI:def 1;
end;
A37: 0 <> diff(f,(f1").y0) by A2,A34;
now
given n being Nat such that
A38: b.n = 0;
A39: n in NAT by ORDINAL1:def 12;
a.n = (f1").(f1.x0) by A9,SEQ_1:57
.= x0 by A8,FUNCT_1:34;
then
A40: f.(a.n + b.n) = f1.x0 by A8,A38,FUNCT_1:47;
(h + c).n = h.n + c.n by SEQ_1:7
.= h.n + f1.x0 by A36,A39;
then h.n + f1.x0 = f1.x0 by A23,A40,A39;
hence contradiction by SEQ_1:5;
end;
then
b is non-zero by SEQ_1:5;
then reconsider b as 0-convergent non-zero Real_Sequence by A28,A30,
FDIFF_1:def 1;
A41: b" is non-zero by SEQ_1:33;
A42: rng a = {(f1").y0}
proof
thus rng a c= {(f1").y0}
proof
let x be object;
assume x in rng a;
then ex n st x = a.n by FUNCT_2:113;
then x = (f1").y0 by SEQ_1:57;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {(f1").y0};
then x = (f1").y0 by TARSKI:def 1;
then a.0 = x by SEQ_1:57;
hence thesis by VALUED_0:28;
end;
A43: rng a c= dom f
proof
let x be object;
assume x in rng a;
then x = (f1").y0 by A42,TARSKI:def 1;
then x = x0 by A8,A9,FUNCT_1:34;
then x in dom f /\ l by A8,RELAT_1:61;
hence thesis by XBOOLE_0:def 4;
end;
now
let n;
A44: (f1").y0 in rng (f1") by A7,FUNCT_1:def 3;
c.n in rng c by VALUED_0:28;
then
A45: c.n = y0 by A14,TARSKI:def 1;
thus (f/*a).n = f.(a.n) by A43,FUNCT_2:108
.= f.((f1").y0) by SEQ_1:57
.= f1.((f1").y0) by A5,A44,FUNCT_1:47
.= c.n by A4,A7,A45,FUNCT_1:35;
end;
then
A46: f/*a = c;
now
let n;
(h + c).n = f.(a.n + b.n) by A23;
then h.n + c.n = f.(a.n + b.n) by SEQ_1:7;
hence h.n = f.(b.n + a.n) - (f/*a).n by A46
.= f.((b + a).n) - (f/*a).n by SEQ_1:7
.= (f/*(b+a)).n - (f/*a).n by A31,FUNCT_2:108
.= (f/*(b+a) - f/*a).n by RFUNCT_2:1;
end;
then
A47: h = f/*(b+a) - f/*a;
then f/*(b+a) - f/*a is non-zero;
then
A48: b"(#)(f/*(b+a) - f/*a) is non-zero by A41,SEQ_1:35;
A49: rng c c= dom (f1")
by A7,A14,TARSKI:def 1;
now
let n;
A50: (h + c).n = (h + c).n;
then
A51: a.n + b.n in dom f1 by A23;
c.n in rng c by VALUED_0:28;
then
A52: c.n = y0 by A14,TARSKI:def 1;
thus (h"(#)((f1")/*(h+c) - (f1")/*c)).n = (h").n * ((f1")/*(h+c) - (f1
")/*c).n by SEQ_1:8
.= (h").n * (((f1")/*(h+c)).n - ((f1")/*c).n) by RFUNCT_2:1
.= (h").n * ((f1").((h + c).n) - ((f1")/*c).n) by A15,FUNCT_2:108
.= (h").n * ((f1").(f.(a.n + b.n)) - ((f1")/*c).n) by A23
.= (h").n * ((f1").(f1.(a.n + b.n)) - ((f1")/*c).n) by A23,A50,
FUNCT_1:47
.= (h").n * (a.n + b.n - ((f1")/*c).n) by A51,FUNCT_1:34
.= (h").n * (a.n + b.n - (f1").(c.n)) by A49,FUNCT_2:108
.= (h").n * (a.n + b.n - a.n) by A52,SEQ_1:57
.= (h" (#) (b"")).n by SEQ_1:8
.= ((b" (#) (f/*(b+a) - f/*a))").n by A47,SEQ_1:36;
end;
then
A53: h
"(#)((f1")/*(h+c) - (f1")/*c) = (b"(#) (f/*(b+a) - f/*a))";
diff(f,(f1").y0) = diff(f,(f1"). y0);
then
A54: b"(#)(f/*(b+a) - f/*a) is convergent by A42,A31,A35,Th12;
A55: lim (b"(#)(f/*(b+a) - f/*a)) = diff(f,(f1").y0) by A42,A31,A35,Th12;
hence h"(#) ((f1")/*(h+c) - (f1")/*c) is convergent by A53,A48,A54,A37,
SEQ_2:21;
thus lim (h"(#)((f1")/*(h+c) - (f1")/*c)) = diff(f,(f1").y0)" by A53,A48
,A54,A55,A37,SEQ_2:22
.= 1/diff(f,(f1").y0) by XCMPLX_1:215;
end;
ex N being Neighbourhood of y0 st N c= dom (f1") by A3,A4,A7,RCOMP_1:18;
hence thesis by A10,Th12;
end;
then for y0 being Real holds y0 in dom (f1") implies f1"
is_differentiable_in y0;
hence f1" is_differentiable_on dom (f1") by A3,A4,FDIFF_1:9;
let x0;
assume x0 in dom (f1");
hence thesis by A6;
end;
theorem
f is_differentiable_in x0 implies for h,c st rng c = {x0} & rng (h + c
) c= dom f & rng (-h + c) c= dom f holds (2(#)h)"(#)(f/*(c+h) - f/*(c-h)) is
convergent & lim((2(#)h)"(#)(f/*(c+h) - f/*(c-h))) = diff(f,x0)
proof
assume
A1: f is_differentiable_in x0;
let h,c such that
A2: rng c = {x0} and
A3: rng (h + c) c= dom f and
A4: rng ((-h) + c) c= dom f;
set fm = (-h)"(#)(f/*(-h + c) - f/*c);
lim (-h) = -lim h by SEQ_2:10; then
A5: -h is 0-convergent;
A6: lim fm = diff(f,x0) by A1,A2,A4,Th12,A5;
set fp = h"(#)(f/*(h+c) - f/*c);
A7: diff(f,x0) = diff(f,x0);
then
A8: fm is convergent by A1,A2,A4,Th12,A5;
A9: fp is convergent by A1,A2,A3,A7,Th12;
then
A10: fp + fm is convergent by A8;
A11: now
let n;
thus (f/*(c+h) - f/*(c-h) + (f/*c - f/*c)).n = (f/*(c+h) - f/*(c-h)).n + (
f/*c - f/*c).n by SEQ_1:7
.= (f/*(c+h) - f/*(c-h)).n + ((f/*c).n - (f/*c).n) by RFUNCT_2:1
.= (f/*(c+h) - f/*(c-h)).n;
end;
A12: 2"(#)(fp + fm) = 2"(#)(h"(#)(f/*(c+h) - f/*c) + (-1)(#)h"(#)(f/*(c + -h
) - f/*c)) by SEQ_1:47
.= 2"(#)(h"(#)(f/*(c+h) - f/*c) + (-1)(#)(h"(#) (f/*(c + -h) - f/*c)))
by SEQ_1:18
.= 2"(#)(h"(#)(f/*(c+h) - f/*c) + h"(#)((-1)(#) (f/*(c + -h) - f/*c)))
by SEQ_1:19
.= 2"(#)(h"(#)(f/*(c+h) - f/*c + (-1)(#)(f/*(c + -h) - f/*c))) by SEQ_1:16
.= 2"(#)h"(#)(f/*(c+h) - f/*c + (-1)(#)(f/*(c + -h) - f/*c)) by SEQ_1:18
.= (2(#)h)"(#)(f/*(c+h) - f/*c + (-1)(#)(f/*(c + -h) - f/*c)) by SEQ_1:46
.= (2(#)h)"(#)(f/*(c+h) - (f/*c - -(f/*(c + -h) - f/*c))) by SEQ_1:30
.= (2(#)h)"(#)(f/*(c+h) - (f/*(c + -h) - (f/*c - f/*c))) by SEQ_1:30
.= (2(#)h)"(#)(f/*(c+h) - f/*(c-h) + (f/*c - f/*c)) by SEQ_1:30;
lim fp = diff(f,x0) by A1,A2,A3,Th12;
then lim (fp + fm) = 1*diff(f,x0) + diff(f,x0) by A9,A8,A6,SEQ_2:6
.= 2*diff(f,x0);
then
A13: lim (2"(#)(fp + fm)) = 2"*(2*diff(f,x0)) by A10,SEQ_2:8
.= diff(f,x0);
2" (#) (fp + fm) is convergent by A10;
hence thesis by A13,A12,A11,FUNCT_2:63;
end;