let k be Nat; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
1 / (2 to_power x) < 1 / (x to_power k)
consider N0 being Nat such that
P1: for x being Nat st N0 <= x holds
x to_power k < 2 to_power x by L1;
set N = N0 + 2;
take N0 + 2 ; :: thesis: for x being Nat st N0 + 2 <= x holds
1 / (2 to_power x) < 1 / (x to_power k)

now :: thesis: for x being Nat st N0 + 2 <= x holds
1 / (2 to_power x) < 1 / (x to_power k)

let x be Nat; :: thesis: ( N0 + 2 <= x implies 1 / (2 to_power x) < 1 / (x to_power k) )
assume AS: N0 + 2 <= x ; :: thesis: 1 / (2 to_power x) < 1 / (x to_power k)
N0 <= N0 + 2 by NAT_1:12;
then N0 <= x by XXREAL_0:2, AS;
then E1: x to_power k < 2 to_power x by P1;
0 < x to_power k by POWER:34, AS;
hence 1 / (2 to_power x) < 1 / (x to_power k) by XREAL_1:76, E1; :: thesis: verum

end;

hence for x being Nat st N0 + 2 <= x holds
1 / (2 to_power x) < 1 / (x to_power k) ; :: thesis: verum