:: FDIFF_3 semantic presentation

theorem Th1: :: FDIFF_3:1

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st ex b₃ being Real st
( b₃ > 0 & [.(b₂ - b₃),b₂.] c= dom b₁ ) holds
ex b₃ being convergent_to_0 Real_Sequenceex b₄ being constant Real_Sequence st
( rng b₄ = {b₂} & rng (b₃ + b₄) c= dom b₁ & ( for b₅ being Nat holds b₃ . b₅ < 0 ) )

proof end;

theorem Th2: :: FDIFF_3:2

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st ex b₃ being Real st
( b₃ > 0 & [.b₂,(b₂ + b₃).] c= dom b₁ ) holds
ex b₃ being convergent_to_0 Real_Sequenceex b₄ being constant Real_Sequence st
( rng b₄ = {b₂} & rng (b₃ + b₄) c= dom b₁ & ( for b₅ being Nat holds b₃ . b₅ > 0 ) )

proof end;

theorem Th3: :: FDIFF_3:3

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st ( for b₃ being convergent_to_0 Real_Sequence
for b₄ being constant Real_Sequence st rng b₄ = {b₂} & rng (b₃ + b₄) c= dom b₁ & ( for b₅ being Nat holds b₃ . b₅ < 0 ) holds
(b₃ " ) (#) ((b₁ * (b₃ + b₄)) - (b₁ * b₄)) is convergent ) & {b₂} c= dom b₁ holds
for b₃, b₄ being convergent_to_0 Real_Sequence
for b₅ being constant Real_Sequence st rng b₅ = {b₂} & rng (b₃ + b₅) c= dom b₁ & ( for b₆ being Nat holds b₃ . b₆ < 0 ) & rng (b₄ + b₅) c= dom b₁ & ( for b₆ being Nat holds b₄ . b₆ < 0 ) holds
lim ((b₃ " ) (#) ((b₁ * (b₃ + b₅)) - (b₁ * b₅))) = lim ((b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅)))

proof end;

theorem Th4: :: FDIFF_3:4

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st ( for b₃ being convergent_to_0 Real_Sequence
for b₄ being constant Real_Sequence st rng b₄ = {b₂} & rng (b₃ + b₄) c= dom b₁ & ( for b₅ being Nat holds b₃ . b₅ > 0 ) holds
(b₃ " ) (#) ((b₁ * (b₃ + b₄)) - (b₁ * b₄)) is convergent ) & {b₂} c= dom b₁ holds
for b₃, b₄ being convergent_to_0 Real_Sequence
for b₅ being constant Real_Sequence st rng b₅ = {b₂} & rng (b₃ + b₅) c= dom b₁ & rng (b₄ + b₅) c= dom b₁ & ( for b₆ being Nat holds b₃ . b₆ > 0 ) & ( for b₆ being Nat holds b₄ . b₆ > 0 ) holds
lim ((b₃ " ) (#) ((b₁ * (b₃ + b₅)) - (b₁ * b₅))) = lim ((b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅)))

proof end;

definition

let c₁ be PartFunc of REAL , REAL ;
let c₂ be Real;
pred c₁ is_Lcontinuous_in c₂ means :Def1: :: FDIFF_3:def 1
( a₂ in dom a₁ & ( for b₁ being Real_Sequence st rng b₁ c= (left_open_halfline a₂) /\ (dom a₁) & b₁ is convergent & lim b₁ = a₂ holds
( a₁ * b₁ is convergent & a₁ . a₂ = lim (a₁ * b₁) ) ) );
pred c₁ is_Rcontinuous_in c₂ means :Def2: :: FDIFF_3:def 2
( a₂ in dom a₁ & ( for b₁ being Real_Sequence st rng b₁ c= (right_open_halfline a₂) /\ (dom a₁) & b₁ is convergent & lim b₁ = a₂ holds
( a₁ * b₁ is convergent & a₁ . a₂ = lim (a₁ * b₁) ) ) );
pred c₁ is_right_differentiable_in c₂ means :Def3: :: FDIFF_3:def 3
( ex b₁ being Real st
( b₁ > 0 & [.a₂,(a₂ + b₁).] c= dom a₁ ) & ( for b₁ being convergent_to_0 Real_Sequence
for b₂ being constant Real_Sequence st rng b₂ = {a₂} & rng (b₁ + b₂) c= dom a₁ & ( for b₃ being Nat holds b₁ . b₃ > 0 ) holds
(b₁ " ) (#) ((a₁ * (b₁ + b₂)) - (a₁ * b₂)) is convergent ) );
pred c₁ is_left_differentiable_in c₂ means :Def4: :: FDIFF_3:def 4
( ex b₁ being Real st
( b₁ > 0 & [.(a₂ - b₁),a₂.] c= dom a₁ ) & ( for b₁ being convergent_to_0 Real_Sequence
for b₂ being constant Real_Sequence st rng b₂ = {a₂} & rng (b₁ + b₂) c= dom a₁ & ( for b₃ being Nat holds b₁ . b₃ < 0 ) holds
(b₁ " ) (#) ((a₁ * (b₁ + b₂)) - (a₁ * b₂)) is convergent ) );

end;

:: deftheorem Def1 defines is_Lcontinuous_in FDIFF_3:def 1 :

:: deftheorem Def2 defines is_Rcontinuous_in FDIFF_3:def 2 :

:: deftheorem Def3 defines is_right_differentiable_in FDIFF_3:def 3 :

:: deftheorem Def4 defines is_left_differentiable_in FDIFF_3:def 4 :

theorem Th5: :: FDIFF_3:5

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_left_differentiable_in b₂ holds
b₁ is_Lcontinuous_in b₂

proof end;

theorem Th6: :: FDIFF_3:6

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being Real st b₁ is_Lcontinuous_in b₂ & b₁ . b₂ <> b₃ & ex b₄ being Real st
( b₄ > 0 & [.(b₂ - b₄),b₂.] c= dom b₁ ) holds
ex b₄ being Real st
( b₄ > 0 & [.(b₂ - b₄),b₂.] c= dom b₁ & ( for b₅ being Real st b₅ in [.(b₂ - b₄),b₂.] holds
b₁ . b₅ <> b₃ ) )

proof end;

theorem Th7: :: FDIFF_3:7

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_right_differentiable_in b₂ holds
b₁ is_Rcontinuous_in b₂

proof end;

theorem Th8: :: FDIFF_3:8

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being Real st b₁ is_Rcontinuous_in b₂ & b₁ . b₂ <> b₃ & ex b₄ being Real st
( b₄ > 0 & [.b₂,(b₂ + b₄).] c= dom b₁ ) holds
ex b₄ being Real st
( b₄ > 0 & [.b₂,(b₂ + b₄).] c= dom b₁ & ( for b₅ being Real st b₅ in [.b₂,(b₂ + b₄).] holds
b₁ . b₅ <> b₃ ) )

proof end;

definition

let c₁ be Real;
let c₂ be PartFunc of REAL , REAL ;
assume E13: c₂ is_left_differentiable_in c₁ ;
func Ldiff c₂,c₁ -> Real means :Def5: :: FDIFF_3:def 5
for b₁ being convergent_to_0 Real_Sequence
for b₂ being constant Real_Sequence st rng b₂ = {a₁} & rng (b₁ + b₂) c= dom a₂ & ( for b₃ being Nat holds b₁ . b₃ < 0 ) holds
a₃ = lim ((b₁ " ) (#) ((a₂ * (b₁ + b₂)) - (a₂ * b₂)));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Ldiff FDIFF_3:def 5 :

definition

let c₁ be Real;
let c₂ be PartFunc of REAL , REAL ;
assume E14: c₂ is_right_differentiable_in c₁ ;
func Rdiff c₂,c₁ -> Real means :Def6: :: FDIFF_3:def 6
for b₁ being convergent_to_0 Real_Sequence
for b₂ being constant Real_Sequence st rng b₂ = {a₁} & rng (b₁ + b₂) c= dom a₂ & ( for b₃ being Nat holds b₁ . b₃ > 0 ) holds
a₃ = lim ((b₁ " ) (#) ((a₂ * (b₁ + b₂)) - (a₂ * b₂)));
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Rdiff FDIFF_3:def 6 :

theorem Th9: :: FDIFF_3:9

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being Real holds
( b₁ is_left_differentiable_in b₂ & Ldiff b₁,b₂ = b₃ iff ( ex b₄ being Real st
( 0 < b₄ & [.(b₂ - b₄),b₂.] c= dom b₁ ) & ( for b₄ being convergent_to_0 Real_Sequence
for b₅ being constant Real_Sequence st rng b₅ = {b₂} & rng (b₄ + b₅) c= dom b₁ & ( for b₆ being Nat holds b₄ . b₆ < 0 ) holds
( (b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅)) is convergent & lim ((b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅))) = b₃ ) ) ) )

proof end;

theorem Th10: :: FDIFF_3:10

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

proof end;

theorem Th11: :: FDIFF_3:11

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

proof end;

theorem Th12: :: FDIFF_3:12

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

proof end;

Lemma16: for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_left_differentiable_in b₃ & b₂ is_left_differentiable_in b₃ & ex b₄ being Real st
( b₄ > 0 & ( for b₅ being Real st b₅ in dom b₂ & b₅ in [.(b₃ - b₄),b₃.] holds
b₂ . b₅ <> 0 ) ) holds
( b₁ / b₂ is_left_differentiable_in b₃ & Ldiff (b₁ / b₂),b₃ = (((Ldiff b₁,b₃) * (b₂ . b₃)) - ((Ldiff b₂,b₃) * (b₁ . b₃))) / ((b₂ . b₃) ^2 ) )

proof end;

theorem Th13: :: FDIFF_3:13

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_left_differentiable_in b₃ & b₂ is_left_differentiable_in b₃ & b₂ . b₃ <> 0 holds
( b₁ / b₂ is_left_differentiable_in b₃ & Ldiff (b₁ / b₂),b₃ = (((Ldiff b₁,b₃) * (b₂ . b₃)) - ((Ldiff b₂,b₃) * (b₁ . b₃))) / ((b₂ . b₃) ^2 ) )

proof end;

Lemma17: for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_left_differentiable_in b₂ & ex b₃ being Real st
( b₃ > 0 & ( for b₄ being Real st b₄ in dom b₁ & b₄ in [.(b₂ - b₃),b₂.] holds
b₁ . b₄ <> 0 ) ) holds
( b₁ ^ is_left_differentiable_in b₂ & Ldiff (b₁ ^ ),b₂ = - ((Ldiff b₁,b₂) / ((b₁ . b₂) ^2 )) )

proof end;

theorem Th14: :: FDIFF_3:14

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_left_differentiable_in b₂ & b₁ . b₂ <> 0 holds
( b₁ ^ is_left_differentiable_in b₂ & Ldiff (b₁ ^ ),b₂ = - ((Ldiff b₁,b₂) / ((b₁ . b₂) ^2 )) )

proof end;

theorem Th15: :: FDIFF_3:15

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being Real holds
( b₁ is_right_differentiable_in b₂ & Rdiff b₁,b₂ = b₃ iff ( ex b₄ being Real st
( b₄ > 0 & [.b₂,(b₂ + b₄).] c= dom b₁ ) & ( for b₄ being convergent_to_0 Real_Sequence
for b₅ being constant Real_Sequence st rng b₅ = {b₂} & rng (b₄ + b₅) c= dom b₁ & ( for b₆ being Nat holds b₄ . b₆ > 0 ) holds
( (b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅)) is convergent & lim ((b₄ " ) (#) ((b₁ * (b₄ + b₅)) - (b₁ * b₅))) = b₃ ) ) ) )

proof end;

theorem Th16: :: FDIFF_3:16

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

proof end;

theorem Th17: :: FDIFF_3:17

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

proof end;

theorem Th18: :: FDIFF_3:18

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

proof end;

Lemma19: for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_right_differentiable_in b₃ & b₂ is_right_differentiable_in b₃ & ex b₄ being Real st
( b₄ > 0 & ( for b₅ being Real st b₅ in dom b₂ & b₅ in [.b₃,(b₃ + b₄).] holds
b₂ . b₅ <> 0 ) ) holds
( b₁ / b₂ is_right_differentiable_in b₃ & Rdiff (b₁ / b₂),b₃ = (((Rdiff b₁,b₃) * (b₂ . b₃)) - ((Rdiff b₂,b₃) * (b₁ . b₃))) / ((b₂ . b₃) ^2 ) )

proof end;

theorem Th19: :: FDIFF_3:19

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st b₁ is_right_differentiable_in b₃ & b₂ is_right_differentiable_in b₃ & b₂ . b₃ <> 0 holds
( b₁ / b₂ is_right_differentiable_in b₃ & Rdiff (b₁ / b₂),b₃ = (((Rdiff b₁,b₃) * (b₂ . b₃)) - ((Rdiff b₂,b₃) * (b₁ . b₃))) / ((b₂ . b₃) ^2 ) )

proof end;

Lemma20: for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_right_differentiable_in b₂ & ex b₃ being Real st
( b₃ > 0 & ( for b₄ being Real st b₄ in dom b₁ & b₄ in [.b₂,(b₂ + b₃).] holds
b₁ . b₄ <> 0 ) ) holds
( b₁ ^ is_right_differentiable_in b₂ & Rdiff (b₁ ^ ),b₂ = - ((Rdiff b₁,b₂) / ((b₁ . b₂) ^2 )) )

proof end;

theorem Th20: :: FDIFF_3:20

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_right_differentiable_in b₂ & b₁ . b₂ <> 0 holds
( b₁ ^ is_right_differentiable_in b₂ & Rdiff (b₁ ^ ),b₂ = - ((Rdiff b₁,b₂) / ((b₁ . b₂) ^2 )) )

proof end;

theorem Th21: :: FDIFF_3:21

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_right_differentiable_in b₂ & b₁ is_left_differentiable_in b₂ & Rdiff b₁,b₂ = Ldiff b₁,b₂ holds
( b₁ is_differentiable_in b₂ & diff b₁,b₂ = Rdiff b₁,b₂ & diff b₁,b₂ = Ldiff b₁,b₂ )

proof end;

theorem Th22: :: FDIFF_3:22

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_differentiable_in b₂ holds
( b₁ is_right_differentiable_in b₂ & b₁ is_left_differentiable_in b₂ & diff b₁,b₂ = Rdiff b₁,b₂ & diff b₁,b₂ = Ldiff b₁,b₂ )

proof end;