:: FDIFF_3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: FDIFF_3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 convergent_to_0 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 convergent_to_0 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being PartFunc of REAL , REAL
for x0 being Real st ( for h being convergent_to_0 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 convergent_to_0 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being PartFunc of REAL , REAL
for x0 being Real st ( for h being convergent_to_0 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 convergent_to_0 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;
pred f is_Lcontinuous_in x0 means :Def1: :: 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) ) ) );
pred f is_Rcontinuous_in x0 means :Def2: :: 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) ) ) );
pred f is_right_differentiable_in x0 means :Def3: :: FDIFF_3:def 3
( ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) & ( for h being convergent_to_0 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 :Def4: :: FDIFF_3:def 4
( ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 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 ) );
end;

:: deftheorem Def1 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) ) ) ) );

:: deftheorem Def2 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) ) ) ) );

:: deftheorem Def3 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 convergent_to_0 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 Def4 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 convergent_to_0 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being PartFunc of REAL , REAL
for x0 being Real st f is_left_differentiable_in x0 holds
f is_Lcontinuous_in x0
proof end;

theorem Th6: :: FDIFF_3:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th7: :: FDIFF_3:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being PartFunc of REAL , REAL
for x0 being Real st f is_right_differentiable_in x0 holds
f is_Rcontinuous_in x0
proof end;

theorem Th8: :: FDIFF_3:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

definition
let x0 be Real;
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 convergent_to_0 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
ex b1 being Real st
for h being convergent_to_0 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
b1 = lim ((h " ) (#) ((f * (h + c)) - (f * c)))
proof end;
uniqueness
for b1, b2 being Real st ( for h being convergent_to_0 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
b1 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) ) & ( for h being convergent_to_0 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
b2 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) ) holds
b1 = b2
proof end;
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 b3 being Real holds
( b3 = Ldiff f,x0 iff for h being convergent_to_0 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
b3 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) );

definition
let x0 be Real;
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 convergent_to_0 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
ex b1 being Real st
for h being convergent_to_0 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
b1 = lim ((h " ) (#) ((f * (h + c)) - (f * c)))
proof end;
uniqueness
for b1, b2 being Real st ( for h being convergent_to_0 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
b1 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) ) & ( for h being convergent_to_0 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
b2 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) ) holds
b1 = b2
proof end;
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 b3 being Real holds
( b3 = Rdiff f,x0 iff for h being convergent_to_0 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
b3 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) );

theorem Th9: :: FDIFF_3:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 convergent_to_0 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FDIFF_3:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FDIFF_3:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )) )
proof end;

theorem Th15: :: FDIFF_3:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 convergent_to_0 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FDIFF_3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: FDIFF_3:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )) )
proof end;

theorem :: FDIFF_3:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: FDIFF_3:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;