let k, n be Nat; :: thesis: for th being Real st 0 <= th & th <= 1 & n <= k holds
th |^ k <= th |^ n
let th be Real; :: 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 Nat holds
( (th GeoSeq) . (m + 1) <= (th GeoSeq) . m & (th GeoSeq) . m >= 0 )

proof

let m be Nat; :: thesis: ( (th GeoSeq) . (m + 1) <= (th GeoSeq) . m & (th GeoSeq) . m >= 0 )
defpred S₁[ Nat] means ( (th GeoSeq) . ($1 + 1) <= (th GeoSeq) . $1 & (th GeoSeq) . $1 >= 0 );
(th GeoSeq) . (0 + 1) = ((th GeoSeq) . 0) * th by PREPOWER:3
.= 1 * th by PREPOWER:3
.= th ;
then A4: S₁[ 0 ] by A2, PREPOWER:3;
A5: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume that
(th GeoSeq) . (m + 1) <= (th GeoSeq) . m and
A6: (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:3;
hence S₁[m + 1] by A1, A2, A6, XREAL_1:153; :: thesis: verum

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A4, A5);
hence ( (th GeoSeq) . (m + 1) <= (th GeoSeq) . m & (th GeoSeq) . m >= 0 ) ; :: thesis: verum

end;

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