let a, b be Real; :: thesis: for n being natural Number st 0 < a & a <= b holds

a |^ n <= b |^ n

let n be natural Number ; :: thesis: ( 0 < a & a <= b implies a |^ n <= b |^ n )

A1: n is Nat by TARSKI:1;

assume that

A2: 0 < a and

A3: a <= b ; :: thesis: a |^ n <= b |^ n

defpred S_{1}[ Nat] means a |^ $1 <= b |^ $1;

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

S_{1}[m1 + 1]

.= 1 by Th3 ;

a |^ 0 = (a GeoSeq) . 0 by Def1

.= 1 by Th3 ;

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

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

hence a |^ n <= b |^ n by A1; :: thesis: verum

a |^ n <= b |^ n

let n be natural Number ; :: thesis: ( 0 < a & a <= b implies a |^ n <= b |^ n )

A1: n is Nat by TARSKI:1;

assume that

A2: 0 < a and

A3: a <= b ; :: thesis: a |^ n <= b |^ n

defpred S

A4: for m1 being Nat st S

S

proof

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

assume A5: a |^ m1 <= b |^ m1 ; :: thesis: S_{1}[m1 + 1]

a |^ m1 > 0 by A2, Th6;

then (a |^ m1) * a <= (b |^ m1) * b by A2, A3, A5, XREAL_1:66;

then a |^ (m1 + 1) <= (b |^ m1) * b by NEWTON:6;

hence S_{1}[m1 + 1]
by NEWTON:6; :: thesis: verum

end;assume A5: a |^ m1 <= b |^ m1 ; :: thesis: S

a |^ m1 > 0 by A2, Th6;

then (a |^ m1) * a <= (b |^ m1) * b by A2, A3, A5, XREAL_1:66;

then a |^ (m1 + 1) <= (b |^ m1) * b by NEWTON:6;

hence S

.= 1 by Th3 ;

a |^ 0 = (a GeoSeq) . 0 by Def1

.= 1 by Th3 ;

then A7: S

for m1 being Nat holds S

hence a |^ n <= b |^ n by A1; :: thesis: verum