let s1, s2 be Rational_Sequence; for a being Real st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 holds
( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
let a be Real; ( s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 implies ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) ) )
assume that
A1:
s1 is convergent
and
A2:
s2 is convergent
and
A3:
lim s1 = lim s2
and
A4:
a > 0
; ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
thus A5:
a #Q s1 is convergent
by A1, A4, Th69; ( a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
s2 is bounded
by A2;
then consider e being Real such that
0 < e
and
A6:
for n being Nat holds |.(s2 . n).| < e
by SEQ_2:3;
s1 is bounded
by A1;
then consider d being Real such that
0 < d
and
A7:
for n being Nat holds |.(s1 . n).| < d
by SEQ_2:3;
consider m1 being Nat such that
A8:
d + e < m1
by SEQ_4:3;
thus A9:
a #Q s2 is convergent
by A2, A4, Th69; lim (a #Q s1) = lim (a #Q s2)
reconsider m1 = m1 as Rational ;
A10:
a #Q m1 > 0
by A4, Th52;
per cases
( a >= 1 or a < 1 )
;
suppose A11:
a < 1
;
lim (a #Q s1) = lim (a #Q s2)then
a / a < 1
/ a
by A4, XREAL_1:74;
then
1
< 1
/ a
by A4, XCMPLX_1:60;
then A12:
lim ((1 / a) #Q s1) = lim ((1 / a) #Q s2)
by A1, A2, A3, Lm7;
A13:
(1 / a) #Q s2 is
convergent
by A2, A4, Th69;
A14:
(1 / a) #Q s1 is
convergent
by A1, A4, Th69;
then A15:
((1 / a) #Q s1) - ((1 / a) #Q s2) is
convergent
by A13;
A16:
lim (((1 / a) #Q s1) - ((1 / a) #Q s2)) =
(lim ((1 / a) #Q s1)) - (lim ((1 / a) #Q s2))
by A14, A13, SEQ_2:12
.=
0
by A12
;
A17:
now for c being Real st c > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < clet c be
Real;
( c > 0 implies ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c )assume A18:
c > 0
;
ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < cthen
c * (a #Q m1) > 0
by A10;
then consider n being
Nat such that A19:
for
m being
Nat st
n <= m holds
|.(((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0).| < c * (a #Q m1)
by A15, A16, SEQ_2:def 7;
take n =
n;
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < clet m be
Nat;
( m >= n implies |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c )assume
m >= n
;
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < cthen
|.(((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0).| < c * (a #Q m1)
by A19;
then A20:
|.((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)).| < c * (a #Q m1)
by RFUNCT_2:1;
A21:
a #Q (s1 . m) <> 0
by A4, Th52;
|.(s1 . m).| < d
by A7;
then A22:
|.(s1 . m).| + |.(s2 . m).| < d + e
by A6, XREAL_1:8;
|.((s1 . m) + (s2 . m)).| <= |.(s1 . m).| + |.(s2 . m).|
by COMPLEX1:56;
then
|.((s1 . m) + (s2 . m)).| < d + e
by A22, XXREAL_0:2;
then
|.((s1 . m) + (s2 . m)).| < m1
by A8, XXREAL_0:2;
then A23:
|.(- ((s1 . m) + (s2 . m))).| < m1
by COMPLEX1:52;
- ((s1 . m) + (s2 . m)) <= |.(- ((s1 . m) + (s2 . m))).|
by ABSVALUE:4;
then
- ((s1 . m) + (s2 . m)) < m1
by A23, XXREAL_0:2;
then A24:
m1 - (- ((s1 . m) + (s2 . m))) > 0
by XREAL_1:50;
A25:
a #Q (s2 . m) <> 0
by A4, Th52;
A26:
a #Q ((s1 . m) + (s2 . m)) > 0
by A4, Th52;
|.((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)).| =
|.(((1 / a) #Q (s1 . m)) - (((1 / a) #Q s2) . m)).|
by Def5
.=
|.(((1 / a) #Q (s1 . m)) - ((1 / a) #Q (s2 . m))).|
by Def5
.=
|.((1 / (a #Q (s1 . m))) - ((1 / a) #Q (s2 . m))).|
by A4, Th57
.=
|.((1 / (a #Q (s1 . m))) - (1 / (a #Q (s2 . m)))).|
by A4, Th57
.=
|.(((a #Q (s1 . m)) ") - (1 / (a #Q (s2 . m)))).|
.=
|.(((a #Q (s1 . m)) ") - ((a #Q (s2 . m)) ")).|
.=
|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (|.(a #Q (s1 . m)).| * |.(a #Q (s2 . m)).|)
by A21, A25, SEQ_2:2
.=
|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / |.((a #Q (s1 . m)) * (a #Q (s2 . m))).|
by COMPLEX1:65
.=
|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / |.(a #Q ((s1 . m) + (s2 . m))).|
by A4, Th53
.=
|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (a #Q ((s1 . m) + (s2 . m)))
by A26, ABSVALUE:def 1
;
then A27:
(|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (a #Q ((s1 . m) + (s2 . m)))) * (a #Q ((s1 . m) + (s2 . m))) < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m)))
by A20, A26, XREAL_1:68;
a #Q ((s1 . m) + (s2 . m)) <> 0
by A4, Th52;
then A28:
|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m)))
by A27, XCMPLX_1:87;
(a #Q m1) * (a #Q ((s1 . m) + (s2 . m))) = a #Q (m1 + ((s1 . m) + (s2 . m)))
by A4, Th53;
then
c * ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m)))) < 1
* c
by A4, A11, A18, A24, Th65, XREAL_1:68;
then
|.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < c
by A28, XXREAL_0:2;
then
|.(((a #Q s1) . m) - (a #Q (s2 . m))).| < c
by Def5;
then
|.(((a #Q s1) . m) - ((a #Q s2) . m)).| < c
by Def5;
hence
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c
by RFUNCT_2:1;
verum end; then
(a #Q s1) - (a #Q s2) is
convergent
by SEQ_2:def 6;
then
lim ((a #Q s1) - (a #Q s2)) = 0
by A17, SEQ_2:def 7;
then
0 = (lim (a #Q s1)) - (lim (a #Q s2))
by A5, A9, SEQ_2:12;
hence
lim (a #Q s1) = lim (a #Q s2)
;
verum end; end;