theorem N158: :: COMPLEX3:50

for a, b being positive Real
for n, m being Real holds
( (a to_power (m + n)) + (b to_power (m + n)) = ((((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 + n)) - (b to_power (m + n)) = ((((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 )