:: FDIFF_1 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_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being Subset of REAL holds
( ( for r being Real holds
( r in Y iff r in REAL ) ) iff Y = REAL )
proof end;

definition
let IT be Real_Sequence;
attr IT is convergent_to_0 means :Def1: :: FDIFF_1:def 1
( IT is_not_0 & IT is convergent & lim IT = 0 );
end;

:: deftheorem Def1 defines convergent_to_0 FDIFF_1:def 1 :
for IT being Real_Sequence holds
( IT is convergent_to_0 iff ( IT is_not_0 & IT is convergent & lim IT = 0 ) );

registration
cluster convergent_to_0 Relation of NAT , REAL ;
existence
ex b1 being Real_Sequence st b1 is convergent_to_0
proof end;
end;

reconsider cs = NAT --> 0 as Real_Sequence by FUNCOP_1:57;

Lm1: for n being Nat holds cs . n = 0
by FUNCOP_1:13;

registration
cluster constant Relation of NAT , REAL ;
existence
ex b1 being Real_Sequence st b1 is constant
proof end;
end;

registration
let s1 be constant Real_Sequence;
cluster -> constant subsequence of s1;
coherence
for b1 being subsequence of s1 holds b1 is constant
by SEQM_3:54;
end;

definition
let IT be PartFunc of REAL , REAL ;
canceled;
attr IT is REST-like means :Def3: :: FDIFF_1:def 3
( IT is total & ( for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (IT * h) is convergent & lim ((h " ) (#) (IT * h)) = 0 ) ) );
end;

:: deftheorem FDIFF_1:def 2 :
canceled;

:: deftheorem Def3 defines REST-like FDIFF_1:def 3 :
for IT being PartFunc of REAL , REAL holds
( IT is REST-like iff ( IT is total & ( for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (IT * h) is convergent & lim ((h " ) (#) (IT * h)) = 0 ) ) ) );

reconsider cf = REAL --> 0 as Function of REAL , REAL by FUNCOP_1:57;

Lm2: for r being Real holds cf . r = 0
by FUNCOP_1:13;

registration
cluster REST-like Relation of REAL , REAL ;
existence
ex b1 being PartFunc of REAL , REAL st b1 is REST-like
proof end;
end;

definition
mode REST is REST-like PartFunc of REAL , REAL ;
end;

definition
let IT be PartFunc of REAL , REAL ;
attr IT is linear means :Def4: :: FDIFF_1:def 4
( IT is total & ex r being Real st
for p being Real holds IT . p = r * p );
end;

:: deftheorem Def4 defines linear FDIFF_1:def 4 :
for IT being PartFunc of REAL , REAL holds
( IT is linear iff ( IT is total & ex r being Real st
for p being Real holds IT . p = r * p ) );

registration
cluster linear Relation of REAL , REAL ;
existence
ex b1 being PartFunc of REAL , REAL st b1 is linear
proof end;
end;

definition
mode LINEAR is linear PartFunc of REAL , REAL ;
end;

theorem :: FDIFF_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FDIFF_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FDIFF_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FDIFF_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th6: :: FDIFF_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being LINEAR holds
( L1 + L2 is LINEAR & L1 - L2 is LINEAR )
proof end;

theorem Th7: :: FDIFF_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for L being LINEAR holds r (#) L is LINEAR
proof end;

theorem Th8: :: FDIFF_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R1, R2 being REST holds
( R1 + R2 is REST & R1 - R2 is REST & R1 (#) R2 is REST )
proof end;

theorem Th9: :: FDIFF_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for R being REST holds r (#) R is REST
proof end;

theorem Th10: :: FDIFF_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L1, L2 being LINEAR holds L1 (#) L2 is REST-like
proof end;

theorem Th11: :: FDIFF_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being REST
for L being LINEAR holds
( R (#) L is REST & L (#) R is REST )
proof end;

definition
let f be PartFunc of REAL , REAL ;
let x0 be real number ;
pred f is_differentiable_in x0 means :Def5: :: FDIFF_1:def 5
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) );
end;

:: deftheorem Def5 defines is_differentiable_in FDIFF_1:def 5 :
for f being PartFunc of REAL , REAL
for x0 being real number holds
( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) );

definition
let f be PartFunc of REAL , REAL ;
let x0 be real number ;
assume A1: f is_differentiable_in x0 ;
func diff f,x0 -> Real means :Def6: :: FDIFF_1:def 6
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( it = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );
existence
ex b1 being Real ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )
proof end;
uniqueness
for b1, b2 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( b1 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( b2 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines diff FDIFF_1:def 6 :
for f being PartFunc of REAL , REAL
for x0 being real number st f is_differentiable_in x0 holds
for b3 being Real holds
( b3 = diff f,x0 iff ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
( b3 = L . 1 & ( for x being Real st x in N holds
(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );

definition
let f be PartFunc of REAL , REAL ;
let X be set ;
pred f is_differentiable_on X means :Def7: :: FDIFF_1:def 7
( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) );
end;

:: deftheorem Def7 defines is_differentiable_on FDIFF_1:def 7 :
for f being PartFunc of REAL , REAL
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Real st x in X holds
f | X is_differentiable_in x ) ) );

theorem :: FDIFF_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FDIFF_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FDIFF_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th15: :: FDIFF_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being PartFunc of REAL , REAL st f is_differentiable_on X holds
X is Subset of REAL
proof end;

theorem Th16: :: FDIFF_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Real st x in Z holds
f is_differentiable_in x ) ) )
proof end;

theorem :: FDIFF_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being Subset of REAL
for f being PartFunc of REAL , REAL st f is_differentiable_on Y holds
Y is open
proof end;

definition
let f be PartFunc of REAL , REAL ;
let X be set ;
assume A1: f is_differentiable_on X ;
func f `| X -> PartFunc of REAL , REAL means :Def8: :: FDIFF_1:def 8
( dom it = X & ( for x being Real st x in X holds
it . x = diff f,x ) );
existence
ex b1 being PartFunc of REAL , REAL st
( dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff f,x ) )
proof end;
uniqueness
for b1, b2 being PartFunc of REAL , REAL st dom b1 = X & ( for x being Real st x in X holds
b1 . x = diff f,x ) & dom b2 = X & ( for x being Real st x in X holds
b2 . x = diff f,x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines `| FDIFF_1:def 8 :
for f being PartFunc of REAL , REAL
for X being set st f is_differentiable_on X holds
for b3 being PartFunc of REAL , REAL holds
( b3 = f `| X iff ( dom b3 = X & ( for x being Real st x in X holds
b3 . x = diff f,x ) ) );

theorem :: FDIFF_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: FDIFF_1:19  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 Z being open Subset of REAL st Z c= dom f & ex r being Real st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
proof end;

registration
let h be convergent_to_0 Real_Sequence;
let n be Nat;
cluster h ^\ n -> convergent_to_0 ;
coherence
h ^\ n is convergent_to_0
proof end;
end;

registration
let c be constant Real_Sequence;
let n be Nat;
cluster c ^\ n -> constant ;
coherence
c ^\ n is constant
proof end;
end;

theorem Th20: :: FDIFF_1: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 number
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h " ) (#) ((f * (h + c)) - (f * c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f * (h + c)) - (f * c))) )
proof end;

theorem Th21: :: FDIFF_1:21  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_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff (f1 + f2),x0 = (diff f1,x0) + (diff f2,x0) )
proof end;

theorem Th22: :: FDIFF_1:22  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_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff (f1 - f2),x0 = (diff f1,x0) - (diff f2,x0) )
proof end;

theorem Th23: :: FDIFF_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for f being PartFunc of REAL , REAL
for x0 being Real st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff (r (#) f),x0 = r * (diff f,x0) )
proof end;

theorem Th24: :: FDIFF_1:24  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_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff (f1 (#) f2),x0 = ((f2 . x0) * (diff f1,x0)) + ((f1 . x0) * (diff f2,x0)) )
proof end;

theorem :: FDIFF_1:25  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 Z being open Subset of REAL st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 1 ) )
proof end;

theorem :: FDIFF_1:26  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 Z being open Subset of REAL st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff f1,x) + (diff f2,x) ) )
proof end;

theorem :: FDIFF_1:27  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 Z being open Subset of REAL st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = (diff f1,x) - (diff f2,x) ) )
proof end;

theorem :: FDIFF_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being Real
for f being PartFunc of REAL , REAL
for Z being open Subset of REAL st Z c= dom (r (#) f) & f is_differentiable_on Z holds
( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff f,x) ) )
proof end;

theorem :: FDIFF_1:29  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 Z being open Subset of REAL st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) f2) `| Z) . x = ((f2 . x) * (diff f1,x)) + ((f1 . x) * (diff f2,x)) ) )
proof end;

theorem :: FDIFF_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom f & f is_constant_on Z holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) )
proof end;

theorem :: FDIFF_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, p being Real
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom f & ( for x being Real st x in Z holds
f . x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )
proof end;

theorem Th32: :: FDIFF_1:32  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 number st f is_differentiable_in x0 holds
f is_continuous_in x0
proof end;

theorem :: FDIFF_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for f being PartFunc of REAL , REAL st f is_differentiable_on X holds
f is_continuous_on X
proof end;

theorem :: FDIFF_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proof end;

theorem :: FDIFF_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x0 being Real
for f being PartFunc of REAL , REAL st f is_differentiable_in x0 holds
ex R being REST st
( R . 0 = 0 & R is_continuous_in 0 )
proof end;