begin
theorem Th29:
theorem
theorem Th31:
theorem Th32:
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_different 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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
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
theorem
theorem
theorem Th43:
theorem
theorem
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
theorem
theorem
theorem Th50:
theorem
theorem
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))!]
theorem
theorem
theorem
theorem Th57:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem