let a, b, c be Real; for f being Function of REAL,REAL st b > 0 & c > 0 & f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]) holds
centroid (f,['(a - c),(a + c)']) = a
let f be Function of REAL,REAL; ( b > 0 & c > 0 & f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).]) implies centroid (f,['(a - c),(a + c)']) = a )
assume that
A1:
b > 0
and
A2:
c > 0
and
A3:
f | ['(a - c),(a + c)'] = ((AffineMap ((b / c),(b - ((a * b) / c)))) | [.(lower_bound ['(a - c),(a + c)']),(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))).]) +* ((AffineMap ((- (b / c)),(b + ((a * b) / c)))) | [.(((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c)))),(upper_bound ['(a - c),(a + c)']).])
; centroid (f,['(a - c),(a + c)']) = a
set s = b / c;
set d = b - ((a * b) / c);
set p = - (b / c);
set q = b + ((a * b) / c);
set C = ['(a - c),(a + c)'];
A7: ((b + ((a * b) / c)) - (b - ((a * b) / c))) / ((b / c) - (- (b / c))) =
(((b + ((a * b) / c)) - b) + ((a * b) / c)) / ((b / c) + (b / c))
.=
(((a * b) / c) + (a * (b / c))) / ((b / c) + (b / c))
by XCMPLX_1:74
.=
((a * (b / c)) + (a * (b / c))) / ((b / c) + (b / c))
by XCMPLX_1:74
.=
(a * ((b / c) + (b / c))) / ((b / c) + (b / c))
.=
a * (((b / c) + (b / c)) / ((b / c) + (b / c)))
by XCMPLX_1:74
.=
a
by XCMPLX_1:88, A1, A2
;
A10:
( a - c <= a & a <= a + c )
by XREAL_1:43, XREAL_1:29, A2;
( [.(lower_bound ['(a - c),(a + c)']),(upper_bound ['(a - c),(a + c)']).] = ['(a - c),(a + c)'] & ['(a - c),(a + c)'] = [.(a - c),(a + c).] )
by A10, INTEGRA5:def 3, INTEGRA1:4, XXREAL_0:2;
then A8:
( lower_bound ['(a - c),(a + c)'] = a - c & a + c = upper_bound ['(a - c),(a + c)'] )
by INTEGRA1:5;
Dd: b - ((a * b) / c) =
((b * c) - (a * b)) / c
by XCMPLX_1:127, A2
.=
((c - a) * b) / c
.=
(b / c) * (c - a)
by XCMPLX_1:74
;
Qq: b + ((a * b) / c) =
((a * b) + (b * c)) / c
by XCMPLX_1:113, A2
.=
(b * (a + c)) / c
.=
(b / c) * (a + c)
by XCMPLX_1:74
;
CE: centroid (f,['(a - c),(a + c)']) =
((((((1 / 3) * (b / c)) * ((a ^3) - ((lower_bound ['(a - c),(a + c)']) ^3))) + (((1 / 2) * (b - ((a * b) / c))) * ((a ^2) - ((lower_bound ['(a - c),(a + c)']) ^2)))) + (((1 / 3) * (- (b / c))) * (((upper_bound ['(a - c),(a + c)']) ^3) - (a ^3)))) + (((1 / 2) * (b + ((a * b) / c))) * (((upper_bound ['(a - c),(a + c)']) ^2) - (a ^2)))) / ((((((1 / 2) * (b / c)) * ((a ^2) - ((lower_bound ['(a - c),(a + c)']) ^2))) + ((b - ((a * b) / c)) * (a - (lower_bound ['(a - c),(a + c)'])))) + (((1 / 2) * (- (b / c))) * (((upper_bound ['(a - c),(a + c)']) ^2) - (a ^2)))) + ((b + ((a * b) / c)) * ((upper_bound ['(a - c),(a + c)']) - a)))
by FUZZY_6:48, A3, A7, Lm6, A2, A1
.=
((((((1 / 3) * (b / c)) * ((a ^3) - ((a - c) ^3))) + (((1 / 2) * (b - ((a * b) / c))) * ((a - (a - c)) * (a + (a - c))))) + (((1 / 3) * (- (b / c))) * (((a + c) ^3) - (a ^3)))) + (((1 / 2) * (b + ((a * b) / c))) * (((a + c) - a) * ((a + c) + a)))) / ((((((1 / 2) * (b / c)) * ((a - (a - c)) * (a + (a - c)))) + ((b - ((a * b) / c)) * c)) + (((1 / 2) * (- (b / c))) * (((a + c) - a) * ((a + c) + a)))) + ((b + ((a * b) / c)) * c))
by A8
;
B1: (((((1 / 3) * (b / c)) * ((a ^3) - ((a - c) ^3))) + (((1 / 2) * (b - ((a * b) / c))) * (c * ((a + a) - c)))) + (((1 / 3) * (- (b / c))) * (((a + c) ^3) - (a ^3)))) + (((1 / 2) * (b + ((a * b) / c))) * (c * ((a + c) + a))) =
(((((1 / 3) * (b / c)) * ((a ^3) - ((a - c) ^3))) + (((1 / 2) * (b - ((a * b) / c))) * (c * ((a + a) - c)))) + (((1 / 3) * (- (b / c))) * (((a + c) |^ 3) - (a ^3)))) + (((1 / 2) * (b + ((a * b) / c))) * (c * ((a + c) + a)))
by POLYEQ_3:27
.=
(((((1 / 3) * (b / c)) * ((a ^3) - ((a - c) |^ 3))) + (((1 / 2) * (b - ((a * b) / c))) * (c * ((a + a) - c)))) + (((1 / 3) * (- (b / c))) * (((a + c) |^ 3) - (a ^3)))) + (((1 / 2) * (b + ((a * b) / c))) * (c * ((a + c) + a)))
by POLYEQ_3:27
.=
(((((1 / 3) * (b / c)) * ((a ^3) - (((a - c) ^2) * (a - c)))) + ((((1 / 2) * c) * (b - ((a * b) / c))) * ((a + a) - c))) + (((1 / 3) * (- (b / c))) * (((a + c) |^ 3) - (a ^3)))) + ((((1 / 2) * c) * (b + ((a * b) / c))) * ((a + c) + a))
by POLYEQ_3:27
.=
(((((1 / 3) * (b / c)) * ((a ^3) - (((a - c) ^2) * (a - c)))) + ((((1 / 2) * c) * ((b / c) * (c - a))) * ((a + a) - c))) + ((((1 / 3) * (b / c)) * (- 1)) * (((a + c) |^ 3) - (a ^3)))) + ((((1 / 2) * c) * ((b / c) * (a + c))) * ((a + c) + a))
by Qq, Dd
.=
(((1 / 3) * (b / c)) * (((a ^3) - (((a - c) ^2) * (a - c))) + ((- 1) * (((a + c) |^ 3) - (a ^3))))) + ((((1 / 2) * c) * (b / c)) * (((a + c) * ((2 * a) + c)) + ((c - a) * ((2 * a) - c))))
.=
(((1 / 3) * (b / c)) * (((a ^3) - ((((a ^2) - ((2 * a) * c)) + (c ^2)) * (a - c))) + ((- 1) * ((((a + c) ^2) * (a + c)) - (a ^3))))) + ((((1 / 2) * c) * (b / c)) * (((((a * (2 * a)) + (a * c)) + (c * (2 * a))) + (c * c)) + ((((c * (2 * a)) - (c * c)) - (a * (2 * a))) + (a * c))))
by POLYEQ_3:27
.=
(((1 / 3) * (b / c)) * (((a ^3) - (((((((a ^2) * a) - ((a ^2) * c)) - (((2 * a) * c) * a)) + (((2 * a) * c) * c)) + ((c ^2) * a)) - ((c ^2) * c))) + ((- 1) * ((((((((a ^2) * a) + ((a ^2) * c)) + (((2 * a) * c) * a)) + (((2 * a) * c) * c)) + ((c ^2) * a)) + ((c ^2) * c)) - (a ^3))))) + (((1 / 2) * (c * (b / c))) * ((6 * a) * c))
.=
(((1 / 3) * (b / c)) * (((a ^3) - (((((((a ^2) * a) - ((a ^2) * c)) - (((2 * a) * c) * a)) + (((2 * a) * c) * c)) + ((c ^2) * a)) - ((c ^2) * c))) + ((- 1) * ((((((((a ^2) * a) + ((a ^2) * c)) + (((2 * a) * c) * a)) + (((2 * a) * c) * c)) + ((c ^2) * a)) + ((c ^2) * c)) - (a ^3))))) + (((1 / 2) * ((c * b) / c)) * ((6 * a) * c))
by XCMPLX_1:74
.=
(((1 / 3) * (b / c)) * ((((((((a ^3) - ((a ^2) * a)) + ((a ^2) * c)) + (((2 * a) * c) * a)) - (((2 * a) * c) * c)) - ((c ^2) * a)) + ((c ^2) * c)) + (((((((((- 1) * (a ^2)) * a) + (((- 1) * (a ^2)) * c)) + (((((- 1) * 2) * a) * c) * a)) + (((((- 1) * 2) * a) * c) * c)) + (((- 1) * (c ^2)) * a)) + (((- 1) * (c ^2)) * c)) - ((- 1) * (a ^3))))) + (((1 / 2) * b) * ((6 * a) * c))
by XCMPLX_1:89, A2
.=
(((1 / 3) * (b / c)) * (((((((((a ^3) - ((a ^2) * a)) + ((a * a) * c)) - (((4 * a) * c) * c)) - ((c ^2) * a)) - ((a ^2) * a)) + (- ((a ^2) * c))) - ((c ^2) * a)) + (- (- (a ^3))))) + (((((1 / 2) * 6) * b) * a) * c)
.=
(((1 / 3) * (b / c)) * (((((((((a ^3) - ((a ^2) * a)) + ((a * a) * c)) - (((4 * a) * c) * c)) - ((c ^2) * a)) - (a ^3)) + (- ((a ^2) * c))) - ((c ^2) * a)) + (- (- (a ^3))))) + (((((1 / 2) * 6) * b) * a) * c)
by POLYEQ_3:def 3
.=
(((1 / 3) * (b / c)) * (((((((- ((a ^2) * a)) + ((a * a) * c)) - (((4 * a) * c) * c)) - ((c ^2) * a)) - ((a ^2) * c)) - ((c ^2) * a)) + (a ^3))) + (((3 * b) * a) * c)
.=
(((1 / 3) * (b / c)) * (((((((- (a ^3)) + ((a * a) * c)) - (((4 * a) * c) * c)) - ((c ^2) * a)) - ((a ^2) * c)) - ((c ^2) * a)) + (a ^3))) + (((3 * b) * a) * c)
by POLYEQ_3:def 3
.=
(((((- 6) * (1 / 3)) * ((b / c) * c)) * a) * c) + (((3 * b) * a) * c)
.=
(((((- 6) * (1 / 3)) * ((c * b) / c)) * a) * c) + (((3 * b) * a) * c)
by XCMPLX_1:74
.=
(((((- 6) * (1 / 3)) * b) * a) * c) + (((3 * b) * a) * c)
by XCMPLX_1:89, A2
.=
a * (b * c)
;
(((((1 / 2) * (b / c)) * ((a - (a - c)) * (a + (a - c)))) + ((b - ((a * b) / c)) * c)) + (((1 / 2) * (- (b / c))) * (((a + c) - a) * ((a + c) + a)))) + ((b + ((a * b) / c)) * c) =
(((((1 / 2) * ((b / c) * c)) * ((2 * a) - c)) - (((1 / 2) * ((b / c) * c)) * ((2 * a) + c))) + (((b / c) * c) * (c - a))) + (((b / c) * c) * (c + a))
by Dd, Qq
.=
(((((1 / 2) * ((b / c) * c)) * ((2 * a) - c)) - (((1 / 2) * ((b / c) * c)) * ((2 * a) + c))) + (((b * c) / c) * (c - a))) + (((b / c) * c) * (c + a))
by XCMPLX_1:74
.=
(((((1 / 2) * ((b / c) * c)) * ((2 * a) - c)) - (((1 / 2) * ((b / c) * c)) * ((2 * a) + c))) + (b * (c - a))) + (((b / c) * c) * (c + a))
by XCMPLX_1:89, A2
.=
(((((1 / 2) * ((b * c) / c)) * ((2 * a) - c)) - (((1 / 2) * ((b / c) * c)) * ((2 * a) + c))) + (b * (c - a))) + (((b / c) * c) * (c + a))
by XCMPLX_1:74
.=
(((((1 / 2) * ((b * c) / c)) * ((2 * a) - c)) - (((1 / 2) * ((b * c) / c)) * ((2 * a) + c))) + (b * (c - a))) + (((b / c) * c) * (c + a))
by XCMPLX_1:74
.=
(((((1 / 2) * ((b * c) / c)) * ((2 * a) - c)) - (((1 / 2) * ((b * c) / c)) * ((2 * a) + c))) + (b * (c - a))) + (((b * c) / c) * (c + a))
by XCMPLX_1:74
.=
(((((1 / 2) * ((b * c) / c)) * ((2 * a) - c)) - (((1 / 2) * ((b * c) / c)) * ((2 * a) + c))) + (b * (c - a))) + (b * (c + a))
by XCMPLX_1:89, A2
.=
(((((1 / 2) * ((b * c) / c)) * ((2 * a) - c)) - (((1 / 2) * b) * ((2 * a) + c))) + (b * (c - a))) + (b * (c + a))
by XCMPLX_1:89, A2
.=
(((((1 / 2) * b) * ((2 * a) - c)) - (((1 / 2) * b) * ((2 * a) + c))) + (b * (c - a))) + (b * (c + a))
by XCMPLX_1:89, A2
.=
b * c
;
hence
centroid (f,['(a - c),(a + c)']) = a
by XCMPLX_1:89, A1, A2, CE, B1; verum