let a, b be Real; :: 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 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_{1}[ Nat] means a |^ (1 + $1) < b |^ (1 + $1);

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

S_{1}[m1 + 1]
_{1}[ 0 ]
by A2;

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

thus a |^ n < b |^ n by A4, A8; :: thesis: verum

a |^ n < b |^ n

let n be natural Number ; :: 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

A5: for m1 being Nat st S

S

proof

A7:
S
let m1 be Nat; :: thesis: ( S_{1}[m1] implies S_{1}[m1 + 1] )

assume A6: a |^ (1 + m1) < b |^ (1 + m1) ; :: thesis: S_{1}[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_{1}[m1 + 1]
by NEWTON:6; :: thesis: verum

end;assume A6: a |^ (1 + m1) < b |^ (1 + m1) ; :: thesis: S

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

A8: for m1 being Nat holds S

thus a |^ n < b |^ n by A4, A8; :: thesis: verum