environ
vocabularies HIDDEN, REAL_1, SUBSET_1, NUMBERS, RCOMP_1, PARTFUN1, TARSKI, RELAT_1, ARYTM_3, FUNCT_1, PREPOWER, FDIFF_1, XBOOLE_0, CARD_1, ARYTM_1, NEWTON, LIMFUNC1, XXREAL_0, SQUARE_1, ORDINAL4, SIN_COS, VALUED_1, TAYLOR_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, PARTFUN2, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, RCOMP_1, REAL_1, VALUED_1, FDIFF_1, NEWTON, PREPOWER, TAYLOR_1, LIMFUNC1, SIN_COS, RFUNCT_1, SQUARE_1;
definitions TARSKI;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, NAT_1, FDIFF_1, FUNCT_1, TARSKI, PREPOWER, RFUNCT_1, XREAL_1, XCMPLX_0, NEWTON, SIN_COS, VALUED_1, XXREAL_1, RELAT_1;
schemes ;
registrations RELSET_1, NUMBERS, NAT_1, INT_1, MEMBERED, RCOMP_1, VALUED_0, XXREAL_0, XREAL_0, PREPOWER, NEWTON, SQUARE_1;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, FDIFF_1, PREPOWER, SIN_COS, TAYLOR_1, VALUED_1, LIMFUNC1, XXREAL_2, RELSET_1, NEWTON;
requirements HIDDEN, SUBSET, NUMERALS, ARITHM, BOOLE;
equalities SQUARE_1, LIMFUNC1;
expansions TARSKI;
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 ) )
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) ) )
Lm3:
for Z being open Subset of REAL st Z c= dom (#R (1 / 2)) holds
( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds
((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) )
Lm4:
for Z being open Subset of REAL st not 0 in Z holds
dom (sin * ((id Z) ^)) = Z
Lm5:
for x being Real st x in dom ln holds
x > 0
by TAYLOR_1:18, XXREAL_1:4;