let a, b be natural number ; :: thesis: ( 1 < a implies b <= a |^ b )
defpred S₁[ natural number ] means $1 <= a |^ $1;
assume A1: 1 < a ; :: thesis: b <= a |^ b
then reconsider a1 = a - 1 as Element of NAT by INT_1:18;
A2: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then A3: k + 1 <= (a |^ k) + 1 by XREAL_1:8;

A4: now

set x = a |^ k;
assume (a |^ k) + 1 > (a |^ k) * a ; :: thesis: contradiction
then ((a |^ k) * a) - ((a |^ k) + 1) < ((a |^ k) + 1) - ((a |^ k) + 1) by XREAL_1:16;
then (((a |^ k) * a1) - 1) + 1 < 0 + 1 by XREAL_1:8;
then ( a |^ k = 0 or a1 = 0 ) by NAT_1:13;
hence contradiction by A1; :: thesis: verum

end;

a |^ (k + 1) = (a |^ k) * a by NEWTON:11;
hence S₁[k + 1] by A3, A4, XXREAL_0:2; :: thesis: verum

end;

A5: S₁[ 0 ] ;
for k being natural number holds S₁[k] from NAT_1:sch 2(A5, A2);
hence b <= a |^ b ; :: thesis: verum