:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski

::

:: Received January 10, 1991

:: Copyright (c) 1991-2021 Association of Mizar Users

registration

let h be non-zero 0 -convergent Real_Sequence;

coherence

( - h is non-zero & - h is convergent ) by SEQ_1:45;

end;
coherence

( - h is non-zero & - h is convergent ) by SEQ_1:45;

theorem Th1: :: FDIFF_2:1

for a, b, d being Real_Sequence st a is convergent & b is convergent & lim a = lim b & ( for n being Element of NAT holds

( d . (2 * n) = a . n & d . ((2 * n) + 1) = b . n ) ) holds

( d is convergent & lim d = lim a )

( d . (2 * n) = a . n & d . ((2 * n) + 1) = b . n ) ) holds

( d is convergent & lim d = lim a )

proof end;

theorem Th2: :: FDIFF_2:2

for a being Real_Sequence st ( for n being Element of NAT holds a . n = 2 * n ) holds

a is V43() sequence of NAT

a is V43() sequence of NAT

proof end;

theorem Th3: :: FDIFF_2:3

for a being Real_Sequence st ( for n being Element of NAT holds a . n = (2 * n) + 1 ) holds

a is V43() sequence of NAT

a is V43() sequence of NAT

proof end;

theorem Th4: :: FDIFF_2:4

for x0 being Real

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} holds

( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} holds

( c is convergent & lim c = x0 & h + c is convergent & lim (h + c) = x0 )

proof end;

theorem Th6: :: FDIFF_2:6

for a being Real_Sequence

for h being non-zero 0 -convergent Real_Sequence st a is subsequence of h holds

a is non-zero 0 -convergent Real_Sequence

for h being non-zero 0 -convergent Real_Sequence st a is subsequence of h holds

a is non-zero 0 -convergent Real_Sequence

proof end;

theorem Th7: :: FDIFF_2:7

for g being Real

for f being PartFunc of REAL,REAL st ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds

for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence 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)))

for f being PartFunc of REAL,REAL st ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {g} & rng (h + c) c= dom f & {g} c= dom f holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds

for h1, h2 being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence 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 end;

theorem Th8: :: FDIFF_2:8

for r being Real

for f being PartFunc of REAL,REAL st ex N being Neighbourhood of r st N c= dom f holds

ex h being non-zero 0 -convergent Real_Sequence ex c being V8() Real_Sequence st

( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )

for f being PartFunc of REAL,REAL st ex N being Neighbourhood of r st N c= dom f holds

ex h being non-zero 0 -convergent Real_Sequence ex c being V8() Real_Sequence st

( rng c = {r} & rng (h + c) c= dom f & {r} c= dom f )

proof end;

theorem Th9: :: FDIFF_2:9

for a being Real_Sequence

for f1, f2 being PartFunc of REAL,REAL st rng a c= dom (f2 * f1) holds

