let a, b, c, d, r, s be Real; for f being Function of REAL,REAL st a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) holds
centroid (f,['a,d']) = ((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + ((c - b) * (((((s - r) / (c - b)) * (c + b)) / 2) + (s - ((c * (s - r)) / (c - b)))))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c))))))
let f be Function of REAL,REAL; ( a < b & b < c & c < d & f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.]) implies centroid (f,['a,d']) = ((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + ((c - b) * (((((s - r) / (c - b)) * (c + b)) / 2) + (s - ((c * (s - r)) / (c - b)))))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c)))))) )
assume that
A1:
( a < b & b < c & c < d )
and
A3:
f | [.a,d.] = (((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))) | [.a,b.]) +* ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))) | [.b,c.])) +* ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))) | [.c,d.])
; centroid (f,['a,d']) = ((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + ((c - b) * (((((s - r) / (c - b)) * (c + b)) / 2) + (s - ((c * (s - r)) / (c - b)))))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c))))))
centroid (f,['a,d']) =
(integral (((id REAL) (#) f),['a,d'])) / (integral (f,['a,d']))
by FUZZY_6:def 1
.=
(((integral (((id REAL) (#) (AffineMap ((r / (b - a)),(- ((a * r) / (b - a)))))),['a,b'])) + (integral (((id REAL) (#) (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))))),['b,c']))) + (integral (((id REAL) (#) (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))))),['c,d']))) / (integral (f,['a,d']))
by Th23, A1, A3
.=
(((integral (((id REAL) (#) (AffineMap ((r / (b - a)),(- ((a * r) / (b - a)))))),['a,b'])) + (integral (((id REAL) (#) (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))))),['b,c']))) + (integral (((id REAL) (#) (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))))),['c,d']))) / (((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])))
by Th24, A1, A3
.=
((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + (integral (((id REAL) (#) (AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b)))))),['b,c']))) + (integral (((id REAL) (#) (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))))),['c,d']))) / (((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])))
by Th4, A1
.=
((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + (integral (((id REAL) (#) (AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c)))))),['c,d']))) / (((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])))
by Th4, A1
.=
((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / (((integral ((AffineMap ((r / (b - a)),(- ((a * r) / (b - a))))),['a,b'])) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])))
by Th4, A1
.=
((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + (integral ((AffineMap (((- s) / (d - c)),(- ((d * (- s)) / (d - c))))),['c,d'])))
by Th4, A1
.=
((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + (integral ((AffineMap (((s - r) / (c - b)),(s - ((c * (s - r)) / (c - b))))),['b,c']))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c))))))
by Th4, A1
;
hence
centroid (f,['a,d']) = ((((b - a) * ((((r / (b - a)) * (((b * b) + (b * a)) + (a * a))) / 3) + (((- ((a * r) / (b - a))) * (b + a)) / 2))) + ((c - b) * (((((s - r) / (c - b)) * (((c * c) + (c * b)) + (b * b))) / 3) + (((s - ((c * (s - r)) / (c - b))) * (c + b)) / 2)))) + ((d - c) * (((((- s) / (d - c)) * (((d * d) + (d * c)) + (c * c))) / 3) + (((- ((d * (- s)) / (d - c))) * (d + c)) / 2)))) / ((((b - a) * ((((r / (b - a)) * (b + a)) / 2) + (- ((a * r) / (b - a))))) + ((c - b) * (((((s - r) / (c - b)) * (c + b)) / 2) + (s - ((c * (s - r)) / (c - b)))))) + ((d - c) * (((((- s) / (d - c)) * (d + c)) / 2) + (- ((d * (- s)) / (d - c))))))
by Th4, A1; verum