let k, n, x be Nat; ( k > n & x > 1 implies x |^ k > x |^ n )
assume that
A1:
k > n
and
A2:
x > 1
; x |^ k > x |^ n
consider m being Nat such that
A3:
k = n + m
by A1, NAT_1:10;
(m + n) - n > n - n
by A1, A3, XREAL_1:9;
then
(m + 1) - 1 > 1 - 1
;
then
m + 1 > 1
by XREAL_1:9;
then A4:
m >= 1
by NAT_1:13;
1 |^ m = 1
;
then A5:
x |^ m > 1
by A2, A4, PREPOWER:10;
A6:
x |^ n >= 1
by A2, PREPOWER:11;
x |^ k = (x |^ n) * (x |^ m)
by A3, NEWTON:8;
hence
x |^ k > x |^ n
by A6, A5, XREAL_1:155; verum