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

Lm6: for x being Real holds 1 - (cos (2 * x)) = 2 * ((sin x) ^2 )
proof end;

Lm7: for x being Real holds 1 + (cos (2 * x)) = 2 * ((cos x) ^2 )
proof end;

Lm1: for x being Real st sin . x > 0 holds
sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2)
proof end;

Lm2: for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds
(sin . x) / ((1 - (cos . x)) #R (1 / 2)) = (1 + (cos . x)) #R (1 / 2)
proof end;

theorem th9: :: FDIFF_6:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, x being Real st a > 0 holds
exp . (x * (log number_e ,a)) = a #R x
proof end;

theorem th15: :: FDIFF_6:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, x being Real st a > 0 holds
exp . (- (x * (log number_e ,a))) = a #R (- x)
proof end;

Lm3: for x being Real st sin . x > 0 & cos . x < 1 & cos . x > - 1 holds
(sin . x) / ((1 + (cos . x)) #R (1 / 2)) = (1 - (cos . x)) #R (1 / 2)
proof end;

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

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

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

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

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

theorem :: FDIFF_6:9  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 ((log_ number_e ) * (#Z n)) & ( for x being Real st x in Z holds
x > 0 ) holds
( (log_ number_e ) * (#Z n) is_differentiable_on Z & ( for x being Real st x in Z holds
(((log_ number_e ) * (#Z n)) `| Z) . x = n / x ) )
proof end;

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

theorem th10: :: FDIFF_6:11  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 (exp * f) & ( for x being Real st x in Z holds
f . x = x * (log number_e ,a) ) & a > 0 holds
( exp * f is_differentiable_on Z & ( for x being Real st x in Z holds
((exp * f) `| Z) . x = (a #R x) * (log number_e ,a) ) )
proof end;

theorem :: FDIFF_6:12  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 ((1 / (log number_e ,a)) (#) ((exp * f1) (#) f2)) & ( for x being Real st x in Z holds
( f1 . x = x * (log number_e ,a) & f2 . x = x - (1 / (log number_e ,a)) ) ) & a > 0 & a <> 1 holds
( (1 / (log number_e ,a)) (#) ((exp * f1) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (log number_e ,a)) (#) ((exp * f1) (#) f2)) `| Z) . x = x * (a #R x) ) )
proof end;

theorem :: FDIFF_6:13  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 / (1 + (log number_e ,a))) (#) ((exp * f) (#) exp )) & ( for x being Real st x in Z holds
f . x = x * (log number_e ,a) ) & a > 0 & a <> 1 / number_e holds
( (1 / (1 + (log number_e ,a))) (#) ((exp * f) (#) exp ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (1 + (log number_e ,a))) (#) ((exp * f) (#) exp )) `| Z) . x = (a #R x) * (exp . x) ) )
proof end;

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

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

theorem th16: :: FDIFF_6: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 (- (exp * f)) & ( for x being Real st x in Z holds
f . x = - (x * (log number_e ,a)) ) & a > 0 holds
( - (exp * f) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp * f)) `| Z) . x = (a #R (- x)) * (log number_e ,a) ) )
proof end;

theorem :: FDIFF_6: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 ((1 / (log number_e ,a)) (#) ((- (exp * f1)) (#) f2)) & ( for x being Real st x in Z holds
( f1 . x = - (x * (log number_e ,a)) & f2 . x = x + (1 / (log number_e ,a)) ) ) & a > 0 & a <> 1 holds
( (1 / (log number_e ,a)) (#) ((- (exp * f1)) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (log number_e ,a)) (#) ((- (exp * f1)) (#) f2)) `| Z) . x = x / (a #R x) ) )
proof end;

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

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

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

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

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

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

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

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

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

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

theorem :: FDIFF_6:28  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 ) * (((#Z 2) * (exp - f1)) / exp ) & ( for x being Real st x in Z holds
( f1 . x = 1 & (exp - f1) . x > 0 ) ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = ((exp . x) + 1) / ((exp . x) - 1) ) )
proof end;

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

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

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

theorem :: FDIFF_6:32  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 ) * (exp / ((#Z 2) * (f1 - exp ))) & ( for x being Real st x in Z holds
( f1 . x = 1 & (f1 - exp ) . x > 0 ) ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = (1 + (exp . x)) / (1 - (exp . x)) ) )
proof end;

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

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

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

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

theorem :: FDIFF_6:37  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 / (3 * (log number_e ,a))) (#) ((#R (3 / 2)) * (f + (exp * f1)))) & ( for x being Real st x in Z holds
( f . x = 1 & f1 . x = x * (log number_e ,a) ) ) & a > 0 & a <> 1 holds
( (2 / (3 * (log number_e ,a))) (#) ((#R (3 / 2)) * (f + (exp * f1))) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / (3 * (log number_e ,a))) (#) ((#R (3 / 2)) * (f + (exp * f1)))) `| Z) . x = (a #R x) * ((1 + (a #R x)) #R (1 / 2)) ) )
proof end;

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

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

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

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

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

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

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

theorem th43: :: FDIFF_6:43  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 / (4 * a)) (#) (sin * f)) & ( for x being Real st x in Z holds
f . x = (2 * a) * x ) & a <> 0 holds
( (1 / (4 * a)) (#) (sin * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (4 * a)) (#) (sin * f)) `| Z) . x = (1 / 2) * (cos ((2 * a) * x)) ) )
proof end;

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

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

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

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

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

theorem :: FDIFF_6: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 (sin * (log_ number_e )) holds
( sin * (log_ number_e ) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (log_ number_e )) `| Z) . x = (cos . (log number_e ,x)) / x ) )
proof end;

theorem :: FDIFF_6: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 (- (cos * (log_ number_e ))) holds
( - (cos * (log_ number_e )) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (cos * (log_ number_e ))) `| Z) . x = (sin . (log number_e ,x)) / x ) )
proof end;