fdiff_2.miz
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 ::
FDIFF_2:1
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 be
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 be
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 be
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 ::
FDIFF_2:2
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 ::
FDIFF_2:3
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 ::
FDIFF_2:4
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 ::
FDIFF_2:5
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 ::
FDIFF_2:6
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 be
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 ::
FDIFF_2:7
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 be
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 be
Nat holds (d
. n)
=
G(n) from
SEQ_1:sch 1;
for n be
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 be
Nat holds (b
. n)
=
F(n) from
SEQ_1:sch 1;
for n be
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 ::
FDIFF_2:8
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 be
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 ::
FDIFF_2:9
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 ::
FDIFF_2:sch1
ExIncSeqofNat { s() ->
Real_Sequence , P[
object] } :
ex q be
increasing
sequence of
NAT st (for n be
Nat holds P[((s()
* q)
. n)]) & for n st (for r st r
= (s()
. n) holds P[r]) holds ex m st n
= (q
. m)
provided
A1: for n holds ex m st n
<= m & P[(s()
. m)];
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 be
Nat holds for x be
Element of
NAT holds 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)] holds 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 be
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 be
Nat st
H[n] holds n
<= M1;
consider X be
Nat such that
A23:
H[X] & for n be
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 be
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 be
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 ::
FDIFF_2:10
(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 be
Element of
REAL holds g
in (
dom L) iff
P[g] and
A10: for g be
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 be
Element of
REAL holds g
in (
dom T) iff
P[g] and
A16: for g be
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 be
Element of
REAL holds g
in (
dom T1) iff
P[g] and
A19: for g be
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 be
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 be
Nat such that
A27: for n be
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)
* (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(.)) 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(.)) 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(.))
- (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() 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(-)) 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(-)
- (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(-))
- (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 ::
FDIFF_2:11
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 be
Nat such that
A8: for n be
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 ::
FDIFF_2:12
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 be
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 holds ex n st k
<= n & ((f1
/* (h
+ c))
. n)
= (f1
. x0);
defpred
P[
object] means $1
= (f1
. x0);
A43: for k holds ex n st k
<= n &
P[((f1
/* (h
+ c))
. n)] by
A42;
consider I1 be
increasing
sequence of
NAT such that
A44: for n be
Nat holds
P[(((f1
/* (h
+ c))
* I1)
. n)] and for n st for r st r
= ((f1
/* (h
+ c))
. n) holds
P[r] holds 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 holds ex n st k
<= n & ((f1
/* (h
+ c))
. n)
<> (f1
. x0);
defpred
P[
object] means $1
<> (f1
. x0);
A60: for k holds ex n st k
<= n &
P[((f1
/* (h
+ c))
. n)] by
A59;
consider I2 be
increasing
sequence of
NAT such that
A61: for n be
Nat holds
P[(((f1
/* (h
+ c))
* I2)
. n)] and
A62: for n st for r st r
= ((f1
/* (h
+ c))
. n) holds
P[r] holds ex m st n
= (I2
. m) from
ExIncSeqofNat(
A60);
now
given n be
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 be
Nat such that
A82: for m be
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 ::
FDIFF_2:13
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 ::
FDIFF_2:14
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 ::
FDIFF_2:15
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,
XBOOLE_1: 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 ::
FDIFF_2:16
f
is_differentiable_on A implies (f
| A)
is_differentiable_on A & (f
`| A)
= ((f
| A)
`| A)
proof
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:
now
let x0 be
Element of
REAL ;
assume
A6: x0
in A;
then
consider N2 be
Neighbourhood of x0 such that
A7: N2
c= A by
RCOMP_1: 18;
A8: (f
| A)
is_differentiable_in x0 by
A1,
A6;
A9: f
is_differentiable_in x0 by
A1,
A6,
FDIFF_1: 9;
then
consider N1 be
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 be
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 ::
FDIFF_2:17
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 ::
FDIFF_2:18
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 ::
FDIFF_2:19
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 ::
FDIFF_2:20
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 ::
FDIFF_2:21
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 ::
FDIFF_2:22
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 ::
FDIFF_2:23
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 ::
FDIFF_2:24
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 be
Nat such that
A11: for m be
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 be
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 ::
FDIFF_2:25
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 ::
FDIFF_2:26
(
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 ::
FDIFF_2:27
(
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 ::
FDIFF_2:28
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 ::
FDIFF_2:29
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 ::
FDIFF_2:30
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 ::
FDIFF_2:31
(
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 ::
FDIFF_2:32
(
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 ::
FDIFF_2:33
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 ::
FDIFF_2:34
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 ::
FDIFF_2:35
(
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 ::
FDIFF_2:36
(
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 ::
FDIFF_2:37
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 be
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 ::
FDIFF_2:38
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 be
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 ::
FDIFF_2:39
(
[#]
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 ::
FDIFF_2:40
(
[#]
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 ::
FDIFF_2:41
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 ::
FDIFF_2:42
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 ::
FDIFF_2:43
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 ::
FDIFF_2:44
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 ::
FDIFF_2:45
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 be
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 be
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 holds 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 be
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 be
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 be
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 ::
FDIFF_2:46
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 be
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 be
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 holds 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 be
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 be
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 be
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 ::
FDIFF_2:47
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 be
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 be
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 holds 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 be
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 be
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 be
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 ::
FDIFF_2:48
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 be
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 be
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 holds 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 be
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 be
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 be
Neighbourhood of y0 st N
c= (
dom (f1
" )) by
A3,
A4,
A7,
RCOMP_1: 18;
hence thesis by
A10,
Th12;
end;
then for y0 be
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 ::
FDIFF_2:49
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;