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

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