:: FDIFF_2 semantic presentation

definition
let c1 be convergent_to_0 Real_Sequence;
redefine func - as - c1 -> convergent_to_0 Real_Sequence;
coherence
- c1 is convergent_to_0 Real_Sequence
proof end;
end;

theorem Th1: :: FDIFF_2:1
for b1, b2, b3 being Real_Sequence st b1 is convergent & b2 is convergent & lim b1 = lim b2 & ( for b4 being Nat holds
( b3 . (2 * b4) = b1 . b4 & b3 . ((2 * b4) + 1) = b2 . b4 ) ) holds
( b3 is convergent & lim b3 = lim b1 )
proof end;

theorem Th2: :: FDIFF_2:2
for b1 being Real_Sequence st ( for b2 being Nat holds b1 . b2 = 2 * b2 ) holds
( b1 is increasing & b1 is natural-yielding )
proof end;

theorem Th3: :: FDIFF_2:3
for b1 being Real_Sequence st ( for b2 being Nat holds b1 . b2 = (2 * b2) + 1 ) holds
( b1 is increasing & b1 is natural-yielding )
proof end;

theorem Th4: :: FDIFF_2:4
for b1 being Real
for b2 being convergent_to_0 Real_Sequence
for b3 being constant Real_Sequence st rng b3 = {b1} holds
( b3 is convergent & lim b3 = b1 & b2 + b3 is convergent & lim (b2 + b3) = b1 )
proof end;

theorem Th5: :: FDIFF_2:5
for b1 being Real
for b2, b3 being Real_Sequence st rng b2 = {b1} & rng b3 = {b1} holds
b2 = b3
proof end;

theorem Th6: :: FDIFF_2:6
for b1 being Real_Sequence
for b2 being convergent_to_0 Real_Sequence st b1 is subsequence of b2 holds
b1 is convergent_to_0 Real_Sequence
proof end;

