let n be Nat; :: thesis: for r being Real
for k being Nat st k >= n & r >= 1 holds
r |^ k >= r |^ n
let r be Real; :: thesis: for k being Nat st k >= n & r >= 1 holds
r |^ k >= r |^ n
let k be Nat; :: thesis: ( k >= n & r >= 1 implies r |^ k >= r |^ n )
assume that
A1: k >= n and
A2: r >= 1 ; :: thesis: r |^ k >= r |^ n
consider m being Nat such that
A3: k = n + m by A1, NAT_1:10;
A4: r |^ k = (r |^ n) * (r |^ m) by A3, NEWTON:8;
r |^ n >= 1 by A2, Th11;
hence r |^ k >= r |^ n by A2, A4, Th11, XREAL_1:151; :: thesis: verum