:: by Ewa Burakowska and Beata Madras

::

:: Received December 12, 1991

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

theorem Th1: :: FDIFF_3:1

for f being PartFunc of REAL,REAL

for x0 being Real st ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) holds

ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st

( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) )

for x0 being Real st ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) holds

ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st

( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) )

proof end;

theorem Th2: :: FDIFF_3:2

for f being PartFunc of REAL,REAL

for x0 being Real st ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) holds

ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st

( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) )

for x0 being Real st ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) holds

ex h being non-zero 0 -convergent Real_Sequence ex c being constant Real_Sequence st

( rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) )

proof end;

theorem Th3: :: FDIFF_3:3

for f being PartFunc of REAL,REAL

for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds

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

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Nat holds h2 . n < 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds

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

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & ( for n being Nat holds h1 . n < 0 ) & rng (h2 + c) c= dom f & ( for n being Nat holds h2 . n < 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

proof end;

theorem Th4: :: FDIFF_3:4

for f being PartFunc of REAL,REAL

for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds

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

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

for x0 being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent ) & {x0} c= dom f holds

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

for c being constant Real_Sequence st rng c = {x0} & rng (h1 + c) c= dom f & rng (h2 + c) c= dom f & ( for n being Nat holds h1 . n > 0 ) & ( for n being Nat holds h2 . n > 0 ) holds

