environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, ARYTM_1, SIN_COS, RELAT_1, SQUARE_1, ARYTM_3, FUNCT_1, XXREAL_0, CARD_1, PREPOWER, POWER, TARSKI, FDIFF_1, VALUED_1, NEWTON, XBOOLE_0, TAYLOR_1, ORDINAL4, COMPLEX1, LIMFUNC1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, LIMFUNC1, RCOMP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, VALUED_1, FDIFF_1, NEWTON, INT_2, PREPOWER, POWER, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1;
definitions ;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_1, FUNCT_1, TARSKI, PREPOWER, RFUNCT_1, SQUARE_1, XREAL_1, XCMPLX_0, NEWTON, SIN_COS, SIN_COS2, WSIERP_1, FDIFF_4, POWER, ABSVALUE, VALUED_1;
schemes ;
registrations ORDINAL1, RELSET_1, XXREAL_0, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0, NEWTON, SIN_COS, SQUARE_1, PREPOWER;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, LIMFUNC1, FDIFF_1, PREPOWER, POWER, SIN_COS, TAYLOR_1, VALUED_1, RELSET_1, NEWTON;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, TAYLOR_1, VALUED_1;
expansions ;
Lm1:
for x being Real holds 1 - (cos (2 * x)) = 2 * ((sin x) ^2)
Lm2:
for x being Real holds 1 + (cos (2 * x)) = 2 * ((cos x) ^2)
Lm3:
for x being Real st sin . x > 0 holds
sin . x = ((1 - (cos . x)) * (1 + (cos . x))) #R (1 / 2)
Lm4:
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)
Lm5:
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)
Lm6:
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) ) )
Lm7:
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)) ) )