( rng a c= dom f1 & rng (f1 /* a) c= dom f2 )

for f1, f2 being PartFunc of REAL,REAL st rng a c= dom (f2 * f1) holds

( rng a c= dom f1 & rng (f1 /* a) c= dom f2 )

proof end;

scheme :: FDIFF_2:sch 1

ExIncSeqofNat{ F_{1}() -> Real_Sequence, P_{1}[ object ] } :

ExIncSeqofNat{ F

ex q being V43() sequence of NAT st

( ( for n being Nat holds P_{1}[(F_{1}() * q) . n] ) & ( for n being Element of NAT st ( for r being Real st r = F_{1}() . n holds

P_{1}[r] ) holds

ex m being Element of NAT st n = q . m ) )

provided
( ( for n being Nat holds P

P

ex m being Element of NAT st n = q . m ) )

proof end;

theorem :: FDIFF_2:10

Lm1: for x0 being Real

for f being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) holds

( f is_differentiable_in x0 & ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )

proof end;

theorem Th11: :: FDIFF_2:11

for x0 being Real

for f being PartFunc of REAL,REAL holds

( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )

for f being PartFunc of REAL,REAL holds

( f is_differentiable_in x0 iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) ) )

proof end;

theorem Th12: :: FDIFF_2:12

for x0, g being Real

for f being PartFunc of REAL,REAL holds

( f is_differentiable_in x0 & diff (f,x0) = g iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence 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 ) ) ) )

for f being PartFunc of REAL,REAL holds

( f is_differentiable_in x0 & diff (f,x0) = g iff ( ex N being Neighbourhood of x0 st N c= dom f & ( for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence 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 end;

Lm2: for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st N c= dom (f2 * f1) & f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds

( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )

proof end;

theorem Th13: :: FDIFF_2:13

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds

( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds

( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )

proof end;

theorem Th14: :: FDIFF_2:14

for x0 being Real

for f1, f2 being PartFunc of REAL,REAL st f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 / f2 is_differentiable_in x0 & diff ((f1 / f2),x0) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

for f1, f2 being PartFunc of REAL,REAL st f2 . x0 <> 0 & f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds

( f1 / f2 is_differentiable_in x0 & diff ((f1 / f2),x0) = (((diff (f1,x0)) * (f2 . x0)) - ((diff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof end;

reconsider jj = 1 as Element of REAL by NUMBERS:19;

theorem Th15: :: FDIFF_2:15

for x0 being Real

for f being PartFunc of REAL,REAL st f . x0 <> 0 & f is_differentiable_in x0 holds

( f ^ is_differentiable_in x0 & diff ((f ^),x0) = - ((diff (f,x0)) / ((f . x0) ^2)) )

for f being PartFunc of REAL,REAL st f . x0 <> 0 & f is_differentiable_in x0 holds

( f ^ is_differentiable_in x0 & diff ((f ^),x0) = - ((diff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem :: FDIFF_2:16

for A being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on A holds

( f | A is_differentiable_on A & f `| A = (f | A) `| A )

for f being PartFunc of REAL,REAL st f is_differentiable_on A holds

( f | A is_differentiable_on A & f `| A = (f | A) `| A )

proof end;

theorem :: FDIFF_2:17

for A being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds

( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds

( f1 + f2 is_differentiable_on A & (f1 + f2) `| A = (f1 `| A) + (f2 `| A) )

proof end;

theorem :: FDIFF_2:18

for A being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds

( f1 - f2 is_differentiable_on A & (f1 - f2) `| A = (f1 `| A) - (f2 `| A) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds

( f1 - f2 is_differentiable_on A & (f1 - f2) `| A = (f1 `| A) - (f2 `| A) )

proof end;

theorem :: FDIFF_2:19

for r being Real

for A being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on A holds

( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )

for A being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on A holds

( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )

proof end;

theorem :: FDIFF_2:20

for A being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds

( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A holds

( f1 (#) f2 is_differentiable_on A & (f1 (#) f2) `| A = ((f1 `| A) (#) f2) + (f1 (#) (f2 `| A)) )

proof end;

Lm3: for f being PartFunc of REAL,REAL holds (f (#) f) " {0} = f " {0}

proof end;

theorem :: FDIFF_2:21

for A being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds

f2 . x0 <> 0 ) holds

( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f2 is_differentiable_on A & ( for x0 being Real st x0 in A holds

f2 . x0 <> 0 ) holds

( f1 / f2 is_differentiable_on A & (f1 / f2) `| A = (((f1 `| A) (#) f2) - ((f2 `| A) (#) f1)) / (f2 (#) f2) )

proof end;

theorem :: FDIFF_2:22

for A being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on A & ( for x0 being Real st x0 in A holds

f . x0 <> 0 ) holds

( f ^ is_differentiable_on A & (f ^) `| A = - ((f `| A) / (f (#) f)) )

for f being PartFunc of REAL,REAL st f is_differentiable_on A & ( for x0 being Real st x0 in A holds

f . x0 <> 0 ) holds

( f ^ is_differentiable_on A & (f ^) `| A = - ((f `| A) / (f (#) f)) )

proof end;

theorem :: FDIFF_2:23

for A being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f1 .: A is open Subset of REAL & f2 is_differentiable_on f1 .: A holds

( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & f1 .: A is open Subset of REAL & f2 is_differentiable_on f1 .: A holds

( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| (f1 .: A)) * f1) (#) (f1 `| A) )

proof end;

theorem Th24: :: FDIFF_2:24

for A being open Subset of REAL

for f being PartFunc of REAL,REAL st A c= dom f & ( for r, p being Real st r in A & p in A holds

|.((f . r) - (f . p)).| <= (r - p) ^2 ) holds

( f is_differentiable_on A & ( for x0 being Real st x0 in A holds

diff (f,x0) = 0 ) )

for f being PartFunc of REAL,REAL st A c= dom f & ( for r, p being Real st r in A & p in A holds

|.((f . r) - (f . p)).| <= (r - p) ^2 ) holds

( f is_differentiable_on A & ( for x0 being Real st x0 in A holds

diff (f,x0) = 0 ) )

proof end;

theorem Th25: :: FDIFF_2:25

for g, p being Real

for f being PartFunc of REAL,REAL st ( for r1, r2 being Real st r1 in ].p,g.[ & r2 in ].p,g.[ holds

|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) & ].p,g.[ c= dom f holds

( f is_differentiable_on ].p,g.[ & f | ].p,g.[ is V8() )

for f being PartFunc of REAL,REAL st ( for r1, r2 being Real st r1 in ].p,g.[ & r2 in ].p,g.[ holds

|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) & ].p,g.[ c= dom f holds

( f is_differentiable_on ].p,g.[ & f | ].p,g.[ is V8() )

proof end;

theorem :: FDIFF_2:26

for r being Real

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in left_open_halfline r & r2 in left_open_halfline r holds

|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds

( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is V8() )

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in left_open_halfline r & r2 in left_open_halfline r holds

|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds

( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is V8() )

proof end;

theorem :: FDIFF_2:27

for r being Real

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in right_open_halfline r & r2 in right_open_halfline r holds

|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds

( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is V8() )

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & ( for r1, r2 being Real st r1 in right_open_halfline r & r2 in right_open_halfline r holds

|.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds

( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is V8() )

proof end;

theorem :: FDIFF_2:28

for f being PartFunc of REAL,REAL st f is total & ( for r1, r2 being Real holds |.((f . r1) - (f . r2)).| <= (r1 - r2) ^2 ) holds

( f is_differentiable_on [#] REAL & f | ([#] REAL) is V8() )

( f is_differentiable_on [#] REAL & f | ([#] REAL) is V8() )

proof end;

theorem Th29: :: FDIFF_2:29

for r being Real

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

0 < diff (f,x0) ) holds

( f | (left_open_halfline r) is increasing & f | (left_open_halfline r) is one-to-one )

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

0 < diff (f,x0) ) holds

( f | (left_open_halfline r) is increasing & f | (left_open_halfline r) is one-to-one )

proof end;

theorem Th30: :: FDIFF_2:30

for r being Real

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

diff (f,x0) < 0 ) holds

( f | (left_open_halfline r) is decreasing & f | (left_open_halfline r) is one-to-one )

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

diff (f,x0) < 0 ) holds

( f | (left_open_halfline r) is decreasing & f | (left_open_halfline r) is one-to-one )

proof end;

theorem :: FDIFF_2:31

for r being Real

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

0 <= diff (f,x0) ) holds

f | (left_open_halfline r) is non-decreasing

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

0 <= diff (f,x0) ) holds

f | (left_open_halfline r) is non-decreasing

proof end;

theorem :: FDIFF_2:32

for r being Real

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

diff (f,x0) <= 0 ) holds

f | (left_open_halfline r) is non-increasing

for f being PartFunc of REAL,REAL st left_open_halfline r c= dom f & f is_differentiable_on left_open_halfline r & ( for x0 being Real st x0 in left_open_halfline r holds

diff (f,x0) <= 0 ) holds

f | (left_open_halfline r) is non-increasing

proof end;

theorem Th33: :: FDIFF_2:33

for r being Real

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

0 < diff (f,x0) ) holds

( f | (right_open_halfline r) is increasing & f | (right_open_halfline r) is one-to-one )

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

0 < diff (f,x0) ) holds

( f | (right_open_halfline r) is increasing & f | (right_open_halfline r) is one-to-one )

proof end;

theorem Th34: :: FDIFF_2:34

for r being Real

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

diff (f,x0) < 0 ) holds

( f | (right_open_halfline r) is decreasing & f | (right_open_halfline r) is one-to-one )

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

diff (f,x0) < 0 ) holds

( f | (right_open_halfline r) is decreasing & f | (right_open_halfline r) is one-to-one )

proof end;

theorem :: FDIFF_2:35

for r being Real

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

0 <= diff (f,x0) ) holds

f | (right_open_halfline r) is non-decreasing

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

0 <= diff (f,x0) ) holds

f | (right_open_halfline r) is non-decreasing

proof end;

theorem :: FDIFF_2:36

for r being Real

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

diff (f,x0) <= 0 ) holds

f | (right_open_halfline r) is non-increasing

for f being PartFunc of REAL,REAL st right_open_halfline r c= dom f & f is_differentiable_on right_open_halfline r & ( for x0 being Real st x0 in right_open_halfline r holds

diff (f,x0) <= 0 ) holds

f | (right_open_halfline r) is non-increasing

proof end;

theorem Th37: :: FDIFF_2:37

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff (f,x0) ) holds

( f | ([#] REAL) is increasing & f is one-to-one )

( f | ([#] REAL) is increasing & f is one-to-one )

proof end;

theorem Th38: :: FDIFF_2:38

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds diff (f,x0) < 0 ) holds

( f | ([#] REAL) is decreasing & f is one-to-one )

( f | ([#] REAL) is decreasing & f is one-to-one )

proof end;

theorem :: FDIFF_2:39

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 <= diff (f,x0) ) holds

f | ([#] REAL) is non-decreasing

f | ([#] REAL) is non-decreasing

proof end;

theorem :: FDIFF_2:40

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds diff (f,x0) <= 0 ) holds

f | ([#] REAL) is non-increasing

f | ([#] REAL) is non-increasing

proof end;

theorem Th41: :: FDIFF_2:41

for g, p being Real

for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds

0 < diff (f,x0) or for x0 being Real st x0 in ].p,g.[ holds

diff (f,x0) < 0 ) holds

rng (f | ].p,g.[) is open

for f being PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds

0 < diff (f,x0) or for x0 being Real st x0 in ].p,g.[ holds

diff (f,x0) < 0 ) holds

rng (f | ].p,g.[) is open

proof end;

theorem Th42: :: FDIFF_2:42

for p being Real

for f being PartFunc of REAL,REAL st left_open_halfline p c= dom f & f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds

0 < diff (f,x0) or for x0 being Real st x0 in left_open_halfline p holds

diff (f,x0) < 0 ) holds

rng (f | (left_open_halfline p)) is open

for f being PartFunc of REAL,REAL st left_open_halfline p c= dom f & f is_differentiable_on left_open_halfline p & ( for x0 being Real st x0 in left_open_halfline p holds

0 < diff (f,x0) or for x0 being Real st x0 in left_open_halfline p holds

diff (f,x0) < 0 ) holds

rng (f | (left_open_halfline p)) is open

proof end;

theorem Th43: :: FDIFF_2:43

for p being Real

for f being PartFunc of REAL,REAL st right_open_halfline p c= dom f & f is_differentiable_on right_open_halfline p & ( for x0 being Real st x0 in right_open_halfline p holds

0 < diff (f,x0) or for x0 being Real st x0 in right_open_halfline p holds

diff (f,x0) < 0 ) holds

rng (f | (right_open_halfline p)) is open

for f being PartFunc of REAL,REAL st right_open_halfline p c= dom f & f is_differentiable_on right_open_halfline p & ( for x0 being Real st x0 in right_open_halfline p holds

0 < diff (f,x0) or for x0 being Real st x0 in right_open_halfline p holds

diff (f,x0) < 0 ) holds

rng (f | (right_open_halfline p)) is open

proof end;

theorem Th44: :: FDIFF_2:44

for f being PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff (f,x0) or for x0 being Real holds diff (f,x0) < 0 ) holds

rng f is open

rng f is open

proof end;

theorem :: FDIFF_2:45

for f being one-to-one PartFunc of REAL,REAL st [#] REAL c= dom f & f is_differentiable_on [#] REAL & ( for x0 being Real holds 0 < diff (f,x0) or for x0 being Real holds diff (f,x0) < 0 ) holds

( f is one-to-one & f " is_differentiable_on dom (f ") & ( for x0 being Real st x0 in dom (f ") holds

diff ((f "),x0) = 1 / (diff (f,((f ") . x0))) ) )

( f is one-to-one & f " is_differentiable_on dom (f ") & ( for x0 being Real st x0 in dom (f ") holds

diff ((f "),x0) = 1 / (diff (f,((f ") . x0))) ) )

proof end;

theorem :: FDIFF_2:46

for p being Real

for f being 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 being Real st x0 in left_open_halfline p holds

0 < diff (f,x0) or for x0 being Real 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 being Real 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))) ) )

for f being 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 being Real st x0 in left_open_halfline p holds

0 < diff (f,x0) or for x0 being Real 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 being Real 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 end;

theorem :: FDIFF_2:47

for p being Real

for f being 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 being Real st x0 in right_open_halfline p holds

0 < diff (f,x0) or for x0 being Real 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 being Real 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))) ) )

for f being 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 being Real st x0 in right_open_halfline p holds

0 < diff (f,x0) or for x0 being Real 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 being Real 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 end;

theorem :: FDIFF_2:48

for g, p being Real

for f being one-to-one PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds

0 < diff (f,x0) or for x0 being Real 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 being Real st x0 in dom ((f | ].p,g.[) ") holds

diff (((f | ].p,g.[) "),x0) = 1 / (diff (f,(((f | ].p,g.[) ") . x0))) ) )

for f being one-to-one PartFunc of REAL,REAL st ].p,g.[ c= dom f & f is_differentiable_on ].p,g.[ & ( for x0 being Real st x0 in ].p,g.[ holds

0 < diff (f,x0) or for x0 being Real 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 being Real st x0 in dom ((f | ].p,g.[) ") holds

diff (((f | ].p,g.[) "),x0) = 1 / (diff (f,(((f | ].p,g.[) ") . x0))) ) )

proof end;

theorem :: FDIFF_2:49

for x0 being Real

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence 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) )

for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() Real_Sequence 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 end;