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_{1}[ Nat] means a < a |^ (2 + $1);

A4: a * a > a * 1 by A1, XREAL_1:68;

A5: for m1 being Nat st S_{1}[m1] holds

S_{1}[m1 + 1]

.= ((a GeoSeq) . (0 + 1)) * a by Th3

.= (((a GeoSeq) . 0) * a) * a by Th3

.= (1 * a) * a by Th3

.= a * a ;

then A6: S_{1}[ 0 ]
by A4;

A7: for m1 being Nat holds S_{1}[m1]
from NAT_1:sch 2(A6, A5);

thus a < a |^ n by A3, A7; :: thesis: verum

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

A4: a * a > a * 1 by A1, XREAL_1:68;

A5: for m1 being Nat st S

S

proof

a |^ (2 + 0) =
(a GeoSeq) . (1 + 1)
by Def1
let m1 be Nat; :: thesis: ( S_{1}[m1] implies S_{1}[m1 + 1] )

assume a < a |^ (2 + m1) ; :: thesis: S_{1}[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_{1}[m1 + 1]
by A4, XXREAL_0:2; :: thesis: verum

end;assume a < a |^ (2 + m1) ; :: thesis: S

then (a |^ (2 + m1)) * a > a * a by A1, XREAL_1:68;

then a |^ ((2 + m1) + 1) > a * a by NEWTON:6;

hence S

.= ((a GeoSeq) . (0 + 1)) * a by Th3

.= (((a GeoSeq) . 0) * a) * a by Th3

.= (1 * a) * a by Th3

.= a * a ;

then A6: S

A7: for m1 being Nat holds S

thus a < a |^ n by A3, A7; :: thesis: verum