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

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

per cases
( a > 0 or a = 0 )
by A1;

end;

suppose A4:
a = 0
; :: thesis: a |^ n < b |^ n

reconsider k = n, k1 = 1 as Integer ;

reconsider m = k - k1 as Element of NAT by A3, INT_1:5;

a |^ n = a |^ (m + 1)

.= (a |^ m) * (a |^ 1) by NEWTON:8

.= (a |^ m) * ((a GeoSeq) . (0 + 1)) by Def1

.= (a |^ m) * (((a GeoSeq) . 0) * 0) by A4, Th3

.= 0 ;

hence a |^ n < b |^ n by A1, A2, Th6; :: thesis: verum

end;reconsider m = k - k1 as Element of NAT by A3, INT_1:5;

a |^ n = a |^ (m + 1)

.= (a |^ m) * (a |^ 1) by NEWTON:8

.= (a |^ m) * ((a GeoSeq) . (0 + 1)) by Def1

.= (a |^ m) * (((a GeoSeq) . 0) * 0) by A4, Th3

.= 0 ;

hence a |^ n < b |^ n by A1, A2, Th6; :: thesis: verum