let a be positive light Real; :: thesis: for n being positive heavy Real holds ((1 + a) to_power n) * ((1 - a) to_power n) < (1 + (a to_power n)) * (1 - (a to_power n))
let n be positive heavy Real; :: thesis: ((1 + a) to_power n) * ((1 - a) to_power n) < (1 + (a to_power n)) * (1 - (a to_power n))
A1: ((1 + a) to_power n) * ((1 - a) to_power n) = ((1 - a) * (1 + a)) to_power n by POWER:30
.= (1 - (a * a)) to_power n ;
A2: (1 + (a to_power n)) * (1 - (a to_power n)) = 1 - ((a to_power n) * (a to_power n))
.= 1 - ((a * a) to_power n) by POWER:30 ;
((1 - (a * a)) to_power n) + ((a * a) to_power n) < ((1 - (a * a)) + (a * a)) to_power n by APB;
then (((1 - (a * a)) to_power n) + ((a * a) to_power n)) - ((a * a) to_power n) < (1 to_power n) - ((a * a) to_power n) by XREAL_1:9;
hence ((1 + a) to_power n) * ((1 - a) to_power n) < (1 + (a to_power n)) * (1 - (a to_power n)) by A1, A2; :: thesis: verum