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