lim ((h1 ") (#) ((f /* (h1 + c)) - (f /* c))) = lim ((h2 ") (#) ((f /* (h2 + c)) - (f /* c)))

proof end;

definition

let f be PartFunc of REAL,REAL;

let x0 be Real;

end;
let x0 be Real;

pred f is_Lcontinuous_in x0 means :: FDIFF_3:def 1

( x0 in dom f & ( for a being Real_Sequence st rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) );

( x0 in dom f & ( for a being Real_Sequence st rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) );

pred f is_Rcontinuous_in x0 means :: FDIFF_3:def 2

( x0 in dom f & ( for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) );

( x0 in dom f & ( for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) );

pred f is_right_differentiable_in x0 means :: FDIFF_3:def 3

( ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

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

( ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

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

pred f is_left_differentiable_in x0 means :: FDIFF_3:def 4

( ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

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

( ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

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

:: deftheorem defines is_Lcontinuous_in FDIFF_3:def 1 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_Lcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_Lcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= (left_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

:: deftheorem defines is_Rcontinuous_in FDIFF_3:def 2 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_Rcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_Rcontinuous_in x0 iff ( x0 in dom f & ( for a being Real_Sequence st rng a c= (right_open_halfline x0) /\ (dom f) & a is convergent & lim a = x0 holds

( f /* a is convergent & f . x0 = lim (f /* a) ) ) ) );

:: deftheorem defines is_right_differentiable_in FDIFF_3:def 3 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_differentiable_in x0 iff ( ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

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

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_right_differentiable_in x0 iff ( ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

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

:: deftheorem defines is_left_differentiable_in FDIFF_3:def 4 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_differentiable_in x0 iff ( ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

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

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_left_differentiable_in x0 iff ( ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

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

theorem Th5: :: FDIFF_3:5

for f being PartFunc of REAL,REAL

for x0 being Real st f is_left_differentiable_in x0 holds

f is_Lcontinuous_in x0

for x0 being Real st f is_left_differentiable_in x0 holds

f is_Lcontinuous_in x0

proof end;

theorem Th6: :: FDIFF_3:6

for f being PartFunc of REAL,REAL

for x0, g2 being Real st f is_Lcontinuous_in x0 & f . x0 <> g2 & ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) holds

ex r1 being Real st

( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds

f . g <> g2 ) )

for x0, g2 being Real st f is_Lcontinuous_in x0 & f . x0 <> g2 & ex r being Real st

( r > 0 & [.(x0 - r),x0.] c= dom f ) holds

ex r1 being Real st

( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds

f . g <> g2 ) )

proof end;

theorem Th7: :: FDIFF_3:7

for f being PartFunc of REAL,REAL

for x0 being Real st f is_right_differentiable_in x0 holds

f is_Rcontinuous_in x0

for x0 being Real st f is_right_differentiable_in x0 holds

f is_Rcontinuous_in x0

proof end;

theorem Th8: :: FDIFF_3:8

for f being PartFunc of REAL,REAL

for x0, g2 being Real st f is_Rcontinuous_in x0 & f . x0 <> g2 & ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) holds

ex r1 being Real st

( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds

f . g <> g2 ) )

for x0, g2 being Real st f is_Rcontinuous_in x0 & f . x0 <> g2 & ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) holds

ex r1 being Real st

( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds

f . g <> g2 ) )

proof end;

definition

let x0 be Real;

let f be PartFunc of REAL,REAL;

assume A1: f is_left_differentiable_in x0 ;

ex b_{1} being Real st

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b_{1} = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

for b_{1}, b_{2} being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b_{1} = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b_{2} = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of REAL,REAL;

assume A1: f is_left_differentiable_in x0 ;

func Ldiff (f,x0) -> Real means :Def5: :: FDIFF_3:def 5

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

it = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));

existence for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

it = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));

ex b

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b

proof end;

uniqueness for b

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b

b

proof end;

:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :

for x0 being Real

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

for b_{3} being Real holds

( b_{3} = Ldiff (f,x0) iff for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b_{3} = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) );

for x0 being Real

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

for b

( b

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

b

definition

let x0 be Real;

let f be PartFunc of REAL,REAL;

assume A1: f is_right_differentiable_in x0 ;

ex b_{1} being Real st

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b_{1} = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))

for b_{1}, b_{2} being Real st ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b_{1} = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b_{2} = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of REAL,REAL;

assume A1: f is_right_differentiable_in x0 ;

func Rdiff (f,x0) -> Real means :Def6: :: FDIFF_3:def 6

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

it = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));

existence for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

it = lim ((h ") (#) ((f /* (h + c)) - (f /* c)));

ex b

for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b

proof end;

uniqueness for b

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b

b

proof end;

:: deftheorem Def6 defines Rdiff FDIFF_3:def 6 :

for x0 being Real

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

for b_{3} being Real holds

( b_{3} = Rdiff (f,x0) iff for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b_{3} = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) );

for x0 being Real

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

for b

( b

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

b

theorem Th9: :: FDIFF_3:9

for f being PartFunc of REAL,REAL

for x0, g being Real holds

( f is_left_differentiable_in x0 & Ldiff (f,x0) = g iff ( ex r being Real st

( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) )

for x0, g being Real holds

( f is_left_differentiable_in x0 & Ldiff (f,x0) = g iff ( ex r being Real st

( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n < 0 ) holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g ) ) ) )

proof end;

theorem :: FDIFF_3:10

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds

( f1 + f2 is_left_differentiable_in x0 & Ldiff ((f1 + f2),x0) = (Ldiff (f1,x0)) + (Ldiff (f2,x0)) )

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds

( f1 + f2 is_left_differentiable_in x0 & Ldiff ((f1 + f2),x0) = (Ldiff (f1,x0)) + (Ldiff (f2,x0)) )

proof end;

theorem :: FDIFF_3:11

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds

( f1 - f2 is_left_differentiable_in x0 & Ldiff ((f1 - f2),x0) = (Ldiff (f1,x0)) - (Ldiff (f2,x0)) )

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds

( f1 - f2 is_left_differentiable_in x0 & Ldiff ((f1 - f2),x0) = (Ldiff (f1,x0)) - (Ldiff (f2,x0)) )

proof end;

theorem :: FDIFF_3:12

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds

( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds

( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )

proof end;

Lm1: for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & ex r0 being Real st

( r0 > 0 & ( for g being Real st g in dom f2 & g in [.(x0 - r0),x0.] holds

f2 . g <> 0 ) ) holds

( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof end;

theorem :: FDIFF_3:13

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2 . x0 <> 0 holds

( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & f2 . x0 <> 0 holds

( f1 / f2 is_left_differentiable_in x0 & Ldiff ((f1 / f2),x0) = (((Ldiff (f1,x0)) * (f2 . x0)) - ((Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof end;

Lm2: for f being PartFunc of REAL,REAL

for x0 being Real st f is_left_differentiable_in x0 & ex r0 being Real st

( r0 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r0),x0.] holds

f . g <> 0 ) ) holds

( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem :: FDIFF_3:14

for f being PartFunc of REAL,REAL

for x0 being Real st f is_left_differentiable_in x0 & f . x0 <> 0 holds

( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

for x0 being Real st f is_left_differentiable_in x0 & f . x0 <> 0 holds

( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem Th15: :: FDIFF_3:15

for f being PartFunc of REAL,REAL

for x0, g1 being Real holds

( f is_right_differentiable_in x0 & Rdiff (f,x0) = g1 iff ( ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g1 ) ) ) )

for x0, g1 being Real holds

( f is_right_differentiable_in x0 & Rdiff (f,x0) = g1 iff ( ex r being Real st

( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being non-zero 0 -convergent Real_Sequence

for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds

( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g1 ) ) ) )

proof end;

theorem :: FDIFF_3:16

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds

( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds

( f1 + f2 is_right_differentiable_in x0 & Rdiff ((f1 + f2),x0) = (Rdiff (f1,x0)) + (Rdiff (f2,x0)) )

proof end;

theorem :: FDIFF_3:17

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds

( f1 - f2 is_right_differentiable_in x0 & Rdiff ((f1 - f2),x0) = (Rdiff (f1,x0)) - (Rdiff (f2,x0)) )

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds

( f1 - f2 is_right_differentiable_in x0 & Rdiff ((f1 - f2),x0) = (Rdiff (f1,x0)) - (Rdiff (f2,x0)) )

proof end;

theorem :: FDIFF_3:18

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds

( f1 (#) f2 is_right_differentiable_in x0 & Rdiff ((f1 (#) f2),x0) = ((Rdiff (f1,x0)) * (f2 . x0)) + ((Rdiff (f2,x0)) * (f1 . x0)) )

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 holds

( f1 (#) f2 is_right_differentiable_in x0 & Rdiff ((f1 (#) f2),x0) = ((Rdiff (f1,x0)) * (f2 . x0)) + ((Rdiff (f2,x0)) * (f1 . x0)) )

proof end;

Lm3: for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & ex r0 being Real st

( r0 > 0 & ( for g being Real st g in dom f2 & g in [.x0,(x0 + r0).] holds

f2 . g <> 0 ) ) holds

( f1 / f2 is_right_differentiable_in x0 & Rdiff ((f1 / f2),x0) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof end;

theorem :: FDIFF_3:19

for f1, f2 being PartFunc of REAL,REAL

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & f2 . x0 <> 0 holds

( f1 / f2 is_right_differentiable_in x0 & Rdiff ((f1 / f2),x0) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

for x0 being Real st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & f2 . x0 <> 0 holds

( f1 / f2 is_right_differentiable_in x0 & Rdiff ((f1 / f2),x0) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) )

proof end;

Lm4: for f being PartFunc of REAL,REAL

for x0 being Real st f is_right_differentiable_in x0 & ex r0 being Real st

( r0 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r0).] holds

f . g <> 0 ) ) holds

( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem :: FDIFF_3:20

for f being PartFunc of REAL,REAL

for x0 being Real st f is_right_differentiable_in x0 & f . x0 <> 0 holds

( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )

for x0 being Real st f is_right_differentiable_in x0 & f . x0 <> 0 holds

( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )

proof end;

theorem :: FDIFF_3:21

for f being PartFunc of REAL,REAL

for x0 being Real st f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff (f,x0) = Ldiff (f,x0) holds

( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

for x0 being Real st f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & Rdiff (f,x0) = Ldiff (f,x0) holds

( f is_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

proof end;

theorem :: FDIFF_3:22

for f being PartFunc of REAL,REAL

for x0 being Real st f is_differentiable_in x0 holds

( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

for x0 being Real st f is_differentiable_in x0 holds

( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff (f,x0) = Rdiff (f,x0) & diff (f,x0) = Ldiff (f,x0) )

proof end;