let a, b be Real; :: thesis: for n being Nat st 0 < a & a < b & 1 <= n holds
a |^ n < b |^ n
let n be Nat; :: thesis: ( 0 < a & a < b & 1 <= n implies a |^ n < b |^ n )
assume that
A1: 0 < a and
A2: a < b and
A3: 1 <= n ; :: thesis: a |^ n < b |^ n
consider m being Nat such that
A4: n = 1 + m by A3, NAT_1:10;
defpred S₁[ Nat] means a |^ (1 + $1) < b |^ (1 + $1);
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 A6: a |^ (1 + m1) < b |^ (1 + m1) ; :: thesis: S₁[m1 + 1]
a |^ (1 + m1) > 0 by A1, Th6;
then (a |^ (1 + m1)) * a < (b |^ (1 + m1)) * b by A1, A2, A6, XREAL_1:97;
then a |^ ((1 + m1) + 1) < (b |^ (1 + m1)) * b by NEWTON:6;
hence S₁[m1 + 1] by NEWTON:6; :: thesis: verum

end;

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