let r be real number ; :: thesis: for m, n being natural number st r > 1 & m > n holds
r |^ m > r |^ n
let m, n be natural number ; :: 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 13;
(m -' n) + n = m by A2, XREAL_1:237;
then A3: r |^ m = (r |^ (m -' n)) * (r |^ n) by NEWTON:13;
m -' n <> 0 by A2, NAT_D:36;
then m -' n > 0 ;
then A4: r |^ (m -' n) > 1 by A1, Th70;
r |^ n > 0 by A1, NEWTON:102;
hence r |^ m > r |^ n by A3, A4, XREAL_1:157; :: thesis: verum