theorem Th7: :: FDIFF_2:7
for b1 being Real
for b2 being PartFunc of REAL , REAL st ( for b3 being convergent_to_0 Real_Sequence
for b4 being constant Real_Sequence st rng b4 = {b1} & rng (b3 + b4) c= dom b2 & {b1} c= dom b2 holds
(b3 " ) (#) ((b2 * (b3 + b4)) - (b2 * b4)) is convergent ) holds
for b3, b4 being convergent_to_0 Real_Sequence
for b5 being constant Real_Sequence st rng b5 = {b1} & rng (b3 + b5) c= dom b2 & rng (b4 + b5) c= dom b2 & {b1} c= dom b2 holds
lim ((b3 " ) (#) ((b2 * (b3 + b5)) - (b2 * b5))) = lim ((b4 " ) (#) ((b2 * (b4 + b5)) - (b2 * b5)))
proof end;

theorem Th8: :: FDIFF_2:8
for b1 being Real
for b2 being PartFunc of REAL , REAL st ex b3 being Neighbourhood of b1 st b3 c= dom b2 holds
ex b3 being convergent_to_0 Real_Sequenceex b4 being constant Real_Sequence st
( rng b4 = {b1} & rng (b3 + b4) c= dom b2 & {b1} c= dom b2 )
proof end;

theorem Th9: :: FDIFF_2:9
for b1 being Real_Sequence
for b2, b3 being PartFunc of REAL , REAL st rng b1 c= dom (b2 * b3) holds
( rng b1 c= dom b3 & rng (b3 * b1) c= dom b2 )
proof end;

scheme :: FDIFF_2:sch 1
s1{ F1() -> Real_Sequence, P1[ set ] } :
ex b1 being increasing Seq_of_Nat st
( ( for b2 being Nat holds P1[(F1() * b1) . b2] ) & ( for b2 being Nat st ( for b3 being Real st b3 = F1() . b2 holds
P1[b3] ) holds
ex b3 being Nat st b2 = b1 . b3 ) )
provided
E10: for b1 being Nat ex b2 being Nat st
( b1 <= b2 & P1[F1() . b2] )
proof end;

theorem Th10: :: FDIFF_2:10
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL st b3 . b1 <> b2 & b3 is_differentiable_in b1 holds
ex b4 being Neighbourhood of b1 st
( b4 c= dom b3 & ( for b5 being Real st b5 in b4 holds
b3 . b5 <> b2 ) )
proof end;

Lemma10: for b1 being Real
for b2 being PartFunc of REAL , REAL st ex b3 being Neighbourhood of b1 st b3 c= dom b2 & ( for b3 being convergent_to_0 Real_Sequence
for b4 being constant Real_Sequence st rng b4 = {b1} & rng (b3 + b4) c= dom b2 holds
(b3 " ) (#) ((b2 * (b3 + b4)) - (b2 * b4)) is convergent ) holds
( b2 is_differentiable_in b1 & ( for b3 being convergent_to_0 Real_Sequence
for b4 being constant Real_Sequence st rng b4 = {b1} & rng (b3 + b4) c= dom b2 holds
diff b2,b1 = lim ((b3 " ) (#) ((b2 * (b3 + b4)) - (b2 * b4))) ) )
proof end;

theorem Th11: :: FDIFF_2:11
for b1 being Real
for b2 being PartFunc of REAL , REAL holds
( b2 is_differentiable_in b1 iff ( ex b3 being Neighbourhood of b1 st b3 c= dom b2 & ( for b3 being convergent_to_0 Real_Sequence
for b4 being constant Real_Sequence st rng b4 = {b1} & rng (b3 + b4) c= dom b2 holds
(b3 " ) (#) ((b2 * (b3 + b4)) - (b2 * b4)) is convergent ) ) )
proof end;

theorem Th12: :: FDIFF_2:12
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL holds
( b3 is_differentiable_in b1 & diff b3,b1 = b2 iff ( ex b4 being Neighbourhood of b1 st b4 c= dom b3 & ( for b4 being convergent_to_0 Real_Sequence
for b5 being constant Real_Sequence st rng b5 = {b1} & rng (b4 + b5) c= dom b3 holds
( (b4 " ) (#) ((b3 * (b4 + b5)) - (b3 * b5)) is convergent & lim ((b4 " ) (#) ((b3 * (b4 + b5)) - (b3 * b5))) = b2 ) ) ) )
proof end;

Lemma13: for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st ex b4 being Neighbourhood of b1 st b4 c= dom (b2 * b3) & b3 is_differentiable_in b1 & b2 is_differentiable_in b3 . b1 holds
( b2 * b3 is_differentiable_in b1 & diff (b2 * b3),b1 = (diff b2,(b3 . b1)) * (diff b3,b1) )
proof end;

theorem Th13: :: FDIFF_2:13
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 is_differentiable_in b1 & b3 is_differentiable_in b2 . b1 holds
( b3 * b2 is_differentiable_in b1 & diff (b3 * b2),b1 = (diff b3,(b2 . b1)) * (diff b2,b1) )
proof end;

theorem Th14: :: FDIFF_2:14
for b1 being Real
for b2, b3 being PartFunc of REAL , REAL st b2 . b1 <> 0 & b3 is_differentiable_in b1 & b2 is_differentiable_in b1 holds
( b3 / b2 is_differentiable_in b1 & diff (b3 / b2),b1 = (((diff b3,b1) * (b2 . b1)) - ((diff b2,b1) * (b3 . b1))) / ((b2 . b1) ^2 ) )
proof end;

theorem Th15: :: FDIFF_2:15
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 . b1 <> 0 & b2 is_differentiable_in b1 holds
( b2 ^ is_differentiable_in b1 & diff (b2 ^ ),b1 = - ((diff b2,b1) / ((b2 . b1) ^2 )) )
proof end;

theorem Th16: :: FDIFF_2:16
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 holds
( b2 | b1 is_differentiable_on b1 & b2 `| b1 = (b2 | b1) `| b1 )
proof end;

theorem Th17: :: FDIFF_2:17
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 & b3 is_differentiable_on b1 holds
( b2 + b3 is_differentiable_on b1 & (b2 + b3) `| b1 = (b2 `| b1) + (b3 `| b1) )
proof end;

theorem Th18: :: FDIFF_2:18
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 & b3 is_differentiable_on b1 holds
( b2 - b3 is_differentiable_on b1 & (b2 - b3) `| b1 = (b2 `| b1) - (b3 `| b1) )
proof end;

theorem Th19: :: FDIFF_2:19
for b1 being Real
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on b2 holds
( b1 (#) b3 is_differentiable_on b2 & (b1 (#) b3) `| b2 = b1 (#) (b3 `| b2) )
proof end;

theorem Th20: :: FDIFF_2:20
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 & b3 is_differentiable_on b1 holds
( b2 (#) b3 is_differentiable_on b1 & (b2 (#) b3) `| b1 = ((b2 `| b1) (#) b3) + (b2 (#) (b3 `| b1)) )
proof end;

Lemma17: for b1 being PartFunc of REAL , REAL holds (b1 (#) b1) " {0} = b1 " {0}
proof end;

theorem Th21: :: FDIFF_2:21
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 & b3 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
b3 . b4 <> 0 ) holds
( b2 / b3 is_differentiable_on b1 & (b2 / b3) `| b1 = (((b2 `| b1) (#) b3) - ((b3 `| b1) (#) b2)) / (b3 (#) b3) )
proof end;

theorem Th22: :: FDIFF_2:22
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
b2 . b3 <> 0 ) holds
( b2 ^ is_differentiable_on b1 & (b2 ^ ) `| b1 = - ((b2 `| b1) / (b2 (#) b2)) )
proof end;

theorem Th23: :: FDIFF_2:23
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b2 is_differentiable_on b1 & b2 .: b1 is open Subset of REAL & b3 is_differentiable_on b2 .: b1 holds
( b3 * b2 is_differentiable_on b1 & (b3 * b2) `| b1 = ((b3 `| (b2 .: b1)) * b2) (#) (b2 `| b1) )
proof end;

theorem Th24: :: FDIFF_2:24
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & ( for b3, b4 being Real st b3 in b1 & b4 in b1 holds
abs ((b2 . b3) - (b2 . b4)) <= (b3 - b4) ^2 ) holds
( b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
diff b2,b3 = 0 ) )
proof end;

theorem Th25: :: FDIFF_2:25
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL st ( for b4, b5 being Real st b4 in ].b1,b2.[ & b5 in ].b1,b2.[ holds
abs ((b3 . b4) - (b3 . b5)) <= (b4 - b5) ^2 ) & b1 < b2 & ].b1,b2.[ c= dom b3 holds
( b3 is_differentiable_on ].b1,b2.[ & b3 is_constant_on ].b1,b2.[ )
proof end;

theorem Th26: :: FDIFF_2:26
for b1 being Real
for b2 being PartFunc of REAL , REAL st left_open_halfline b1 c= dom b2 & ( for b3, b4 being Real st b3 in left_open_halfline b1 & b4 in left_open_halfline b1 holds
abs ((b2 . b3) - (b2 . b4)) <= (b3 - b4) ^2 ) holds
( b2 is_differentiable_on left_open_halfline b1 & b2 is_constant_on left_open_halfline b1 )
proof end;

theorem Th27: :: FDIFF_2:27
for b1 being Real
for b2 being PartFunc of REAL , REAL st right_open_halfline b1 c= dom b2 & ( for b3, b4 being Real st b3 in right_open_halfline b1 & b4 in right_open_halfline b1 holds
abs ((b2 . b3) - (b2 . b4)) <= (b3 - b4) ^2 ) holds
( b2 is_differentiable_on right_open_halfline b1 & b2 is_constant_on right_open_halfline b1 )
proof end;

theorem Th28: :: FDIFF_2:28
for b1 being PartFunc of REAL , REAL st b1 is total & ( for b2, b3 being Real holds abs ((b1 . b2) - (b1 . b3)) <= (b2 - b3) ^2 ) holds
( b1 is_differentiable_on [#] REAL & b1 is_constant_on [#] REAL )
proof end;

theorem Th29: :: FDIFF_2:29
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on left_open_halfline b1 & ( for b3 being Real st b3 in left_open_halfline b1 holds
0 < diff b2,b3 ) holds
( b2 is_increasing_on left_open_halfline b1 & b2 | (left_open_halfline b1) is one-to-one )
proof end;

theorem Th30: :: FDIFF_2:30
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on left_open_halfline b1 & ( for b3 being Real st b3 in left_open_halfline b1 holds
diff b2,b3 < 0 ) holds
( b2 is_decreasing_on left_open_halfline b1 & b2 | (left_open_halfline b1) is one-to-one )
proof end;

theorem Th31: :: FDIFF_2:31
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on left_open_halfline b1 & ( for b3 being Real st b3 in left_open_halfline b1 holds
0 <= diff b2,b3 ) holds
b2 is_non_decreasing_on left_open_halfline b1
proof end;

theorem Th32: :: FDIFF_2:32
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on left_open_halfline b1 & ( for b3 being Real st b3 in left_open_halfline b1 holds
diff b2,b3 <= 0 ) holds
b2 is_non_increasing_on left_open_halfline b1
proof end;

theorem Th33: :: FDIFF_2:33
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on right_open_halfline b1 & ( for b3 being Real st b3 in right_open_halfline b1 holds
0 < diff b2,b3 ) holds
( b2 is_increasing_on right_open_halfline b1 & b2 | (right_open_halfline b1) is one-to-one )
proof end;

theorem Th34: :: FDIFF_2:34
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on right_open_halfline b1 & ( for b3 being Real st b3 in right_open_halfline b1 holds
diff b2,b3 < 0 ) holds
( b2 is_decreasing_on right_open_halfline b1 & b2 | (right_open_halfline b1) is one-to-one )
proof end;

theorem Th35: :: FDIFF_2:35
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on right_open_halfline b1 & ( for b3 being Real st b3 in right_open_halfline b1 holds
0 <= diff b2,b3 ) holds
b2 is_non_decreasing_on right_open_halfline b1
proof end;

theorem Th36: :: FDIFF_2:36
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on right_open_halfline b1 & ( for b3 being Real st b3 in right_open_halfline b1 holds
diff b2,b3 <= 0 ) holds
b2 is_non_increasing_on right_open_halfline b1
proof end;

theorem Th37: :: FDIFF_2:37
for b1 being PartFunc of REAL , REAL st b1 is_differentiable_on [#] REAL & ( for b2 being Real holds 0 < diff b1,b2 ) holds
( b1 is_increasing_on [#] REAL & b1 is one-to-one )
proof end;

theorem Th38: :: FDIFF_2:38
for b1 being PartFunc of REAL , REAL st b1 is_differentiable_on [#] REAL & ( for b2 being Real holds diff b1,b2 < 0 ) holds
( b1 is_decreasing_on [#] REAL & b1 is one-to-one )
proof end;

theorem Th39: :: FDIFF_2:39
for b1 being PartFunc of REAL , REAL st b1 is_differentiable_on [#] REAL & ( for b2 being Real holds 0 <= diff b1,b2 ) holds
b1 is_non_decreasing_on [#] REAL
proof end;

theorem Th40: :: FDIFF_2:40
for b1 being PartFunc of REAL , REAL st b1 is_differentiable_on [#] REAL & ( for b2 being Real holds diff b1,b2 <= 0 ) holds
b1 is_non_increasing_on [#] REAL
proof end;

theorem Th41: :: FDIFF_2:41
for b1, b2 being Real
for b3 being PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
0 < diff b3,b4 or for b4 being Real st b4 in ].b1,b2.[ holds
diff b3,b4 < 0 ) holds
rng (b3 | ].b1,b2.[) is open
proof end;

theorem Th42: :: FDIFF_2:42
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on left_open_halfline b1 & ( for b3 being Real st b3 in left_open_halfline b1 holds
0 < diff b2,b3 or for b3 being Real st b3 in left_open_halfline b1 holds
diff b2,b3 < 0 ) holds
rng (b2 | (left_open_halfline b1)) is open
proof end;

theorem Th43: :: FDIFF_2:43
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_on right_open_halfline b1 & ( for b3 being Real st b3 in right_open_halfline b1 holds
0 < diff b2,b3 or for b3 being Real st b3 in right_open_halfline b1 holds
diff b2,b3 < 0 ) holds
rng (b2 | (right_open_halfline b1)) is open
proof end;

theorem Th44: :: FDIFF_2:44
for b1 being PartFunc of REAL , REAL st b1 is_differentiable_on [#] REAL & ( for b2 being Real holds 0 < diff b1,b2 or for b2 being Real holds diff b1,b2 < 0 ) holds
rng b1 is open
proof end;

theorem Th45: :: FDIFF_2:45
for b1 being one-to-one PartFunc of REAL , REAL st b1 is_differentiable_on [#] REAL & ( for b2 being Real holds 0 < diff b1,b2 or for b2 being Real holds diff b1,b2 < 0 ) holds
( b1 is one-to-one & b1 " is_differentiable_on dom (b1 " ) & ( for b2 being Real st b2 in dom (b1 " ) holds
diff (b1 " ),b2 = 1 / (diff b1,((b1 " ) . b2)) ) )
proof end;

theorem Th46: :: FDIFF_2:46
for b1 being Real
for b2 being one-to-one PartFunc of REAL , REAL st b2 is_differentiable_on left_open_halfline b1 & ( for b3 being Real st b3 in left_open_halfline b1 holds
0 < diff b2,b3 or for b3 being Real st b3 in left_open_halfline b1 holds
diff b2,b3 < 0 ) holds
( b2 | (left_open_halfline b1) is one-to-one & (b2 | (left_open_halfline b1)) " is_differentiable_on dom ((b2 | (left_open_halfline b1)) " ) & ( for b3 being Real st b3 in dom ((b2 | (left_open_halfline b1)) " ) holds
diff ((b2 | (left_open_halfline b1)) " ),b3 = 1 / (diff b2,(((b2 | (left_open_halfline b1)) " ) . b3)) ) )
proof end;

theorem Th47: :: FDIFF_2:47
for b1 being Real
for b2 being one-to-one PartFunc of REAL , REAL st b2 is_differentiable_on right_open_halfline b1 & ( for b3 being Real st b3 in right_open_halfline b1 holds
0 < diff b2,b3 or for b3 being Real st b3 in right_open_halfline b1 holds
diff b2,b3 < 0 ) holds
( b2 | (right_open_halfline b1) is one-to-one & (b2 | (right_open_halfline b1)) " is_differentiable_on dom ((b2 | (right_open_halfline b1)) " ) & ( for b3 being Real st b3 in dom ((b2 | (right_open_halfline b1)) " ) holds
diff ((b2 | (right_open_halfline b1)) " ),b3 = 1 / (diff b2,(((b2 | (right_open_halfline b1)) " ) . b3)) ) )
proof end;

theorem Th48: :: FDIFF_2:48
for b1, b2 being Real
for b3 being one-to-one PartFunc of REAL , REAL st b3 is_differentiable_on ].b1,b2.[ & ( for b4 being Real st b4 in ].b1,b2.[ holds
0 < diff b3,b4 or for b4 being Real st b4 in ].b1,b2.[ holds
diff b3,b4 < 0 ) holds
( b3 | ].b1,b2.[ is one-to-one & (b3 | ].b1,b2.[) " is_differentiable_on dom ((b3 | ].b1,b2.[) " ) & ( for b4 being Real st b4 in dom ((b3 | ].b1,b2.[) " ) holds
diff ((b3 | ].b1,b2.[) " ),b4 = 1 / (diff b3,(((b3 | ].b1,b2.[) " ) . b4)) ) )
proof end;

theorem Th49: :: FDIFF_2:49
for b1 being Real
for b2 being PartFunc of REAL , REAL st b2 is_differentiable_in b1 holds
for b3 being convergent_to_0 Real_Sequence
for b4 being constant Real_Sequence st rng b4 = {b1} & rng (b3 + b4) c= dom b2 & rng ((- b3) + b4) c= dom b2 holds
( ((2 (#) b3) " ) (#) ((b2 * (b4 + b3)) - (b2 * (b4 - b3))) is convergent & lim (((2 (#) b3) " ) (#) ((b2 * (b4 + b3)) - (b2 * (b4 - b3)))) = diff b2,b1 )
proof end;