:: FDIFF_5 semantic presentation

Lemma1: for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 + b4) & ( for b5 being Real st b5 in b2 holds
b3 . b5 = b1 ) & b4 = #Z 2 holds
( b3 + b4 is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 + b4) `| b2) . b5 = 2 * b5 ) )
proof end;

Lemma2: for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 - b4) & ( for b5 being Real st b5 in b2 holds
b3 . b5 = b1 ) & b4 = #Z 2 holds
( b3 - b4 is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 - b4) `| b2) . b5 = - (2 * b5) ) )
proof end;

Lemma3: for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((#R (1 / 2)) * b2) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 > 0 ) ) holds
( (#R (1 / 2)) * b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((#R (1 / 2)) * b2) `| b1) . b3 = (1 / 2) * (b3 #R (- (1 / 2))) ) )
proof end;

theorem Th1: :: FDIFF_5:1
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 / b4) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b1 + b5 & b4 . b5 = b1 - b5 & b4 . b5 <> 0 ) ) holds
( b3 / b4 is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 / b4) `| b2) . b5 = (2 * b1) / ((b1 - b5) ^2 ) ) )
proof end;

theorem Th2: :: FDIFF_5:2
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom (b3 / b4) & ( for b5 being Real st b5 in b2 holds
( b3 . b5 = b5 - b1 & b4 . b5 = b5 + b1 & b4 . b5 <> 0 ) ) holds
( b3 / b4 is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
((b3 / b4) `| b2) . b5 = (2 * b1) / ((b5 + b1) ^2 ) ) )
proof end;

theorem Th3: :: FDIFF_5:3
for b1, b2 being Real
for b3 being open Subset of REAL
for b4, b5 being PartFunc of REAL , REAL st b3 c= dom (b4 / b5) & ( for b6 being Real st b6 in b3 holds
( b4 . b6 = b6 - b1 & b5 . b6 = b6 - b2 & b5 . b6 <> 0 ) ) holds
( b4 / b5 is_differentiable_on b3 & ( for b6 being Real st b6 in b3 holds
((b4 / b5) `| b3) . b6 = (b1 - b2) / ((b6 - b2) ^2 ) ) )
proof end;

theorem Th4: :: FDIFF_5:4
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom b2 & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( b2 ^ is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((b2 ^ ) `| b1) . b3 = - (1 / (b3 ^2 )) ) )
proof end;

theorem Th5: :: FDIFF_5:5
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (sin * (b2 ^ )) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( sin * (b2 ^ ) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((sin * (b2 ^ )) `| b1) . b3 = - ((1 / (b3 ^2 )) * (cos . (1 / b3))) ) )
proof end;

theorem Th6: :: FDIFF_5:6
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (cos * (b2 ^ )) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( cos * (b2 ^ ) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((cos * (b2 ^ )) `| b1) . b3 = (1 / (b3 ^2 )) * (sin . (1 / b3)) ) )
proof end;

