let c, d be Real; ( 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 (1,0,c,d)) . m) - (1 / c)).| < p )
set f = rseq (1,0,c,d);
assume A1:
0 < c
; for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
let p be Real; ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p )
assume A2:
0 < p
; ex n being Nat st
for m being Nat st n <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
set f1 = rseq (0,(- d),(c * c),(c * d));
lim (rseq (0,(- d),(c * c),(c * d))) = 0
by A1, Th10;
then consider n being Nat such that
A3:
for m being Nat st n <= m holds
|.(((rseq (0,(- d),(c * c),(c * d))) . m) - 0).| < p
by A2, SEQ_2:def 7;
consider m1 being Nat such that
A4:
0 < (c * m1) + d
by A1, Th1;
reconsider mm = max (m1,(n + 1)) as Nat by TARSKI:1;
take
mm
; for m being Nat st mm <= m holds
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
let m be Nat; ( mm <= m implies |.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p )
assume A5:
mm <= m
; |.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
m1 <= mm
by XXREAL_0:25;
then
m1 <= m
by A5, XXREAL_0:2;
then
c * m1 <= c * m
by A1, XREAL_1:64;
then A6:
(c * m1) + d <= (c * m) + d
by XREAL_1:6;
A7:
n + 0 <= n + 1
by XREAL_1:6;
n + 1 <= mm
by XXREAL_0:25;
then
n <= mm
by A7, XXREAL_0:2;
then A8:
n <= m
by A5, XXREAL_0:2;
((rseq (1,0,c,d)) . m) - (1 / c) =
(((1 * m) + 0) / ((c * m) + d)) - (1 / c)
by Th5
.=
((m * c) - (1 * ((c * m) + d))) / (((c * m) + d) * c)
by A1, A6, A4, XCMPLX_1:130
.=
((0 * m) + (- d)) / (((c * c) * m) + (c * d))
.=
((rseq (0,(- d),(c * c),(c * d))) . m) - 0
by Th5
;
hence
|.(((rseq (1,0,c,d)) . m) - (1 / c)).| < p
by A3, A8; verum