:: Real Function Differentiability - Part II :: by Jaros{\l}aw Kotowicz and Konrad Raczkowski :: :: Received January 10, 1991 :: Copyright (c) 1991-2012 Association of Mizar Users begin registration let h be non-zero 0 -convergent Real_Sequence; cluster - h -> non-zero convergent ; coherence ( - h is non-empty & - h is convergent ) proofend; 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 ) proofend; 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 V37() sequence of NAT proofend; 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 V37() sequence of NAT proofend; 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 ) proofend; 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 proofend; 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 proofend; 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))) proofend; 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 ) proofend; 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 ) proofend; scheme :: FDIFF_2:sch 1 ExIncSeqofNat{ F1() -> Real_Sequence, P1[ set ] } : ex q being V37() sequence of NAT st ( ( for n being Element of NAT holds P1[(F1() * q) . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds P1[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 & P1[F1() . m] ) proofend; 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 ) ) proofend; 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))) ) ) proofend; 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 ) ) ) proofend; 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 ) ) ) ) proofend; 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)) ) proofend; 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)) ) proofend; 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) ) proofend; 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)) ) proofend; 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 ) proofend; 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) ) proofend; 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) ) proofend; 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) ) proofend; 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)) ) proofend; Lm3: for f being PartFunc of REAL,REAL holds (f (#) f) " {0} = f " {0} proofend; 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) ) proofend; 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)) ) proofend; 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) ) proofend; 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 ) ) proofend; 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 V8() ) proofend; 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 V8() ) proofend; 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 V8() ) proofend; 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 V8() ) proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 ) proofend; 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 ) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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))) ) ) proofend; 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))) ) ) proofend; 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))) ) ) proofend; 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))) ) ) proofend; 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) ) proofend;