:: by Konrad Raczkowski and Pawe{\l} Sadowski

::

:: Received June 18, 1990

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

theorem Th1: :: FDIFF_1:1

for Y being Subset of REAL holds

( ( for r being Real holds

( r in Y iff r in REAL ) ) iff Y = REAL )

( ( for r being Real holds

( r in Y iff r in REAL ) ) iff Y = REAL )

proof end;

:: deftheorem Def1 defines -convergent FDIFF_1:def 1 :

for x being Real

for IT being Real_Sequence holds

( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

for x being Real

for IT being Real_Sequence holds

( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

registration

ex b_{1} being Real_Sequence st

( b_{1} is 0 -convergent & b_{1} is non-zero )
end;

cluster V1() V4( NAT ) V5( REAL ) Function-like non empty total non-zero quasi_total complex-valued ext-real-valued real-valued 0 -convergent for Element of K19(K20(NAT,REAL));

existence ex b

( b

proof end;

registration
end;

registration
end;

set cs = seq_const 0;

definition

let IT be PartFunc of REAL,REAL;

end;
attr IT is RestFunc-like means :Def2: :: FDIFF_1:def 2

( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) );

( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) );

:: deftheorem Def2 defines RestFunc-like FDIFF_1:def 2 :

for IT being PartFunc of REAL,REAL holds

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) ) );

for IT being PartFunc of REAL,REAL holds

( IT is RestFunc-like iff ( IT is total & ( for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) ) ) );

registration

ex b_{1} being PartFunc of REAL,REAL st b_{1} is RestFunc-like
end;

cluster V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued RestFunc-like for Element of K19(K20(REAL,REAL));

existence ex b

proof end;

:: deftheorem Def3 defines linear FDIFF_1:def 3 :

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

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

ex b_{1} being PartFunc of REAL,REAL st b_{1} is linear
end;

cluster V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued linear for Element of K19(K20(REAL,REAL));

existence ex b

proof end;

theorem Th4: :: FDIFF_1:4

for R1, R2 being RestFunc holds

( R1 + R2 is RestFunc & R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )

( R1 + R2 is RestFunc & R1 - R2 is RestFunc & R1 (#) R2 is RestFunc )

proof end;

definition

let f be PartFunc of REAL,REAL;

let x0 be Real;

end;
let x0 be Real;

pred f is_differentiable_in x0 means :: FDIFF_1:def 4

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

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 LinearFunc ex R being RestFunc st

for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) );

:: deftheorem defines is_differentiable_in FDIFF_1:def 4 :

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) );

for f being PartFunc of REAL,REAL

for x0 being Real holds

( f is_differentiable_in x0 iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc 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;

assume A1: f is_differentiable_in x0 ;

ex b_{1} being Real ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b_{1} = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )

for b_{1}, b_{2} being Real st ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b_{1} = 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 LinearFunc ex R being RestFunc st

( b_{2} = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) holds

b_{1} = b_{2}

end;
let x0 be Real;

assume A1: f is_differentiable_in x0 ;

func diff (f,x0) -> Real means :Def5: :: FDIFF_1:def 5

ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc 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 N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( it = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) );

ex b

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) )

proof end;

uniqueness for b

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) & ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) holds

b

proof end;

:: deftheorem Def5 defines diff FDIFF_1:def 5 :

for f being PartFunc of REAL,REAL

for x0 being Real st f is_differentiable_in x0 holds

for b_{3} being Real holds

