let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) holds
( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (a - c) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 & f . (a + c) = 0 )
let f be Function of REAL,REAL; :: thesis: ( b > 0 & c > 0 & ( for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ) implies ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (a - c) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 & f . (a + c) = 0 ) )
assume that
A1: b > 0 and
A2: c > 0 and
A3: for x being Real holds f . x = max (0,(b - |.((b * (x - a)) / c).|)) ; :: thesis: ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (a - c) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 & f . (a + c) = 0 )
A5: ( a < a + c & a - c < a ) by XREAL_1:44, XREAL_1:29, A2;
A8: ( [.(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 XXREAL_0:2, A5, INTEGRA5:def 3, INTEGRA1:4;
A6: f . (a - c) = max (0,(b - |.((b * ((a - c) - a)) / c).|)) by A3
.= max (0,(b - |.(((- 1) * (c * b)) / c).|))
.= max (0,(b - |.((- 1) * ((c * b) / c)).|)) by XCMPLX_1:74
.= max (0,(b - |.(- ((c * b) / c)).|))
.= max (0,(b - |.(- b).|)) by A2, XCMPLX_1:89
.= max (0,(b - (- (- b)))) by ABSVALUE:def 1, A1
.= 0 ;
f . (a + c) = max (0,(b - |.((b * ((a + c) - a)) / c).|)) by A3
.= max (0,(b - |.b.|)) by A2, XCMPLX_1:89
.= max (0,(b - b)) by ABSVALUE:def 1, A1
.= 0 ;
hence ( f . (lower_bound ['(a - c),(a + c)']) = 0 & f . (a - c) = 0 & f . (upper_bound ['(a - c),(a + c)']) = 0 & f . (a + c) = 0 ) by A6, A8, INTEGRA1:5; :: thesis: verum