let a, n be Nat; :: thesis: ( 1 < a implies ex k being Nat st
( 1 < k & n < a |^ k ) )
assume A1: 1 < a ; :: thesis: ex k being Nat st
( 1 < k & n < a |^ k )

per cases ( n = 0 or n >= 1 ) by NAT_1:14;

suppose A2: n = 0 ; :: thesis: ex k being Nat st
( 1 < k & n < a |^ k )

take 2 ; :: thesis: ( 1 < 2 & n < a |^ 2 )
thus ( 1 < 2 & n < a |^ 2 ) by A1, A2; :: thesis: verum

end;

suppose n >= 1 ; :: thesis: ex k being Nat st
( 1 < k & n < a |^ k )

per cases then ( n = 1 or n > 1 ) by XXREAL_0:1;

suppose A3: n = 1 ; :: thesis: ex k being Nat st
( 1 < k & n < a |^ k )

take 2 ; :: thesis: ( 1 < 2 & n < a |^ 2 )
thus 1 < 2 ; :: thesis: n < a |^ 2
1 * 1 < a * a by A1, XREAL_1:96;
hence n < a |^ 2 by A3, WSIERP_1:1; :: thesis: verum

end;

suppose A4: n > 1 ; :: thesis: ex k being Nat st
( 1 < k & n < a |^ k )

take n ; :: thesis: ( 1 < n & n < a |^ n )
thus ( 1 < n & n < a |^ n ) by A1, A4, NAT_3:2; :: thesis: verum

end;

end;

end;

end;