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

theorem Th1: :: FDIFF_4: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 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 = a + 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 / (a + x) ) )
proof end;

theorem Th2: :: FDIFF_4: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 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 - a & 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 - a) ) )
proof end;

theorem :: FDIFF_4:3  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 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 = a - 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 / (a - x) ) )
proof end;

theorem :: FDIFF_4:4  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 f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) - (a (#) f)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) holds
( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) )
proof end;

theorem :: FDIFF_4:5  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 f, f1 being PartFunc of REAL , REAL st Z c= dom (((2 * a) (#) f) - (id Z)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 ) ) holds
( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) )
proof end;

theorem :: FDIFF_4:6  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 f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) - ((2 * a) (#) f)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x + a & f1 . x > 0 ) ) holds
( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) )
proof end;

theorem :: FDIFF_4:7  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 f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) + ((2 * a) (#) f)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 ) ) holds
( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) )
proof end;

theorem :: FDIFF_4:8  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 f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) + ((a - b) (#) f)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) holds
( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) )
proof end;

theorem :: FDIFF_4:9  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 f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) + ((a + b) (#) f)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x - b & f1 . x > 0 ) ) holds
( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) )
proof end;

theorem :: FDIFF_4:10  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 f, f1 being PartFunc of REAL , REAL st Z c= dom ((id Z) - ((a + b) (#) f)) & f = (log_ number_e ) * f1 & ( for x being Real st x in Z holds
( f1 . x = x + b & f1 . x > 0 ) ) holds
( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) )
proof end;

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

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

theorem Th13: :: FDIFF_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c, a, b 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 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) holds
( (log_ number_e ) * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) )
proof end;

theorem Th14: :: FDIFF_4:14  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 f being PartFunc of REAL , REAL st Z c= dom f & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^ ) `| Z) . x = - (1 / ((a + x) ^2 )) ) )
proof end;

theorem :: FDIFF_4:15  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 f being PartFunc of REAL , REAL st Z c= dom ((- 1) (#) (f ^ )) & ( for x being Real st x in Z holds
( f . x = a + x & f . x <> 0 ) ) holds
( (- 1) (#) (f ^ ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 1) (#) (f ^ )) `| Z) . x = 1 / ((a + x) ^2 ) ) )
proof end;

theorem :: FDIFF_4:16  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 f being PartFunc of REAL , REAL st Z c= dom f & ( for x being Real st x in Z holds
( f . x = a - x & f . x <> 0 ) ) holds
( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((f ^ ) `| Z) . x = 1 / ((a - x) ^2 ) ) )
proof end;

theorem Th17: :: FDIFF_4:17  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 ^2 ) & 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;

theorem :: FDIFF_4:18  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)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) holds
( (log_ number_e ) * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2 ) + (x |^ 2)) ) )
proof end;

theorem :: FDIFF_4:19  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))) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) holds
( - ((log_ number_e ) * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
((- ((log_ number_e ) * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2 ) - (x |^ 2)) ) )
proof end;

theorem Th20: :: FDIFF_4:20  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 ) & f2 = #Z 3 holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) )
proof end;

theorem :: FDIFF_4:21  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)) & f2 = #Z 3 & ( for x being Real st x in Z holds
( f1 . x = a & (f1 + f2) . x > 0 ) ) holds
( (log_ number_e ) * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) )
proof end;

theorem :: FDIFF_4: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 ((log_ number_e ) * (f1 / f2)) & ( for x being Real st x in Z holds
( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) holds
( (log_ number_e ) * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2 ) - (x ^2 )) ) )
proof end;

theorem :: FDIFF_4: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)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) holds
( (log_ number_e ) * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2 ) - (a ^2 )) ) )
proof end;

theorem Th24: :: FDIFF_4:24  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 ((log_ number_e ) * (f1 / f2)) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds
( (log_ number_e ) * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) )
proof end;

theorem :: FDIFF_4:25  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 f, f1, f2 being PartFunc of REAL , REAL st Z c= dom ((1 / (a - b)) (#) f) & f = (log_ number_e ) * (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) holds
( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) )
proof end;

theorem :: FDIFF_4:26  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)) & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds
( (log_ number_e ) * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) )
proof end;

theorem Th27: :: FDIFF_4:27  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 f being PartFunc of REAL , REAL st Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds
(((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) )
proof end;

theorem :: FDIFF_4:28  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 f being PartFunc of REAL , REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) )
proof end;

theorem :: FDIFF_4:29  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 f being PartFunc of REAL , REAL st Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) )
proof end;

theorem :: FDIFF_4:30  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 f being PartFunc of REAL , REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a + x & f . x > 0 ) ) holds
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) )
proof end;

theorem :: FDIFF_4:31  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 f being PartFunc of REAL , REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds
( f . x = a - x & f . x > 0 ) ) holds
( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) )
proof end;

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

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

theorem :: FDIFF_4:34  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 f, f1, f2 being PartFunc of REAL , REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & 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 = x * (((a ^2 ) + (x |^ 2)) #R (- (1 / 2))) ) )
proof end;

theorem :: FDIFF_4:35  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 f, f1, f2 being PartFunc of REAL , REAL st Z c= dom (- ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = a ^2 & 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 = x * (((a ^2 ) - (x |^ 2)) #R (- (1 / 2))) ) )
proof end;

theorem :: FDIFF_4:36  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, f2 being PartFunc of REAL , REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds
( f1 . x = x & f . x > 0 ) ) holds
( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) )
proof end;

theorem :: FDIFF_4:37  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 f being PartFunc of REAL , REAL st Z c= dom (sin * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) )
proof end;

theorem :: FDIFF_4:38  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 f being PartFunc of REAL , REAL st Z c= dom (cos * f) & ( for x being Real st x in Z holds
f . x = (a * x) + b ) holds
( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) )
proof end;

theorem :: FDIFF_4:39  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 st ( for x being Real st x in Z holds
cos . x <> 0 ) holds
( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((cos ^ ) `| Z) . x = (sin . x) / ((cos . x) ^2 ) ) )
proof end;

