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

proof

let m1 be Element of NAT ; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume a |^ (2 + m1) < a ; :: thesis: S₁[m1 + 1]
then (a |^ (2 + m1)) * a < a * a by A1, XREAL_1:70;
then a |^ ((2 + m1) + 1) < a * a by NEWTON:11;
hence S₁[m1 + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

a |^ (2 + 0 ) = (a GeoSeq ) . (1 + 1) by Def1
.= ((a GeoSeq ) . (0 + 1)) * a by Th4
.= (((a GeoSeq ) . 0 ) * a) * a by Th4
.= (1 * a) * a by Th4
.= a * a ;
then A7: S₁[ 0 ] by A5;
A8: for m1 being Element of NAT holds S₁[m1] from NAT_1:sch 1(A7, A6);
m in NAT by ORDINAL1:def 13;
hence a |^ n < a by A4, A8; :: thesis: verum