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₁[ Nat] means a |^ $1 <= b |^ $1;
A4: for m1 being Nat st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Nat; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume A5: a |^ m1 <= b |^ m1 ; :: thesis: S₁[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₁[m1 + 1] by NEWTON:6; :: thesis: verum

end;

A6: b |^ 0 = (b GeoSeq) . 0 by Def1
.= 1 by Th3 ;
a |^ 0 = (a GeoSeq) . 0 by Def1
.= 1 by Th3 ;
then A7: S₁[ 0 ] by A6;
for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A7, A4);
hence a |^ n <= b |^ n by A1; :: thesis: verum