begin
theorem Th1:
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th11:
theorem
theorem
theorem
theorem
theorem Th16:
theorem
theorem
theorem
theorem
theorem
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!]
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r (#) f1) - f2),x0,x1!] = (r * [!f1,x0,x1!]) - [!f2,x0,x1!]
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!(f1 + (r (#) f2)),x0,x1!] = [!f1,x0,x1!] + (r * [!f2,x0,x1!])
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!(f1 - (r (#) f2)),x0,x1!] = [!f1,x0,x1!] - (r * [!f2,x0,x1!])
theorem
for
r1,
r2,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])
theorem Th31:
theorem
for
x0,
x1,
x2 being
Real for
f being
Function of
REAL,
REAL st
x0,
x1,
x2 are_mutually_different holds
[!f,x0,x1,x2!] = [!f,x0,x2,x1!]
theorem
for
h,
x being
Real for
f1,
f2 being
Function of
REAL,
REAL for
S being
Seq_Sequence st ( for
n,
i being
Nat st
i <= n holds
(S . n) . i = ((n choose i) * (((bdif (f1,h)) . i) . x)) * (((bdif (f2,h)) . (n -' i)) . (x - (i * h))) ) holds
(
((bdif ((f1 (#) f2),h)) . 1) . x = Sum (
(S . 1),1) &
((bdif ((f1 (#) f2),h)) . 2) . x = Sum (
(S . 2),2) )
theorem Th34:
theorem
for
h,
x being
Real for
f1,
f2 being
Function of
REAL,
REAL for
S being
Seq_Sequence st ( for
n,
i being
Nat st
i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) holds
(
((cdif ((f1 (#) f2),h)) . 1) . x = Sum (
(S . 1),1) &
((cdif ((f1 (#) f2),h)) . 2) . x = Sum (
(S . 2),2) )
theorem
theorem
theorem
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = sqrt x ) &
x0,
x1,
x2,
x3 are_mutually_different &
x0 > 0 &
x1 > 0 &
x2 > 0 &
x3 > 0 holds
[!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
theorem
theorem
theorem
theorem
theorem
theorem
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = x ^2 ) &
x0,
x1,
x2,
x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = 0
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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem