let r be Real; :: thesis: for m, n being Nat st r > 1 & m > n holds
r |^ m > r |^ n
let m, n be Nat; :: thesis: ( r > 1 & m > n implies r |^ m > r |^ n )
assume that
A1: r > 1 and
A2: m > n ; :: thesis: r |^ m > r |^ n
reconsider m = m, n = n as Element of NAT by ORDINAL1:def 12;
(m -' n) + n = m by A2, XREAL_1:235;
then A3: r |^ m = (r |^ (m -' n)) * (r |^ n) by NEWTON:8;
m -' n <> 0 by A2, NAT_D:36;
then r |^ (m -' n) > 1 by A1, Th65;
hence r |^ m > r |^ n by A1, A3, NEWTON:83, XREAL_1:155; :: thesis: verum