let a, b, c, d be Real; ( b > 0 & c > 0 & d > 0 & d < b implies centroid ((d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))),['(a - c),(a + c)']) = a )
assume A1:
( b > 0 & c > 0 & d > 0 & d < b )
; centroid ((d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))),['(a - c),(a + c)']) = a
A5:
( d - b < b - b & b - d > d - d )
by A1, XREAL_1:9;
set a1 = a + ((d - b) / (b / c));
set a2 = a + ((b - d) / (b / c));
set c0 = (a + c) - (a + ((b - d) / (b / c)));
0 + b > (- d) + b
by XREAL_1:6, A1;
then
b / b > (b - d) / b
by A1, XREAL_1:74;
then
(b / b) * c > ((b - d) / b) * c
by A1, XREAL_1:68;
then
b / (b / c) > ((b - d) / b) * c
by XCMPLX_1:82;
then
b / (b / c) > (b - d) / (b / c)
by XCMPLX_1:82;
then A6:
(b / (b / c)) - ((b - d) / (b / c)) > ((b - d) / (b / c)) - ((b - d) / (b / c))
by XREAL_1:9;
A3: (a + c) - (a + ((b - d) / (b / c))) =
c - ((b - d) / (b / c))
.=
(b / (b / c)) - ((b - d) / (b / c))
by A1, XCMPLX_1:52
;
A4: (a + ((d - b) / (b / c))) - ((a + c) - (a + ((b - d) / (b / c)))) =
((((- (b - d)) / (b / c)) - c) + a) + ((b - d) / (b / c))
.=
(((- ((b - d) / (b / c))) - c) + a) + ((b - d) / (b / c))
by XCMPLX_1:187
.=
a - c
;
centroid ((d (#) (TrapezoidalFS (((a + ((d - b) / (b / c))) - ((a + c) - (a + ((b - d) / (b / c))))),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),((a + ((b - d) / (b / c))) + ((a + c) - (a + ((b - d) / (b / c)))))))),['((a + ((d - b) / (b / c))) - ((a + c) - (a + ((b - d) / (b / c))))),((a + ((b - d) / (b / c))) + ((a + c) - (a + ((b - d) / (b / c)))))']) =
((a + ((- (b - d)) / (b / c))) + (a + ((b - d) / (b / c)))) / 2
by FUZZY_7:50, A1, A5, A3, A6, XREAL_1:6
.=
((a + (- ((b - d) / (b / c)))) + (a + ((b - d) / (b / c)))) / 2
by XCMPLX_1:187
.=
a
;
hence
centroid ((d (#) (TrapezoidalFS ((a - c),(a + ((d - b) / (b / c))),(a + ((b - d) / (b / c))),(a + c)))),['(a - c),(a + c)']) = a
by A4; verum