let seq be Real_Sequence; :: thesis: ex Nseq being increasing sequence of NAT st seq * Nseq is monotone
defpred S1[ Nat] means for m being Nat st $1 < m holds
seq . $1 < seq . m;
consider XN being Subset of NAT such that
A1: for n being Element of NAT holds
( n in XN iff S1[n] ) from SUBSET_1:sch 3();
A2: now :: thesis: ( ex k1 being Nat st
for n being Nat st n in XN holds
n <= k1 implies ex Nseq1 being increasing sequence of NAT st seq * Nseq1 is monotone )
given k1 being Nat such that A3: for n being Nat st n in XN holds
n <= k1 ; :: thesis: ex Nseq1 being increasing sequence of NAT st seq * Nseq1 is monotone
set seq1 = seq ^\ (1 + k1);
defpred S2[ set , set , set ] means for k, l being Nat st k = $2 & l = $3 holds
( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k & ( for m being Nat st k < m & (seq ^\ (1 + k1)) . m <= (seq ^\ (1 + k1)) . k holds
l <= m ) );
A4: now :: thesis: for k being Nat st k1 < k holds
ex n being Nat st
( k < n & seq . n <= seq . k )
let k be Nat; :: thesis: ( k1 < k implies ex n being Nat st
( k < n & seq . n <= seq . k ) )
A5: k in NAT by ORDINAL1:def 12;
assume k1 < k ; :: thesis: ex n being Nat st
( k < n & seq . n <= seq . k )
then not k in XN by A3;
then consider m being Nat such that
A6: k < m and
A7: not seq . k < seq . m by A1, A5;
take n = m; :: thesis: ( k < n & seq . n <= seq . k )
thus k < n by A6; :: thesis: seq . n <= seq . k
thus seq . n <= seq . k by A7; :: thesis: verum
end;
A8: now :: thesis: for k being Nat ex l being Element of NAT st
( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k )
let k be Nat; :: thesis: ex l being Element of NAT st
( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k )
0 + k1 < (k + 1) + k1 by XREAL_1:8;
then consider n being Nat such that
A9: (k + 1) + k1 < n and
A10: seq . n <= seq . ((k + 1) + k1) by A4;
consider m being Nat such that
A11: n = ((k + 1) + k1) + m by A9, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
n - (1 + k1) = (k + 0) + m by A11;
then consider n1 being Element of NAT such that
A12: n1 = n - (1 + k1) ;
seq . n <= seq . (k + (1 + k1)) by A10;
then A13: seq . n <= (seq ^\ (1 + k1)) . k by NAT_1:def 3;
take l = n1; :: thesis: ( k < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k )
now :: thesis: k < l
assume not k < l ; :: thesis: contradiction
then (n - (1 + k1)) + (1 + k1) <= k + (1 + k1) by A12, XREAL_1:6;
hence contradiction by A9; :: thesis: verum
end;
hence k < l ; :: thesis: (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k
n = l + (1 + k1) by A12;
hence (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . k by A13, NAT_1:def 3; :: thesis: verum
end;
A14: for n being Nat
for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S2[n,x,y]
defpred S3[ Nat] means ( x < $1 & (seq ^\ (1 + k1)) . $1 <= (seq ^\ (1 + k1)) . x );
ex n being Element of NAT st S3[n] by A8;
then A15: ex n being Nat st S3[n] ;
ex l being Nat st
( S3[l] & ( for m being Nat st S3[m] holds
l <= m ) ) from NAT_1:sch 5(A15);
 then consider l being Nat such that
A16: ( x < l & (seq ^\ (1 + k1)) . l <= (seq ^\ (1 + k1)) . x & ( for m being Nat st x < m & (seq ^\ (1 + k1)) . m <= (seq ^\ (1 + k1)) . x holds
l <= m ) ) ;
take l ; :: thesis: ( l is Element of NAT & S2[n,x,l] )
l in NAT by ORDINAL1:def 12;
hence ( l is Element of NAT & S2[n,x,l] ) by A16; :: thesis: verum
end;
consider f being sequence of NAT such that
f . 0 = 0 and
A17: for n being Nat holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A14);
A18: dom f = NAT by FUNCT_2:def 1;
rng f c= REAL ;
then reconsider f = f as Real_Sequence by A18, RELSET_1:4;
for n being Nat holds f . n < f . (n + 1) by A17;
then reconsider f = f as increasing sequence of NAT by SEQM_3:def 6;
consider Nseq being increasing sequence of NAT such that
A19: seq ^\ (1 + k1) = seq * Nseq by VALUED_0:def 17;
reconsider Nseq1 = Nseq * f as increasing sequence of NAT ;
take Nseq1 = Nseq1; :: thesis: seq * Nseq1 is monotone
now :: thesis: for n being Nat holds (seq * Nseq1) . (n + 1) <= (seq * Nseq1) . n
let n be Nat; :: thesis: (seq * Nseq1) . (n + 1) <= (seq * Nseq1) . n
A20: ( n in NAT & n + 1 in NAT ) by ORDINAL1:def 12;
(seq ^\ (1 + k1)) . (f . (n + 1)) <= (seq ^\ (1 + k1)) . (f . n) by A17;
then ((seq ^\ (1 + k1)) * f) . (n + 1) <= (seq ^\ (1 + k1)) . (f . n) by FUNCT_2:15;
then ((seq * Nseq) * f) . (n + 1) <= ((seq ^\ (1 + k1)) * f) . n by A19, FUNCT_2:15, A20;
then (seq * Nseq1) . (n + 1) <= ((seq * Nseq) * f) . n by A19, RELAT_1:36;
hence (seq * Nseq1) . (n + 1) <= (seq * Nseq1) . n by RELAT_1:36; :: thesis: verum
end;
then seq * Nseq1 is non-increasing ;
hence seq * Nseq1 is monotone by SEQM_3:def 5; :: thesis: verum
end;
now :: thesis: ( ( for l being Nat ex n being Nat st
( n in XN & not n <= l ) ) implies ex Nseq being increasing sequence of NAT st seq * Nseq is monotone )
defpred S2[ set , set , set ] means for k, l being Element of NAT st k = $2 & l = $3 holds
( l in XN & k < l & ( for m being Nat st m in XN & k < m holds
l <= m ) );
assume A21: for l being Nat ex n being Nat st
( n in XN & not n <= l ) ; :: thesis: ex Nseq being increasing sequence of NAT st seq * Nseq is monotone
then consider n1 being Nat such that
A22: n1 in XN and
not n1 <= 0 ;
reconsider O9 = n1 as Element of NAT by ORDINAL1:def 12;
A23: for n being Nat
for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S2[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S2[n,x,y]
defpred S3[ Nat] means ( $1 in XN & x < $1 );
ex n being Nat st S3[n] by A21;
then ex n being Element of NAT st S3[n] ;
then A24: ex n being Nat st S3[n] ;
ex l being Nat st
( S3[l] & ( for m being Nat st S3[m] holds
l <= m ) ) from NAT_1:sch 5(A24);
 then consider l being Nat such that
A25: ( l in XN & x < l & ( for m being Nat st m in XN & x < m holds
l <= m ) ) ;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
take l ; :: thesis: S2[n,x,l]
thus S2[n,x,l] by A25; :: thesis: verum
end;
consider f being sequence of NAT such that
A26: f . 0 = O9 and
A27: for n being Nat holds S2[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A23);
A28: dom f = NAT by FUNCT_2:def 1;
rng f c= REAL ;
then reconsider f = f as Real_Sequence by A28, RELSET_1:4;
A29: for n being Nat holds
( n is Element of NAT & f . n is Element of NAT ) by ORDINAL1:def 12;
A30: now :: thesis: for n being Nat holds f . n < f . (n + 1)
let n be Nat; :: thesis: f . n < f . (n + 1)
( f . n is Element of NAT & f . (n + 1) is Element of NAT ) by A29;
hence f . n < f . (n + 1) by A27; :: thesis: verum
end;
A31: now :: thesis: for n, n being Nat holds S3[n]
defpred S3[ Nat] means f . $1 in XN;
let n be Nat; :: thesis: for n being Nat holds S3[n]
A32: now :: thesis: for k being Nat st S3[k] holds
S3[k + 1]
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume S3[k] ; :: thesis: S3[k + 1]
( f . k is Element of NAT & f . (k + 1) is Element of NAT ) by A29;
hence S3[k + 1] by A27; :: thesis: verum
end;
A33: S3[ 0 ] by A22, A26;
thus for n being Nat holds S3[n] from NAT_1:sch 2(A33, A32); :: thesis: verum
end;
reconsider f = f as increasing sequence of NAT by A30, SEQM_3:def 6;
take Nseq = f; :: thesis: seq * Nseq is monotone
now :: thesis: for n being Nat holds (seq * Nseq) . n < (seq * Nseq) . (n + 1)
let n be Nat; :: thesis: (seq * Nseq) . n < (seq * Nseq) . (n + 1)
A34: n in NAT by ORDINAL1:def 12;
( Nseq . n in XN & Nseq . n < Nseq . (n + 1) ) by A31, A30;
then seq . (Nseq . n) < seq . (Nseq . (n + 1)) by A1;
then (seq * Nseq) . n < seq . (Nseq . (n + 1)) by FUNCT_2:15, A34;
hence (seq * Nseq) . n < (seq * Nseq) . (n + 1) by FUNCT_2:15; :: thesis: verum
end;
then seq * Nseq is increasing ;
hence seq * Nseq is monotone by SEQM_3:def 5; :: thesis: verum
end;
hence ex Nseq being increasing sequence of NAT st seq * Nseq is monotone by A2; :: thesis: verum