let z be Nat; :: thesis: ( 2 <= z implies for k being Nat ex N being Nat st
for x being Nat st N <= x holds
1 / (z to_power x) < 1 / (x to_power k) )
assume P0: 2 <= z ; :: thesis: for k being Nat ex N being Nat st
for x being Nat st N <= x holds
1 / (z to_power x) < 1 / (x to_power k)
let k be Nat; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
1 / (z to_power x) < 1 / (x to_power k)
consider N being Nat such that
P1: for x being Nat st N <= x holds
1 / (2 to_power x) < 1 / (x to_power k) by L2;
take N ; :: thesis: for x being Nat st N <= x holds
1 / (z to_power x) < 1 / (x to_power k)

now :: thesis: for x being Nat st N <= x holds
1 / (z to_power x) < 1 / (x to_power k)

let x be Nat; :: thesis: ( N <= x implies 1 / (z to_power x) < 1 / (x to_power k) )
assume N <= x ; :: thesis: 1 / (z to_power x) < 1 / (x to_power k)
then E1: 1 / (2 to_power x) < 1 / (x to_power k) by P1;
P3: 0 < 2 to_power x by POWER:34;
2 to_power x <= z to_power x

proof

now :: thesis: ( ( 2 = z & 2 to_power x <= z to_power x ) or ( 2 < z & 2 to_power x <= z to_power x ) )

per cases ( 2 = z or 2 < z ) by P0, XXREAL_0:1;

case 2 = z ; :: thesis: 2 to_power x <= z to_power x

hence 2 to_power x <= z to_power x ; :: thesis: verum

end;

case LL1: 2 < z ; :: thesis: 2 to_power x <= z to_power x

now :: thesis: ( ( x = 0 & 2 to_power x <= z to_power x ) or ( 0 < x & 2 to_power x <= z to_power x ) )

per cases ( x = 0 or 0 < x ) ;

case LL2: x = 0 ; :: thesis: 2 to_power x <= z to_power x

then 2 to_power x = 1 by POWER:24
.= z to_power x by POWER:24, LL2 ;
hence 2 to_power x <= z to_power x ; :: thesis: verum

end;

case 0 < x ; :: thesis: 2 to_power x <= z to_power x

hence 2 to_power x <= z to_power x by POWER:37, LL1; :: thesis: verum

end;

end;

end;

hence 2 to_power x <= z to_power x ; :: thesis: verum

end;

end;

end;

hence 2 to_power x <= z to_power x ; :: thesis: verum

end;

then 1 / (z to_power x) <= 1 / (2 to_power x) by P3, XREAL_1:118;
hence 1 / (z to_power x) < 1 / (x to_power k) by E1, XXREAL_0:2; :: thesis: verum

end;

hence for x being Nat st N <= x holds
1 / (z to_power x) < 1 / (x to_power k) ; :: thesis: verum