let a, b be positive Real; :: thesis: for n, m being positive Real holds
( (a to_power (n + m)) + (b to_power (n + m)) = (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2 iff a = b )
let n, m be positive Real; :: thesis: ( (a to_power (n + m)) + (b to_power (n + m)) = (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2 iff a = b )
( a = b implies ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) = 0 ) ;
then A1: ( a = b implies (a to_power (n + m)) + (b to_power (n + m)) = ((((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) + 0) / 2 ) by N158;
( a <> b implies ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) > 0 )
proof
assume a <> b ; :: thesis: ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) > 0
per cases then ( a > b or a < b ) by XXREAL_0:1;
suppose a > b ; :: thesis: ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) > 0
then ( a to_power n > b to_power n & a to_power m > b to_power m ) by POWER:37;
then ( (a to_power n) - (b to_power n) > (b to_power n) - (b to_power n) & (a to_power m) - (b to_power m) > (b to_power m) - (b to_power m) ) by XREAL_1:9;
hence ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) > 0 ; :: thesis: verum
end;
suppose a < b ; :: thesis: ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) > 0
then ( a to_power n < b to_power n & a to_power m < b to_power m ) by POWER:37;
then ( (a to_power n) - (b to_power n) < (b to_power n) - (b to_power n) & (a to_power m) - (b to_power m) < (b to_power m) - (b to_power m) ) by XREAL_1:9;
hence ((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)) > 0 ; :: thesis: verum
end;
end;
end;
then ( a <> b implies (((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m))) > (((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + 0 ) by XREAL_1:6;
then ( a <> b implies ((((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) + (((a to_power n) - (b to_power n)) * ((a to_power m) - (b to_power m)))) / 2 > (((a to_power m) + (b to_power m)) * ((a to_power n) + (b to_power n))) / 2 ) by XREAL_1:68;
hence ( (a to_power (n + m)) + (b to_power (n + m)) = (((a to_power n) + (b to_power n)) * ((a to_power m) + (b to_power m))) / 2 iff a = b ) by A1, N158; :: thesis: verum