environ
vocabularies HIDDEN, DIFF_1, ARYTM_3, ARYTM_1, FUNCT_1, NUMBERS, RELAT_1, ZFMISC_1, REAL_1, XXREAL_0, SQUARE_1, SIN_COS, VALUED_1, CARD_1, POWER, SIN_COS4, XBOOLE_0, TAYLOR_1, LIMFUNC1, NEWTON, NAT_1;
notations HIDDEN, ORDINAL1, XCMPLX_0, XREAL_0, REAL_1, NAT_1, SERIES_1, XXREAL_0, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, FUNCT_1, PARTFUN1, RELAT_1, VALUED_0, VALUED_1, FUNCOP_1, NAT_D, NEWTON, FUNCT_2, RELSET_1, SEQFUNC, SQUARE_1, SIN_COS, SIN_COS4, DIFF_1, DIFF_2, FDIFF_9, RFUNCT_1, COMPLEX1, MEMBERED, MEMBER_1, FUNCT_3, TAYLOR_1, POWER, PARTFUN2, LIMFUNC1;
definitions ;
theorems XCMPLX_1, NEWTON, RFUNCT_1, ZFMISC_1, VALUED_1, DIFF_1, SIN_COS4, FDIFF_8, XBOOLE_0, DIFF_3, XXREAL_0, SIN_COS5, TAYLOR_1, POWER, SIN_COS, XXREAL_1;
schemes NAT_1;
registrations ORDINAL1, XREAL_0, MEMBERED, VALUED_0, DIFF_1, RELSET_1, SQUARE_1, SIN_COS, XCMPLX_0, NEWTON, XXREAL_0, NAT_1;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, SEQFUNC, NEWTON, SERIES_1, MEASURE6, NAT_D, PARTFUN3, DIFF_1, FUNCOP_1, RELSET_1, DIFF_2, VALUED_2, SQUARE_1, SIN_COS, SIN_COS4, FDIFF_9, XCMPLX_0, FUNCT_1, FUNCT_3, XXREAL_0, COMPLEX1, VALUED_1, RFUNCT_1, XREAL_0, PARTFUN2, SEQ_2, SIN_COS5, TAYLOR_1, POWER, RCOMP_1, LIMFUNC1, FDIFF_1, PREPOWER;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities DIFF_1, SIN_COS4, SQUARE_1, SIN_COS, FDIFF_9, XCMPLX_0, TAYLOR_1, LIMFUNC1;
expansions ;
theorem
for
k,
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = k / (x ^2) ) &
x0 <> 0 &
x1 <> 0 &
x2 <> 0 &
x3 <> 0 &
x0,
x1,
x2,
x3 are_mutually_distinct holds
[!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3)
theorem
for
h,
x0,
x1 being
Real for
f,
g being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = (fD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!]
theorem
for
h,
x0,
x1 being
Real for
f,
g being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = (bD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!]
theorem
for
h,
x0,
x1 being
Real for
f,
g being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = (cD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]