let a, b be real number ; :: thesis: for n being natural number st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
let n be natural number ; :: thesis: ( 0 < a & a < b & 1 <= n implies a |^ n < b |^ n )
assume A1: ( 0 < a & a < b & 1 <= n ) ; :: thesis: a |^ n < b |^ n
then consider m being Nat such that
A2: n = 1 + m by NAT_1:10;
A3: m in NAT by ORDINAL1:def 13;
A4: a |^ (1 + 0 ) = (a GeoSeq ) . (0 + 1) by Def1
.= ((a GeoSeq ) . 0 ) * a by Th4
.= 1 * a by Th4
.= a ;
defpred S₁[ Element of NAT ] means a |^ (1 + $1) < b |^ (1 + $1);
b |^ (1 + 0 ) = (b GeoSeq ) . (0 + 1) by Def1
.= ((b GeoSeq ) . 0 ) * b by Th4
.= 1 * b by Th4
.= b ;
then A5: S₁[ 0 ] by A1, A4;
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 A7: a |^ (1 + m1) < b |^ (1 + m1) ; :: thesis: S₁[m1 + 1]
a |^ (1 + m1) > 0 by A1, Th13;
then (a |^ (1 + m1)) * a < (b |^ (1 + m1)) * b by A1, A7, XREAL_1:99;
then a |^ ((1 + m1) + 1) < (b |^ (1 + m1)) * b by NEWTON:11;
hence S₁[m1 + 1] by NEWTON:11; :: thesis: verum

end;

for m1 being Element of NAT holds S₁[m1] from NAT_1:sch 1(A5, A6);
hence a |^ n < b |^ n by A2, A3; :: thesis: verum