theorem Th7: :: FDIFF_5:7
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((id b1) (#) (sin * (b2 ^ ))) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( (id b1) (#) (sin * (b2 ^ )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((id b1) (#) (sin * (b2 ^ ))) `| b1) . b3 = (sin . (1 / b3)) - ((1 / b3) * (cos . (1 / b3))) ) )
proof end;

theorem Th8: :: FDIFF_5:8
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((id b1) (#) (cos * (b2 ^ ))) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( (id b1) (#) (cos * (b2 ^ )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((id b1) (#) (cos * (b2 ^ ))) `| b1) . b3 = (cos . (1 / b3)) + ((1 / b3) * (sin . (1 / b3))) ) )
proof end;

theorem Th9: :: FDIFF_5:9
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((sin * (b2 ^ )) (#) (cos * (b2 ^ ))) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( (sin * (b2 ^ )) (#) (cos * (b2 ^ )) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((sin * (b2 ^ )) (#) (cos * (b2 ^ ))) `| b1) . b3 = (1 / (b3 ^2 )) * (((sin . (1 / b3)) ^2 ) - ((cos . (1 / b3)) ^2 )) ) )
proof end;

theorem Th10: :: FDIFF_5:10
for b1 being Nat
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((sin * b3) (#) ((#Z b1) * sin )) & b1 >= 1 & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b1 * b4 ) holds
( (sin * b3) (#) ((#Z b1) * sin ) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((sin * b3) (#) ((#Z b1) * sin )) `| b2) . b4 = (b1 * ((sin . b4) #Z (b1 - 1))) * (sin . ((b1 + 1) * b4)) ) )
proof end;

theorem Th11: :: FDIFF_5:11
for b1 being Nat
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((cos * b3) (#) ((#Z b1) * sin )) & b1 >= 1 & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b1 * b4 ) holds
( (cos * b3) (#) ((#Z b1) * sin ) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((cos * b3) (#) ((#Z b1) * sin )) `| b2) . b4 = (b1 * ((sin . b4) #Z (b1 - 1))) * (cos . ((b1 + 1) * b4)) ) )
proof end;

theorem Th12: :: FDIFF_5:12
for b1 being Nat
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((cos * b3) (#) ((#Z b1) * cos )) & b1 >= 1 & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b1 * b4 ) holds
( (cos * b3) (#) ((#Z b1) * cos ) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((cos * b3) (#) ((#Z b1) * cos )) `| b2) . b4 = - ((b1 * ((cos . b4) #Z (b1 - 1))) * (sin . ((b1 + 1) * b4))) ) )
proof end;

theorem Th13: :: FDIFF_5:13
for b1 being Nat
for b2 being open Subset of REAL
for b3 being PartFunc of REAL , REAL st b2 c= dom ((sin * b3) (#) ((#Z b1) * cos )) & b1 >= 1 & ( for b4 being Real st b4 in b2 holds
b3 . b4 = b1 * b4 ) holds
( (sin * b3) (#) ((#Z b1) * cos ) is_differentiable_on b2 & ( for b4 being Real st b4 in b2 holds
(((sin * b3) (#) ((#Z b1) * cos )) `| b2) . b4 = (b1 * ((cos . b4) #Z (b1 - 1))) * (cos . ((b1 + 1) * b4)) ) )
proof end;

theorem Th14: :: FDIFF_5:14
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((b2 ^ ) (#) sin ) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( (b2 ^ ) (#) sin is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((b2 ^ ) (#) sin ) `| b1) . b3 = ((1 / b3) * (cos . b3)) - ((1 / (b3 ^2 )) * (sin . b3)) ) )
proof end;

theorem Th15: :: FDIFF_5:15
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((b2 ^ ) (#) cos ) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 <> 0 ) ) holds
( (b2 ^ ) (#) cos is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((b2 ^ ) (#) cos ) `| b1) . b3 = (- ((1 / b3) * (sin . b3))) - ((1 / (b3 ^2 )) * (cos . b3)) ) )
proof end;

theorem Th16: :: FDIFF_5:16
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom (sin + ((#R (1 / 2)) * b2)) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 > 0 ) ) holds
( sin + ((#R (1 / 2)) * b2) is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
((sin + ((#R (1 / 2)) * b2)) `| b1) . b3 = (cos . b3) + ((1 / 2) * (b3 #R (- (1 / 2)))) ) )
proof end;

theorem Th17: :: FDIFF_5:17
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom (b2 (#) (sin * (b3 ^ ))) & b2 = #Z 2 & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = b4 & b3 . b4 <> 0 ) ) holds
( b2 (#) (sin * (b3 ^ )) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
((b2 (#) (sin * (b3 ^ ))) `| b1) . b4 = ((2 * b4) * (sin . (1 / b4))) - (cos . (1 / b4)) ) )
proof end;

theorem Th18: :: FDIFF_5:18
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom (b2 (#) (cos * (b3 ^ ))) & b2 = #Z 2 & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = b4 & b3 . b4 <> 0 ) ) holds
( b2 (#) (cos * (b3 ^ )) is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
((b2 (#) (cos * (b3 ^ ))) `| b1) . b4 = ((2 * b4) * (cos . (1 / b4))) + (sin . (1 / b4)) ) )
proof end;

theorem Th19: :: FDIFF_5:19
for b1 being open Subset of REAL
for b2 being PartFunc of REAL , REAL st b1 c= dom ((log_ number_e ) * b2) & ( for b3 being Real st b3 in b1 holds
( b2 . b3 = b3 & b2 . b3 > 0 ) ) holds
( (log_ number_e ) * b2 is_differentiable_on b1 & ( for b3 being Real st b3 in b1 holds
(((log_ number_e ) * b2) `| b1) . b3 = 1 / b3 ) )
proof end;

theorem Th20: :: FDIFF_5:20
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom ((id b1) (#) b2) & b2 = (log_ number_e ) * b3 & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = b4 & b3 . b4 > 0 ) ) holds
( (id b1) (#) b2 is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
(((id b1) (#) b2) `| b1) . b4 = 1 + ((log_ number_e ) . b4) ) )
proof end;

theorem Th21: :: FDIFF_5:21
for b1 being open Subset of REAL
for b2, b3, b4 being PartFunc of REAL , REAL st b1 c= dom (b2 (#) b3) & b2 = #Z 2 & b3 = (log_ number_e ) * b4 & ( for b5 being Real st b5 in b1 holds
( b4 . b5 = b5 & b4 . b5 > 0 ) ) holds
( b2 (#) b3 is_differentiable_on b1 & ( for b5 being Real st b5 in b1 holds
((b2 (#) b3) `| b1) . b5 = b5 + ((2 * b5) * ((log_ number_e ) . b5)) ) )
proof end;

theorem Th22: :: FDIFF_5:22
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((b3 + b4) / (b3 - b4)) & ( for b5 being Real st b5 in b2 holds
b3 . b5 = b1 ) & b4 = #Z 2 & ( for b5 being Real st b5 in b2 holds
(b3 - b4) . b5 > 0 ) holds
( (b3 + b4) / (b3 - b4) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((b3 + b4) / (b3 - b4)) `| b2) . b5 = ((4 * b1) * b5) / ((b1 - (b5 |^ 2)) |^ 2) ) )
proof end;

theorem Th23: :: FDIFF_5:23
for b1 being Real
for b2 being open Subset of REAL
for b3, b4 being PartFunc of REAL , REAL st b2 c= dom ((log_ number_e ) * ((b3 + b4) / (b3 - b4))) & ( for b5 being Real st b5 in b2 holds
b3 . b5 = b1 ) & b4 = #Z 2 & ( for b5 being Real st b5 in b2 holds
(b3 - b4) . b5 > 0 ) & ( for b5 being Real st b5 in b2 holds
(b3 + b4) . b5 > 0 ) holds
( (log_ number_e ) * ((b3 + b4) / (b3 - b4)) is_differentiable_on b2 & ( for b5 being Real st b5 in b2 holds
(((log_ number_e ) * ((b3 + b4) / (b3 - b4))) `| b2) . b5 = ((4 * b1) * b5) / ((b1 |^ 2) - (b5 |^ 4)) ) )
proof end;

theorem Th24: :: FDIFF_5:24
for b1 being open Subset of REAL
for b2, b3, b4 being PartFunc of REAL , REAL st b1 c= dom ((b2 ^ ) (#) b3) & ( for b5 being Real st b5 in b1 holds
b2 . b5 = b5 ) & b3 = (log_ number_e ) * b4 & ( for b5 being Real st b5 in b1 holds
( b4 . b5 = b5 & b4 . b5 > 0 ) ) holds
( (b2 ^ ) (#) b3 is_differentiable_on b1 & ( for b5 being Real st b5 in b1 holds
(((b2 ^ ) (#) b3) `| b1) . b5 = (1 / (b5 ^2 )) * (1 - ((log_ number_e ) . b5)) ) )
proof end;

theorem Th25: :: FDIFF_5:25
for b1 being open Subset of REAL
for b2, b3 being PartFunc of REAL , REAL st b1 c= dom (b2 ^ ) & b2 = (log_ number_e ) * b3 & ( for b4 being Real st b4 in b1 holds
( b3 . b4 = b4 & b3 . b4 > 0 ) ) & ( for b4 being Real st b4 in b1 holds
b2 . b4 <> 0 ) holds
( b2 ^ is_differentiable_on b1 & ( for b4 being Real st b4 in b1 holds
((b2 ^ ) `| b1) . b4 = - (1 / (b4 * (((log_ number_e ) . b4) ^2 ))) ) )
proof end;