let a be Real; :: thesis: for n being Nat st 1 < a & 2 <= n holds
a < a |^ n
let n be Nat; :: thesis: ( 1 < a & 2 <= n implies a < a |^ n )
assume that
A1: 1 < a and
A2: 2 <= n ; :: thesis: a < a |^ n
consider m being Nat such that
A3: n = 2 + m by A2, NAT_1:10;
defpred S₁[ Nat] means a < a |^ (2 + $1);
A4: a * a > a * 1 by A1, XREAL_1:68;
A5: for m1 being Nat st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Nat; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume a < a |^ (2 + m1) ; :: thesis: S₁[m1 + 1]
then (a |^ (2 + m1)) * a > a * a by A1, XREAL_1:68;
then a |^ ((2 + m1) + 1) > a * a by NEWTON:6;
hence S₁[m1 + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

a |^ (2 + 0) = (a GeoSeq) . (1 + 1) by Def1
.= ((a GeoSeq) . (0 + 1)) * a by Th3
.= (((a GeoSeq) . 0) * a) * a by Th3
.= (1 * a) * a by Th3
.= a * a ;
then A6: S₁[ 0 ] by A4;
A7: for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A6, A5);
thus a < a |^ n by A3, A7; :: thesis: verum