:: FDIFF_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) )
proof end;

Lm2: for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom (f1 - f2) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 holds
( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 - f2) `| Z) . x = - (2 * x) ) )
proof end;

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

theorem :: FDIFF_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2 ) ) )
proof end;

theorem :: FDIFF_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2 ) ) )
proof end;

theorem :: FDIFF_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2 ) ) )
proof end;

theorem Th4: :: FDIFF_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 = x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^ ) `| Z) . x = - (1 / (x ^2 )) ) )
proof end;

theorem Th5: :: FDIFF_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom (sin * (f ^ )) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( sin * (f ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (f ^ )) `| Z) . x = - ((1 / (x ^2 )) * (cos . (1 / x))) ) )
proof end;

theorem Th6: :: FDIFF_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom (cos * (f ^ )) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( cos * (f ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (f ^ )) `| Z) . x = (1 / (x ^2 )) * (sin . (1 / x)) ) )
proof end;

theorem :: FDIFF_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((id Z) (#) (sin * (f ^ ))) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( (id Z) (#) (sin * (f ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (sin * (f ^ ))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) )
proof end;

theorem :: FDIFF_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((id Z) (#) (cos * (f ^ ))) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( (id Z) (#) (cos * (f ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (cos * (f ^ ))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) )
proof end;

theorem :: FDIFF_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((sin * (f ^ )) (#) (cos * (f ^ ))) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( (sin * (f ^ )) (#) (cos * (f ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * (f ^ )) (#) (cos * (f ^ ))) `| Z) . x = (1 / (x ^2 )) * (((sin . (1 / x)) ^2 ) - ((cos . (1 / x)) ^2 )) ) )
proof end;

theorem :: FDIFF_5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) )
proof end;

theorem :: FDIFF_5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * sin )) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
proof end;

theorem :: FDIFF_5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (cos * f) (#) ((#Z n) * cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((cos * f) (#) ((#Z n) * cos )) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) )
proof end;

theorem :: FDIFF_5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos )) & n >= 1 & ( for x being Real st x in Z holds
f . x = n * x ) holds
( (sin * f) (#) ((#Z n) * cos ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((sin * f) (#) ((#Z n) * cos )) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) )
proof end;

theorem :: FDIFF_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((f ^ ) (#) sin ) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( (f ^ ) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
(((f ^ ) (#) sin ) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2 )) * (sin . x)) ) )
proof end;

theorem :: FDIFF_5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((f ^ ) (#) cos ) & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( (f ^ ) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((f ^ ) (#) cos ) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2 )) * (cos . x)) ) )
proof end;

theorem :: FDIFF_5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom (sin + ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = x & f . x > 0 ) ) holds
( sin + ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + ((#R (1 / 2)) * f)) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) )
proof end;

theorem :: FDIFF_5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for g, f being PartFunc of REAL , REAL st Z c= dom (g (#) (sin * (f ^ ))) & g = #Z 2 & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( g (#) (sin * (f ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (sin * (f ^ ))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) )
proof end;

theorem :: FDIFF_5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for g, f being PartFunc of REAL , REAL st Z c= dom (g (#) (cos * (f ^ ))) & g = #Z 2 & ( for x being Real st x in Z holds
( f . x = x & f . x <> 0 ) ) holds
( g (#) (cos * (f ^ )) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (cos * (f ^ ))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) )
proof end;

theorem Th19: :: FDIFF_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f being PartFunc of REAL , REAL st Z c= dom ((log_ number_e ) * f) & ( for x being Real st x in Z holds
( f . x = x & f . x > 0 ) ) holds
( (log_ number_e ) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * f) `| Z) . x = 1 / x ) )
proof end;

theorem :: FDIFF_5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) (#) f) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x & f1 . x > 0 ) ) holds
( (id Z) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) f) `| Z) . x = 1 + ((log_ number_e ) . x) ) )
proof end;

theorem :: FDIFF_5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for g, f, f1 being PartFunc of REAL , REAL st Z c= dom (g (#) f) & g = #Z 2 & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x & f1 . x > 0 ) ) holds
( g (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) f) `| Z) . x = x + ((2 * x) * ((log_ number_e ) . x)) ) )
proof end;

theorem Th22: :: FDIFF_5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) holds
( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) )
proof end;

theorem :: FDIFF_5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL , REAL st Z c= dom ((log_ number_e ) * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds
f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds
(f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds
(f1 + f2) . x > 0 ) holds
( (log_ number_e ) * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) )
proof end;

theorem :: FDIFF_5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f, g, f1 being PartFunc of REAL , REAL st Z c= dom ((f ^ ) (#) g) & ( for x being Real st x in Z holds
f . x = x ) & g = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x & f1 . x > 0 ) ) holds
( (f ^ ) (#) g is_differentiable_on Z & ( for x being Real st x in Z holds
(((f ^ ) (#) g) `| Z) . x = (1 / (x ^2 )) * (1 - ((log_ number_e ) . x)) ) )
proof end;

theorem :: FDIFF_5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Z being open Subset of REAL
for f, f1 being PartFunc of REAL , REAL st Z c= dom (f ^ ) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x & f1 . x > 0 ) ) & ( for x being Real st x in Z holds
f . x <> 0 ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^ ) `| Z) . x = - (1 / (x * (((log_ number_e ) . x) ^2 ))) ) )
proof end;