let a, b be positive Real; :: thesis: ( a <> b implies ex n, m being Real st a - b = ((a / b) to_power n) * (((a / b) to_power m) - 1) )
assume A1: a <> b ; :: thesis: ex n, m being Real st a - b = ((a / b) to_power n) * (((a / b) to_power m) - 1)
consider x, y being Real such that
A2: ( a = (a / b) to_power x & b = (a / b) to_power y ) by A1, ATB;
(a / b) to_power x = (a / b) to_power (y + (x - y))
.= ((a / b) to_power y) * ((a / b) to_power (x - y)) by POWER:27 ;
then ((a / b) to_power y) * (((a / b) to_power (x - y)) - 1) = a - b by A2;
hence ex n, m being Real st a - b = ((a / b) to_power n) * (((a / b) to_power m) - 1) ; :: thesis: verum