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