let n be Element of NAT ; :: thesis: for r being real number
for k being natural number st k >= n & r >= 1 holds
r |^ k >= r |^ n
let r be real number ; :: thesis: for k being natural number st k >= n & r >= 1 holds
r |^ k >= r |^ n
let k be natural number ; :: 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:13;
A5: r |^ n >= 1 by A2, Th19;
r |^ m >= 1 by A2, Th19;
hence r |^ k >= r |^ n by A4, A5, XREAL_1:153; :: thesis: verum