let r be Real_Sequence; :: thesis: ( ( for n being non zero Nat ex q being Prime st
( r . n = q / n & not q divides n & ( for p being Prime st not p divides n holds
q <= p ) ) ) implies ( r is convergent & lim r = 0 ) )
assume A1: for n being non zero Nat ex q being Prime st
( r . n = q / n & not q divides n & ( for p being Prime st not p divides n holds
q <= p ) ) ; :: thesis: ( r is convergent & lim r = 0 )
A2: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((r . m) - 0).| < p
proof
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((r . m) - 0).| < p )
assume A3: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((r . m) - 0).| < p
consider w being Nat such that
A4: ( w > 0 & 1 / w < p ) by A3, UNIFORM1:1;
set m = w + 4;
take N = (Product (primesFinS (w + 4))) + 1; :: thesis: for m being Nat st N <= m holds
|.((r . m) - 0).| < p
let n be Nat; :: thesis: ( N <= n implies |.((r . n) - 0).| < p )
assume A5: N <= n ; :: thesis: |.((r . n) - 0).| < p
A6: 2 |^ (w + 4) <= Product (primesFinS (w + 4)) by Th26;
1 <= w + 4 by NAT_1:14;
then 2 <= 2 |^ (w + 4) by PREPOWER:12;
then 2 <= Product (primesFinS (w + 4)) by A6, XXREAL_0:2;
then 2 < N by NAT_1:13;
then 2 < n by A5, XXREAL_0:2;
then consider k being non zero Nat such that
A7: ( Product (primesFinS k) <= n & n < Product (primesFinS (k + 1)) ) by Th27;
set k1 = k - 1;
Product (primesFinS (w + 4)) < N by NAT_1:13;
then Product (primesFinS (w + 4)) < n by A5, XXREAL_0:2;
then Product (primesFinS (w + 4)) < Product (primesFinS (k + 1)) by A7, XXREAL_0:2;
then w + 4 < k + 1 by Th33;
then A8: ( 4 <= w + 4 & w + 4 <= k ) by NAT_1:13, XREAL_1:31;
then 3 + 1 <= (k - 1) + 1 by XXREAL_0:2;
then A9: 3 <= k - 1 by XREAL_1:8;
n is non zero Nat by A5;
then consider q being Prime such that
A10: r . n = q / n and
not q divides n and
A11: for p being Prime st not p divides n holds
q <= p by A1;
1 <= primenumber (k - 1) by INT_2:def 4;
then A12: 1 + (primenumber k) <= (primenumber (k - 1)) + (primenumber ((k - 1) + 1)) by XREAL_1:6;
q <= primenumber k
proof
assume A13: q > primenumber k ; :: thesis: contradiction
for i being Nat st i < k + 1 holds
primenumber i divides n then Product (primesFinS (k + 1)) divides n by Th32;
then Product (primesFinS (k + 1)) <= n by A5, NAT_D:7;
hence contradiction by A7; :: thesis: verum
end;
then q < 1 + (primenumber k) by NAT_1:13;
then A15: q < (primenumber (k - 1)) + (primenumber ((k - 1) + 1)) by A12, XXREAL_0:2;
(primenumber (k - 1)) + (primenumber ((k - 1) + 1)) <= Product (primesFinS (k - 1)) by A9, NUMBER13:23;
then q < Product (primesFinS (k - 1)) by A15, XXREAL_0:2;
then A16: q / n < (Product (primesFinS (k - 1))) / n by A5, XREAL_1:74;
(Product (primesFinS (k - 1))) / n <= (Product (primesFinS (k - 1))) / (Product (primesFinS k)) by A7, XREAL_1:118;
then A17: q / n < (Product (primesFinS (k - 1))) / (Product (primesFinS k)) by A16, XXREAL_0:2;
Product (primesFinS ((k - 1) + 1)) = (Product (primesFinS (k - 1))) * (primenumber (k - 1)) by Th25;
then A18: (1 * (Product (primesFinS (k - 1)))) / (Product (primesFinS k)) = 1 / (primenumber (k - 1)) by XCMPLX_1:91;
k - 1 <= primenumber (k - 1) by PRIMRECI:11;
then 1 / (primenumber (k - 1)) <= 1 / (k - 1) by A9, XREAL_1:118;
then A19: q / n < 1 / (k - 1) by A17, A18, XXREAL_0:2;
(w + 3) + 1 <= (k - 1) + 1 by A8;
then w + 3 <= 0 + (k - 1) by XREAL_1:6;
then w < k - 1 by XREAL_1:8;
then 1 / (k - 1) < 1 / w by A4, XREAL_1:76;
then 1 / (k - 1) < p by A4, XXREAL_0:2;
then A20: q / n < p by A19, XXREAL_0:2;
|.(q / n).| = q / n by ABSVALUE:def 1;
then |.((r . n) - 0).| < p by A20, A10;
hence |.((r . n) - 0).| < p ; :: thesis: verum
end;
then r is convergent by SEQ_2:def 6;
hence ( r is convergent & lim r = 0 ) by A2, SEQ_2:def 7; :: thesis: verum