:: Real Function Differentiability - Part II
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received January 10, 1991
:: Copyright (c) 1991-2011 Association of Mizar Users

begin

definition

let h be convergent_to_0 Real_Sequence;
:: original: -
redefine func - h -> convergent_to_0 Real_Sequence;
coherence
- h is convergent_to_0 Real_Sequence

proof end;

end;

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 )

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 V36() 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 V36() sequence of NAT

proof end;

theorem Th4: :: FDIFF_2:4

for x0 being Real
for h being convergent_to_0 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 Th5: :: FDIFF_2:5

for r being Real
for a, b being Real_Sequence st rng a = {r} & rng b = {r} holds
a = b

proof end;

theorem Th6: :: FDIFF_2:6

for a being Real_Sequence
for h being convergent_to_0 Real_Sequence st a is subsequence of h holds
a is convergent_to_0 Real_Sequence

proof end;

theorem Th7: :: FDIFF_2:7

for g being Real
for f being PartFunc of REAL,REAL st ( for h being convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 f2, f1 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₁() -> Real_Sequence, P₁[ set ] } :

ex q being V36() sequence of NAT st
( ( for n being Element of NAT holds P₁[(F₁() * q) . n] ) & ( for n being Element of NAT st ( for r being Real st r = F₁() . n holds
P₁[r] ) holds
ex m being Element of NAT st n = q . m ) )

provided

A1: for n being Element of NAT ex m being Element of NAT st
( n <= m & P₁[F₁() . m] )

proof end;

theorem :: FDIFF_2:10

for x0, r being Real
for f being PartFunc of REAL,REAL st f . x0 <> r & f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )

proof end;

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 convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 convergent_to_0 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 f2, f1 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)) )

proof end;

theorem Th14: :: FDIFF_2:14

for x0 being Real
for f2, f1 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;

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)) )

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 )

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) )

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) )

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) )

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)) )

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) )

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)) )

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) )

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
abs ((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 p, g 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
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) & ].p,g.[ c= dom f holds
( f is_differentiable_on ].p,g.[ & f | ].p,g.[ is constant )

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
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) holds
( f is_differentiable_on left_open_halfline r & f | (left_open_halfline r) is constant )

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
abs ((f . r1) - (f . r2)) <= (r1 - r2) ^2 ) holds
( f is_differentiable_on right_open_halfline r & f | (right_open_halfline r) is constant )

proof end;

theorem :: FDIFF_2:28

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

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 )

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 )

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

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

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 )

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 )

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

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

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 )

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 )

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

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

proof end;

theorem Th41: :: FDIFF_2:41

for p, g 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

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

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

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

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))) ) )

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))) ) )

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))) ) )

proof end;

theorem :: FDIFF_2:48

for p, g 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))) ) )

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 convergent_to_0 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;