:: FDIFF_1 semantic presentation

theorem Th1: :: FDIFF_1:1

for b₁ being Subset of REAL holds
( ( for b₂ being Real holds
( b₂ in b₁ iff b₂ in REAL ) ) iff b₁ = REAL )

proof end;

definition

let c₁ be Real_Sequence;
attr a₁ is convergent_to_0 means :Def1: :: FDIFF_1:def 1
( a₁ is_not_0 & a₁ is convergent & lim a₁ = 0 );

end;

:: deftheorem Def1 defines convergent_to_0 FDIFF_1:def 1 :

registration

cluster convergent_to_0 Relation of NAT , REAL ;
existence

proof end;

end;

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

Lemma3: for b₁ being Nat holds c₁ . b₁ = 0
by FUNCOP_1:13;

registration

cluster constant Relation of NAT , REAL ;
existence

proof end;

end;

registration

let c₂ be constant Real_Sequence;
cluster -> constant subsequence of a₁;
coherence by SEQM_3:54;

end;

definition

let c₂ be PartFunc of REAL , REAL ;
canceled;
attr a₁ is REST-like means :Def3: :: FDIFF_1:def 3
( a₁ is total & ( for b₁ being convergent_to_0 Real_Sequence holds
( (b₁ " ) (#) (a₁ * b₁) is convergent & lim ((b₁ " ) (#) (a₁ * b₁)) = 0 ) ) );

end;

:: deftheorem Def2 FDIFF_1:def 2 :

:: deftheorem Def3 defines REST-like FDIFF_1:def 3 :

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

Lemma5: for b₁ being Real holds c₂ . b₁ = 0
by FUNCOP_1:13;

registration

cluster REST-like Relation of REAL , REAL ;
existence

proof end;

end;

definition

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

end;

definition

let c₃ be PartFunc of REAL , REAL ;
attr a₁ is linear means :Def4: :: FDIFF_1:def 4
( a₁ is total & ex b₁ being Real st
for b₂ being Real holds a₁ . b₂ = b₁ * b₂ );

end;

:: deftheorem Def4 defines linear FDIFF_1:def 4 :

registration

cluster linear Relation of REAL , REAL ;
existence

proof end;

end;

definition

mode LINEAR is linear PartFunc of REAL , REAL ;

end;

theorem Th2: :: FDIFF_1:2

canceled;

theorem Th3: :: FDIFF_1:3

canceled;

theorem Th4: :: FDIFF_1:4

canceled;

theorem Th5: :: FDIFF_1:5

canceled;

theorem Th6: :: FDIFF_1:6

for b₁, b₂ being LINEAR holds
( b₁ + b₂ is LINEAR & b₁ - b₂ is LINEAR )

proof end;

theorem Th7: :: FDIFF_1:7

for b₁ being Real
for b₂ being LINEAR holds b₁ (#) b₂ is LINEAR

proof end;

theorem Th8: :: FDIFF_1:8

for b₁, b₂ being REST holds
( b₁ + b₂ is REST & b₁ - b₂ is REST & b₁ (#) b₂ is REST )

proof end;

theorem Th9: :: FDIFF_1:9

for b₁ being Real
for b₂ being REST holds b₁ (#) b₂ is REST

proof end;

theorem Th10: :: FDIFF_1:10

for b₁, b₂ being LINEAR holds b₁ (#) b₂ is REST-like

proof end;

theorem Th11: :: FDIFF_1:11

for b₁ being REST
for b₂ being LINEAR holds
( b₁ (#) b₂ is REST & b₂ (#) b₁ is REST )

proof end;

definition

let c₃ be PartFunc of REAL , REAL ;
let c₄ be real number ;
pred c₁ is_differentiable_in c₂ means :Def5: :: FDIFF_1:def 5
ex b₁ being Neighbourhood of a₂ st
( b₁ c= dom a₁ & ex b₂ being LINEARex b₃ being REST st
for b₄ being Real st b₄ in b₁ holds
(a₁ . b₄) - (a₁ . a₂) = (b₂ . (b₄ - a₂)) + (b₃ . (b₄ - a₂)) );

end;

:: deftheorem Def5 defines is_differentiable_in FDIFF_1:def 5 :

definition

let c₃ be PartFunc of REAL , REAL ;
let c₄ be real number ;
assume E14: c₃ is_differentiable_in c₄ ;
func diff c₁,c₂ -> Real means :Def6: :: FDIFF_1:def 6
ex b₁ being Neighbourhood of a₂ st
( b₁ c= dom a₁ & ex b₂ being LINEARex b₃ being REST st
( a₃ = b₂ . 1 & ( for b₄ being Real st b₄ in b₁ holds
(a₁ . b₄) - (a₁ . a₂) = (b₂ . (b₄ - a₂)) + (b₃ . (b₄ - a₂)) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines diff FDIFF_1:def 6 :

definition

let c₃ be PartFunc of REAL , REAL ;
let c₄ be set ;
pred c₁ is_differentiable_on c₂ means :Def7: :: FDIFF_1:def 7
( a₂ c= dom a₁ & ( for b₁ being Real st b₁ in a₂ holds
a₁ | a₂ is_differentiable_in b₁ ) );

end;

:: deftheorem Def7 defines is_differentiable_on FDIFF_1:def 7 :

theorem Th12: :: FDIFF_1:12

canceled;

theorem Th13: :: FDIFF_1:13

canceled;

theorem Th14: :: FDIFF_1:14

canceled;

theorem Th15: :: FDIFF_1:15

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_differentiable_on b₁ holds
b₁ is Subset of REAL

proof end;

theorem Th16: :: FDIFF_1:16

for b₁ being open Subset of REAL
for b₂ being PartFunc of REAL , REAL holds
( b₂ is_differentiable_on b₁ iff ( b₁ c= dom b₂ & ( for b₃ being Real st b₃ in b₁ holds
b₂ is_differentiable_in b₃ ) ) )

proof end;

theorem Th17: :: FDIFF_1:17

for b₁ being Subset of REAL
for b₂ being PartFunc of REAL , REAL st b₂ is_differentiable_on b₁ holds
b₁ is open

proof end;

definition

let c₃ be PartFunc of REAL , REAL ;
let c₄ be set ;
assume E18: c₃ is_differentiable_on c₄ ;
func c₁ `| c₂ -> PartFunc of REAL , REAL means :Def8: :: FDIFF_1:def 8
( dom a₃ = a₂ & ( for b₁ being Real st b₁ in a₂ holds
a₃ . b₁ = diff a₁,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines `| FDIFF_1:def 8 :

theorem Th18: :: FDIFF_1:18

canceled;

theorem Th19: :: FDIFF_1:19

for b₁ being PartFunc of REAL , REAL
for b₂ being open Subset of REAL st b₂ c= dom b₁ & ex b₃ being Real st rng b₁ = {b₃} holds
( b₁ is_differentiable_on b₂ & ( for b₃ being Real st b₃ in b₂ holds
(b₁ `| b₂) . b₃ = 0 ) )

proof end;

registration

let c₃ be convergent_to_0 Real_Sequence;
let c₄ be Nat;
cluster a₁ ^\ a₂ -> convergent_to_0 ;
coherence

proof end;

end;

registration

let c₃ be constant Real_Sequence;
let c₄ be Nat;
cluster a₁ ^\ a₂ -> constant ;
coherence

proof end;

end;

theorem Th20: :: FDIFF_1:20

for b₁ being PartFunc of REAL , REAL
for b₂ being real number
for b₃ being Neighbourhood of b₂ st b₁ is_differentiable_in b₂ & b₃ c= dom b₁ holds
for b₄ being convergent_to_0 Real_Sequence
for b₅ being constant Real_Sequence st rng b₅ = {b₂} & rng (b₄ + b₅) c= b₃ holds
( (b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅)) is convergent & diff b₁,b₂ = lim ((b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅))) )

proof end;

theorem Th21: :: FDIFF_1:21

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_differentiable_in b₃ & b₂ is_differentiable_in b₃ holds
( b₁ + b₂ is_differentiable_in b₃ & diff (b₁ + b₂),b₃ = (diff b₁,b₃) + (diff b₂,b₃) )

proof end;

theorem Th22: :: FDIFF_1:22

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_differentiable_in b₃ & b₂ is_differentiable_in b₃ holds
( b₁ - b₂ is_differentiable_in b₃ & diff (b₁ - b₂),b₃ = (diff b₁,b₃) - (diff b₂,b₃) )

proof end;

theorem Th23: :: FDIFF_1:23

for b₁ being Real
for b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₂ is_differentiable_in b₃ holds
( b₁ (#) b₂ is_differentiable_in b₃ & diff (b₁ (#) b₂),b₃ = b₁ * (diff b₂,b₃) )

proof end;

theorem Th24: :: FDIFF_1:24

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_differentiable_in b₃ & b₂ is_differentiable_in b₃ holds
( b₁ (#) b₂ is_differentiable_in b₃ & diff (b₁ (#) b₂),b₃ = ((b₂ . b₃) * (diff b₁,b₃)) + ((b₁ . b₃) * (diff b₂,b₃)) )

proof end;

theorem Th25: :: FDIFF_1:25

for b₁ being PartFunc of REAL , REAL
for b₂ being open Subset of REAL st b₂ c= dom b₁ & b₁ | b₂ = id b₂ holds
( b₁ is_differentiable_on b₂ & ( for b₃ being Real st b₃ in b₂ holds
(b₁ `| b₂) . b₃ = 1 ) )

proof end;

theorem Th26: :: FDIFF_1:26

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being open Subset of REAL st b₃ c= dom (b₁ + b₂) & b₁ is_differentiable_on b₃ & b₂ is_differentiable_on b₃ holds
( b₁ + b₂ is_differentiable_on b₃ & ( for b₄ being Real st b₄ in b₃ holds
((b₁ + b₂) `| b₃) . b₄ = (diff b₁,b₄) + (diff b₂,b₄) ) )

proof end;

theorem Th27: :: FDIFF_1:27

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being open Subset of REAL st b₃ c= dom (b₁ - b₂) & b₁ is_differentiable_on b₃ & b₂ is_differentiable_on b₃ holds
( b₁ - b₂ is_differentiable_on b₃ & ( for b₄ being Real st b₄ in b₃ holds
((b₁ - b₂) `| b₃) . b₄ = (diff b₁,b₄) - (diff b₂,b₄) ) )

proof end;

theorem Th28: :: FDIFF_1:28

for b₁ being Real
for b₂ being PartFunc of REAL , REAL
for b₃ being open Subset of REAL st b₃ c= dom (b₁ (#) b₂) & b₂ is_differentiable_on b₃ holds
( b₁ (#) b₂ is_differentiable_on b₃ & ( for b₄ being Real st b₄ in b₃ holds
((b₁ (#) b₂) `| b₃) . b₄ = b₁ * (diff b₂,b₄) ) )

proof end;

theorem Th29: :: FDIFF_1:29

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being open Subset of REAL st b₃ c= dom (b₁ (#) b₂) & b₁ is_differentiable_on b₃ & b₂ is_differentiable_on b₃ holds
( b₁ (#) b₂ is_differentiable_on b₃ & ( for b₄ being Real st b₄ in b₃ holds
((b₁ (#) b₂) `| b₃) . b₄ = ((b₂ . b₄) * (diff b₁,b₄)) + ((b₁ . b₄) * (diff b₂,b₄)) ) )

proof end;

theorem Th30: :: FDIFF_1:30

for b₁ being open Subset of REAL
for b₂ being PartFunc of REAL , REAL st b₁ c= dom b₂ & b₂ is_constant_on b₁ holds
( b₂ is_differentiable_on b₁ & ( for b₃ being Real st b₃ in b₁ holds
(b₂ `| b₁) . b₃ = 0 ) )

proof end;

theorem Th31: :: FDIFF_1:31

for b₁, b₂ being Real
for b₃ being open Subset of REAL
for b₄ being PartFunc of REAL , REAL st b₃ c= dom b₄ & ( for b₅ being Real st b₅ in b₃ holds
b₄ . b₅ = (b₁ * b₅) + b₂ ) holds
( b₄ is_differentiable_on b₃ & ( for b₅ being Real st b₅ in b₃ holds
(b₄ `| b₃) . b₅ = b₁ ) )

proof end;

theorem Th32: :: FDIFF_1:32

for b₁ being PartFunc of REAL , REAL
for b₂ being real number st b₁ is_differentiable_in b₂ holds
b₁ is_continuous_in b₂

proof end;

theorem Th33: :: FDIFF_1:33

for b₁ being set
for b₂ being PartFunc of REAL , REAL st b₂ is_differentiable_on b₁ holds
b₂ is_continuous_on b₁

proof end;

theorem Th34: :: FDIFF_1:34

for b₁ being set
for b₂ being open Subset of REAL
for b₃ being PartFunc of REAL , REAL st b₃ is_differentiable_on b₁ & b₂ c= b₁ holds
b₃ is_differentiable_on b₂

proof end;

theorem Th35: :: FDIFF_1:35

for b₁ being Real
for b₂ being PartFunc of REAL , REAL st b₂ is_differentiable_in b₁ holds
ex b₃ being REST st
( b₃ . 0 = 0 & b₃ is_continuous_in 0 )

proof end;