let n, k be Element of NAT ; :: thesis: for th being real number st 0 <= th & th <= 1 & n <= k holds
th |^ k <= th |^ n
let th be real number ; :: thesis: ( 0 <= th & th <= 1 & n <= k implies th |^ k <= th |^ n )
assume that
A1: 0 <= th and
A2: th <= 1 and
A3: n <= k ; :: thesis: th |^ k <= th |^ n
A4: for m being Element of NAT holds
( (th GeoSeq ) . (m + 1) <= (th GeoSeq ) . m & (th GeoSeq ) . m >= 0 )

proof

let m be Element of NAT ; :: thesis: ( (th GeoSeq ) . (m + 1) <= (th GeoSeq ) . m & (th GeoSeq ) . m >= 0 )
defpred S₁[ Element of NAT ] means ( (th GeoSeq ) . ($1 + 1) <= (th GeoSeq ) . $1 & (th GeoSeq ) . $1 >= 0 );
A5: (th GeoSeq ) . (0 + 1) = ((th GeoSeq ) . 0 ) * th by PREPOWER:4
.= 1 * th by PREPOWER:4
.= th ;
A6: S₁[ 0 ] by A2, A5, PREPOWER:4;
A7: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume that
(th GeoSeq ) . (m + 1) <= (th GeoSeq ) . m and
A8: (th GeoSeq ) . m >= 0 ; :: thesis: S₁[m + 1]
A9: ( (th GeoSeq ) . ((m + 1) + 1) = ((th GeoSeq ) . (m + 1)) * th & (th GeoSeq ) . (m + 1) = ((th GeoSeq ) . m) * th ) by PREPOWER:4;
thus S₁[m + 1] by A1, A2, A8, A9, XREAL_1:155; :: thesis: verum

end;

A10: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A6, A7);
thus ( (th GeoSeq ) . (m + 1) <= (th GeoSeq ) . m & (th GeoSeq ) . m >= 0 ) by A10; :: thesis: verum

end;

A11: th GeoSeq is non-increasing by A4, SEQM_3:def 14;
A12: ( th |^ k = (th GeoSeq ) . k & th |^ n = (th GeoSeq ) . n ) by PREPOWER:def 1;
thus th |^ k <= th |^ n by A3, A11, A12, SEQM_3:14; :: thesis: verum