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
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 );
(th GeoSeq ) . (0 + 1) = ((th GeoSeq ) . 0 ) * th by PREPOWER:4
.= 1 * th by PREPOWER:4
.= th ;
then A6: S₁[ 0 ] by A2, 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]
( (th GeoSeq ) . ((m + 1) + 1) = ((th GeoSeq ) . (m + 1)) * th & (th GeoSeq ) . (m + 1) = ((th GeoSeq ) . m) * th ) by PREPOWER:4;
hence S₁[m + 1] by A1, A2, A8, XREAL_1:155; :: thesis: verum

end;

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

end;

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