defpred S₁[ Nat] means for a being Nat st a > 1 holds
a |^ $1 > $1;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]

now

let a be Nat; :: thesis: ( a > 1 implies b₁ |^ (n + 1) > n + 1 )
assume A3: a > 1 ; :: thesis: b₁ |^ (n + 1) > n + 1
then a >= 1 + 1 by NAT_1:13;
then A4: a * n >= 2 * n by XREAL_1:66;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: b₁ |^ (n + 1) > n + 1

hence a |^ (n + 1) > n + 1 by A3, NEWTON:10; :: thesis: verum

end;

suppose n > 0 ; :: thesis: b₁ |^ (n + 1) > n + 1

then n >= 0 + 1 by NAT_1:13;
then n + n >= n + 1 by XREAL_1:8;
then A5: a * n >= n + 1 by A4, XXREAL_0:2;
(a |^ n) * a > n * a by A2, A3, XREAL_1:70;
then a |^ (n + 1) > n * a by NEWTON:11;
hence a |^ (n + 1) > n + 1 by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A6: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A1);
hence for a, n being Nat st a > 1 holds
a |^ n > n ; :: thesis: verum