( b_{3} = diff (f,x0) iff ex N being Neighbourhood of x0 st

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b_{3} = L . 1 & ( for x being Real st x in N holds

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );

for f being PartFunc of REAL,REAL

for x0 being Real st f is_differentiable_in x0 holds

for b

( b

( N c= dom f & ex L being LinearFunc ex R being RestFunc st

( b

(f . x) - (f . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) );

definition

let f be PartFunc of REAL,REAL;

let X be set ;

end;
let X be set ;

pred f is_differentiable_on X means :: FDIFF_1:def 6

( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) );

( X c= dom f & ( for x being Real st x in X holds

f | X is_differentiable_in x ) );

:: deftheorem defines is_differentiable_on FDIFF_1:def 6 :

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

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 Th8: :: FDIFF_1:8

for X being set

for f being PartFunc of REAL,REAL st f is_differentiable_on X holds

X is Subset of REAL by XBOOLE_1:1;

for f being PartFunc of REAL,REAL st f is_differentiable_on X holds

X is Subset of REAL by XBOOLE_1:1;

theorem Th9: :: FDIFF_1:9

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

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:10

for Y being Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on Y holds

Y is open

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 ;

ex b_{1} being PartFunc of REAL,REAL st

( dom b_{1} = X & ( for x being Real st x in X holds

b_{1} . x = diff (f,x) ) )

for b_{1}, b_{2} being PartFunc of REAL,REAL st dom b_{1} = X & ( for x being Real st x in X holds

b_{1} . x = diff (f,x) ) & dom b_{2} = X & ( for x being Real st x in X holds

b_{2} . x = diff (f,x) ) holds

b_{1} = b_{2}

end;
let X be set ;

assume A1: f is_differentiable_on X ;

func f `| X -> PartFunc of REAL,REAL means :Def7: :: FDIFF_1:def 7

( dom it = X & ( for x being Real st x in X holds

it . x = diff (f,x) ) );

existence ( dom it = X & ( for x being Real st x in X holds

it . x = diff (f,x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines `| FDIFF_1:def 7 :

for f being PartFunc of REAL,REAL

for X being set st f is_differentiable_on X holds

for b_{3} being PartFunc of REAL,REAL holds

( b_{3} = f `| X iff ( dom b_{3} = X & ( for x being Real st x in X holds

b_{3} . x = diff (f,x) ) ) );

for f being PartFunc of REAL,REAL

for X being set st f is_differentiable_on X holds

for b

( b

b

theorem :: FDIFF_1:11

for Z being open Subset of REAL

for f being PartFunc of REAL,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 ) )

for f being PartFunc of REAL,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 non-zero Real_Sequence;

let n be Nat;

coherence

for b_{1} being Real_Sequence st b_{1} = h ^\ n holds

b_{1} is non-zero

end;
let n be Nat;

coherence

for b

b

proof end;

registration

let h be non-zero 0 -convergent Real_Sequence;

let n be Nat;

coherence

for b_{1} being Real_Sequence st b_{1} = h ^\ n holds

( b_{1} is non-zero & b_{1} is 0 -convergent )

end;
let n be Nat;

coherence

for b

( b

proof end;

theorem Th12: :: FDIFF_1:12

for f being PartFunc of REAL,REAL

for x0 being Real

for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() 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))) )

for x0 being Real

for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds

for h being non-zero 0 -convergent Real_Sequence

for c being V8() 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 Th13: :: FDIFF_1:13

for x0 being Real

for f1, f2 being PartFunc of REAL,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)) )

for f1, f2 being PartFunc of REAL,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 Th14: :: FDIFF_1:14

for x0 being Real

for f1, f2 being PartFunc of REAL,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)) )

for f1, f2 being PartFunc of REAL,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 Th15: :: FDIFF_1:15

for x0, r being Real

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

( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )

for f being PartFunc of REAL,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 Th16: :: FDIFF_1:16

for x0 being Real

for f1, f2 being PartFunc of REAL,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))) )

for f1, f2 being PartFunc of REAL,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 Th17: :: FDIFF_1:17

for Z being open Subset of REAL

for f being PartFunc of REAL,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 ) )

for f being PartFunc of REAL,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:18

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,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)) ) )

for f1, f2 being PartFunc of REAL,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:19

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,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)) ) )

for f1, f2 being PartFunc of REAL,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:20

for r being Real

for Z being open Subset of REAL

for f being PartFunc of REAL,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)) ) )

for Z being open Subset of REAL

for f being PartFunc of REAL,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:21

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,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))) ) )

for f1, f2 being PartFunc of REAL,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:22

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = 0 ) )

for f being PartFunc of REAL,REAL st Z c= dom f & f | Z is V8() holds

( f is_differentiable_on Z & ( for x being Real st x in Z holds

(f `| Z) . x = 0 ) )

proof end;

theorem :: FDIFF_1:23

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

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 Th24: :: FDIFF_1:24

for f being PartFunc of REAL,REAL

for x0 being Real st f is_differentiable_in x0 holds

f is_continuous_in x0

for x0 being Real st f is_differentiable_in x0 holds

f is_continuous_in x0

proof end;

theorem :: FDIFF_1:25

for X being set

for f being PartFunc of REAL,REAL st f is_differentiable_on X holds

f | X is continuous

for f being PartFunc of REAL,REAL st f is_differentiable_on X holds

f | X is continuous

proof end;

theorem Th26: :: FDIFF_1:26

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

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;

:: deftheorem Def8 defines differentiable FDIFF_1:def 8 :

for f being PartFunc of REAL,REAL holds

( f is differentiable iff f is_differentiable_on dom f );

for f being PartFunc of REAL,REAL holds

( f is differentiable iff f is_differentiable_on dom f );

Lm1: {} REAL is closed

by XBOOLE_1:3;

Lm2: [#] REAL is open

by XBOOLE_1:37, Lm1;

registration

ex b_{1} being Function of REAL,REAL st b_{1} is differentiable
end;

cluster V1() V4( REAL ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued differentiable for Element of K19(K20(REAL,REAL));

existence ex b

proof end;

theorem :: FDIFF_1:28