let m be positive Nat; :: thesis: for x0 being Element of F_Real
for s, z0 being Real st 0 < x0 & x0 <= m & 0 < s & s < 1 & 1 < z0 holds
|.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m)
let x0 be Element of F_Real; :: thesis: for s, z0 being Real st 0 < x0 & x0 <= m & 0 < s & s < 1 & 1 < z0 holds
|.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m)
let s, z0 be Real; :: thesis: ( 0 < x0 & x0 <= m & 0 < s & s < 1 & 1 < z0 implies |.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m) )
assume A1: ( 0 < x0 & x0 <= m & 0 < s & s < 1 & 1 < z0 ) ; :: thesis: |.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m)
set t = 1 - s;
1 - s < 1 - 0 by A1, XREAL_1:15;
then x0 * (1 - s) < x0 by XREAL_1:157, A1;
then x0 * (1 - s) < m by A1, XXREAL_0:2;
then A4: ( 0 < z0 to_power (x0 * (1 - s)) & z0 to_power (x0 * (1 - s)) < z0 to_power m ) by A1, POWER:34, POWER:39;
|.(- (x0 * (z0 to_power (x0 * (1 - s))))).| = |.(x0 * (z0 to_power (x0 * (1 - s)))).| by COMPLEX1:52
.= x0 * (z0 to_power (x0 * (1 - s))) by A4, A1, ABSVALUE:def 1 ;
hence |.(- (x0 * (z0 to_power (x0 * (1 - s))))).| <= m * (z0 to_power m) by A1, A4, XREAL_1:97; :: thesis: verum