theorem :: FDIFF_4:40  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 st ( for x being Real st x in Z holds
sin . x <> 0 ) holds
( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds
((sin ^ ) `| Z) . x = - ((cos . x) / ((sin . x) ^2 )) ) )
proof end;

theorem :: FDIFF_4:41  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 st Z c= dom (sin (#) cos ) holds
( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) cos ) `| Z) . x = cos (2 * x) ) )
proof end;

theorem :: FDIFF_4:42  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 st Z c= dom ((log_ number_e ) * cos ) & ( for x being Real st x in Z holds
cos . x > 0 ) holds
( (log_ number_e ) * cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * cos ) `| Z) . x = - (tan x) ) )
proof end;

theorem :: FDIFF_4:43  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 st Z c= dom ((log_ number_e ) * sin ) & ( for x being Real st x in Z holds
sin . x > 0 ) holds
( (log_ number_e ) * sin is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * sin ) `| Z) . x = cot x ) )
proof end;

theorem Th44: :: FDIFF_4:44  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 st Z c= dom ((- (id Z)) (#) cos ) holds
( (- (id Z)) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (id Z)) (#) cos ) `| Z) . x = (- (cos . x)) + (x * (sin . x)) ) )
proof end;

theorem Th45: :: FDIFF_4:45  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 st Z c= dom ((id Z) (#) sin ) holds
( (id Z) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) sin ) `| Z) . x = (sin . x) + (x * (cos . x)) ) )
proof end;

theorem :: FDIFF_4:46  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 st Z c= dom (((- (id Z)) (#) cos ) + sin ) holds
( ((- (id Z)) (#) cos ) + sin is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (id Z)) (#) cos ) + sin ) `| Z) . x = x * (sin . x) ) )
proof end;

theorem :: FDIFF_4:47  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 st Z c= dom (((id Z) (#) sin ) + cos ) holds
( ((id Z) (#) sin ) + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) (#) sin ) + cos ) `| Z) . x = x * (cos . x) ) )
proof end;

theorem :: FDIFF_4:48  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 st Z c= dom (2 (#) ((#R (1 / 2)) * sin )) & ( for x being Real st x in Z holds
sin . x > 0 ) holds
( 2 (#) ((#R (1 / 2)) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * sin )) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) )
proof end;

theorem Th49: :: FDIFF_4:49  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 st Z c= dom ((1 / 2) (#) ((#Z 2) * sin )) holds
( (1 / 2) (#) ((#Z 2) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * sin )) `| Z) . x = (sin . x) * (cos . x) ) )
proof end;

theorem :: FDIFF_4:50  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 st Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin ))) & ( for x being Real st x in Z holds
( sin . x > 0 & sin . x < 1 ) ) holds
( sin + ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) )
proof end;

theorem :: FDIFF_4:51  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 st Z c= dom (((1 / 2) (#) ((#Z 2) * sin )) - cos ) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x < 1 ) ) holds
( ((1 / 2) (#) ((#Z 2) * sin )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 2) (#) ((#Z 2) * sin )) - cos ) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) )
proof end;

theorem :: FDIFF_4:52  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 st Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin ))) & ( for x being Real st x in Z holds
( sin . x > 0 & sin . x > - 1 ) ) holds
( sin - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) )
proof end;

theorem :: FDIFF_4:53  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 st Z c= dom ((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x > - 1 ) ) holds
( (- cos ) - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) )
proof end;

theorem :: FDIFF_4:54  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 st Z c= dom ((1 / n) (#) ((#Z n) * sin )) & n > 0 holds
( (1 / n) (#) ((#Z n) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * sin )) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) )
proof end;

theorem :: FDIFF_4:55  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 (exp (#) f) & ( for x being Real st x in Z holds
f . x = x - 1 ) holds
( exp (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp (#) f) `| Z) . x = x * (exp . x) ) )
proof end;

theorem :: FDIFF_4:56  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 ) * (exp / (exp + f))) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( (log_ number_e ) * (exp / (exp + f)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (exp / (exp + f))) `| Z) . x = 1 / ((exp . x) + 1) ) )
proof end;

theorem :: FDIFF_4:57  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 ) * ((exp - f) / exp )) & ( for x being Real st x in Z holds
( f . x = 1 & (exp - f) . x > 0 ) ) holds
( (log_ number_e ) * ((exp - f) / exp ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * ((exp - f) / exp )) `| Z) . x = 1 / ((exp . x) - 1) ) )
proof end;