let a be non trivial Nat; :: thesis: for n, m being Nat st n > m holds
a |^ n > a |^ m
let n, m be Nat; :: thesis: ( n > m implies a |^ n > a |^ m )
assume A1: n > m ; :: thesis: a |^ n > a |^ m
then consider k being Nat such that
A2: n = m + k by NAT_1:10;
k <> 0 by A1, A2;
then k + 1 > 0 + 1 by XREAL_1:6;
then k >= 1 by NAT_1:13;
then a |^ k >= a |^ 1 by Th1;
then A3: a |^ k >= a ;
a >= 2 by NAT_2:29;
then a |^ k >= 1 + 1 by A3, XXREAL_0:2;
then a |^ k > 1 by NAT_1:13;
then 1 * (a |^ m) < (a |^ k) * (a |^ m) by XREAL_1:68;
hence a |^ n > a |^ m by A2, NEWTON:8; :: thesis: verum