let a, k, r be Nat; :: thesis: for x being Real st 1 < x & 0 < k holds
x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))
let x be Real; :: thesis: ( 1 < x & 0 < k implies x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r)) )
assume that
A1: 1 < x and
A2: 0 < k ; :: thesis: x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r))
set xNak = x |^ ((a * k) + r);
0 + 1 <= k by A2, NAT_1:13;
then k = (k -' 1) + 1 by XREAL_1:235;
then x |^ ((a * k) + r) = x #Z (a + ((a * (k -' 1)) + r)) by PREPOWER:36;
then x |^ ((a * k) + r) = (x #Z a) * (x #Z ((a * (k -' 1)) + r)) by A1, PREPOWER:44;
then x |^ ((a * k) + r) = (x |^ a) * (x #Z ((a * (k -' 1)) + r)) by PREPOWER:36;
hence x |^ ((a * k) + r) = (x |^ a) * (x |^ ((a * (k -' 1)) + r)) by PREPOWER:36; :: thesis: verum