let c, d be Real; :: thesis: ( 0 < c implies for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p )
set f = rseq (0,1,c,d);
assume A1: 0 < c ; :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p )
assume A2: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p
consider z being Nat such that
A3: (c * z) + d > 0 by A1, Th1;
consider n being Nat such that
A4: n > (1 - (p * d)) / (c * p) by SEQ_4:3;
reconsider mm = max (n,z) as Nat by TARSKI:1;
take mm ; :: thesis: for m being Nat st mm <= m holds
|.(((rseq (0,1,c,d)) . m) - 0).| < p
let m be Nat; :: thesis: ( mm <= m implies |.(((rseq (0,1,c,d)) . m) - 0).| < p )
assume A5: mm <= m ; :: thesis: |.(((rseq (0,1,c,d)) . m) - 0).| < p
A6: (rseq (0,1,c,d)) . m = ((0 * m) + 1) / ((c * m) + d) by Th5
.= 1 / ((c * m) + d) ;
mm >= z by XXREAL_0:25;
then m >= z by A5, XXREAL_0:2;
then c * m >= c * z by A1, XREAL_1:64;
then A7: (c * m) + d >= (c * z) + d by XREAL_1:6;
A8: (p * ((c * m) + d)) / ((c * m) + d) = p by A3, A7, XCMPLX_1:89;
A9: ((1 - (p * d)) / (c * p)) * (c * p) = 1 - (p * d) by A1, A2, XCMPLX_1:87;
mm >= n by XXREAL_0:25;
then (1 - (p * d)) / (c * p) < mm by A4, XXREAL_0:2;
then (1 - (p * d)) / (c * p) < m by A5, XXREAL_0:2;
then ((1 - (p * d)) / (c * p)) * (c * p) < m * (c * p) by A1, A2, XREAL_1:68;
then (1 - (p * d)) + (p * d) < (m * (c * p)) + (p * d) by A9, XREAL_1:8;
then A10: 1 / ((c * m) + d) < p by A8, A3, A7, XREAL_1:74;
- p < 0 by A2;
hence |.(((rseq (0,1,c,d)) . m) - 0).| < p by A3, A7, A6, A10, SEQ_2:1; :: thesis: verum