let a be Real; :: thesis: for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds

lim s2 = a #R (lim s1)

let s1, s2 be Real_Sequence; :: thesis: ( a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) implies lim s2 = a #R (lim s1) )

assume that

A1: a > 0 and

A2: s1 is convergent and

A3: s2 is convergent and

A4: for n being Nat holds s2 . n = a #R (s1 . n) ; :: thesis: lim s2 = a #R (lim s1)

lim s2 = a #R (lim s1)

let s1, s2 be Real_Sequence; :: thesis: ( a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) implies lim s2 = a #R (lim s1) )

assume that

A1: a > 0 and

A2: s1 is convergent and

A3: s2 is convergent and

A4: for n being Nat holds s2 . n = a #R (s1 . n) ; :: thesis: lim s2 = a #R (lim s1)

per cases
( a >= 1 or a < 1 )
;

end;

suppose A5:
a < 1
; :: thesis: lim s2 = a #R (lim s1)

then A15: 1 <= 1 / a by A1, XCMPLX_1:106;

A16: a #R (lim s1) <> 0 by A1, Th81;

then A18: lim (s2 ") = (lim s2) " by A3, A6, SEQ_2:22;

s2 " is convergent by A3, A6, A17, SEQ_2:21;

then (lim s2) " = (1 / a) #R (lim s1) by A2, A15, A18, A14, Lm12

.= 1 / (a #R (lim s1)) by A1, Th79 ;

then 1 = (1 / (a #R (lim s1))) * (lim s2) by A6, XCMPLX_0:def 7;

then a #R (lim s1) = (a #R (lim s1)) * ((1 / (a #R (lim s1))) * (lim s2))

.= ((a #R (lim s1)) * (1 / (a #R (lim s1)))) * (lim s2)

.= 1 * (lim s2) by A16, XCMPLX_1:106 ;

hence lim s2 = a #R (lim s1) ; :: thesis: verum

end;

A6: now :: thesis: not lim s2 = 0

assume A7:
lim s2 = 0
; :: thesis: contradiction

a #R ((lim s1) + 1) > 0 by A1, Th81;

then consider n being Nat such that

A8: for m being Nat st m >= n holds

|.((s2 . m) - 0).| < a #R ((lim s1) + 1) by A3, A7, SEQ_2:def 7;

consider n1 being Nat such that

A9: for m being Nat st m >= n1 holds

|.((s1 . m) - (lim s1)).| < 1 by A2, SEQ_2:def 7;

end;a #R ((lim s1) + 1) > 0 by A1, Th81;

then consider n being Nat such that

A8: for m being Nat st m >= n holds

|.((s2 . m) - 0).| < a #R ((lim s1) + 1) by A3, A7, SEQ_2:def 7;

consider n1 being Nat such that

A9: for m being Nat st m >= n1 holds

|.((s1 . m) - (lim s1)).| < 1 by A2, SEQ_2:def 7;

now :: thesis: for m being Nat holds not m >= n + n1

hence
contradiction
; :: thesis: verumlet m be Nat; :: thesis: not m >= n + n1

assume A10: m >= n + n1 ; :: thesis: contradiction

n + n1 >= n1 by NAT_1:12;

then m >= n1 by A10, XXREAL_0:2;

then A11: |.((s1 . m) - (lim s1)).| < 1 by A9;

(s1 . m) - (lim s1) <= |.((s1 . m) - (lim s1)).| by ABSVALUE:4;

then (s1 . m) - (lim s1) < 1 by A11, XXREAL_0:2;

then A12: ((s1 . m) - (lim s1)) + (lim s1) < (lim s1) + 1 by XREAL_1:6;

n + n1 >= n by NAT_1:12;

then m >= n by A10, XXREAL_0:2;

then |.((s2 . m) - 0).| < a #R ((lim s1) + 1) by A8;

then A13: |.(a #R (s1 . m)).| < a #R ((lim s1) + 1) by A4;

a #R (s1 . m) > 0 by A1, Th81;

then a #R (s1 . m) < a #R ((lim s1) + 1) by A13, ABSVALUE:def 1;

hence contradiction by A1, A5, A12, Th84; :: thesis: verum

end;assume A10: m >= n + n1 ; :: thesis: contradiction

n + n1 >= n1 by NAT_1:12;

then m >= n1 by A10, XXREAL_0:2;

then A11: |.((s1 . m) - (lim s1)).| < 1 by A9;

(s1 . m) - (lim s1) <= |.((s1 . m) - (lim s1)).| by ABSVALUE:4;

then (s1 . m) - (lim s1) < 1 by A11, XXREAL_0:2;

then A12: ((s1 . m) - (lim s1)) + (lim s1) < (lim s1) + 1 by XREAL_1:6;

n + n1 >= n by NAT_1:12;

then m >= n by A10, XXREAL_0:2;

then |.((s2 . m) - 0).| < a #R ((lim s1) + 1) by A8;

then A13: |.(a #R (s1 . m)).| < a #R ((lim s1) + 1) by A4;

a #R (s1 . m) > 0 by A1, Th81;

then a #R (s1 . m) < a #R ((lim s1) + 1) by A13, ABSVALUE:def 1;

hence contradiction by A1, A5, A12, Th84; :: thesis: verum

A14: now :: thesis: for n being Nat holds (s2 ") . n = (1 / a) #R (s1 . n)

a * (1 / a) <= 1 * (1 / a)
by A1, A5, XREAL_1:64;let n be Nat; :: thesis: (s2 ") . n = (1 / a) #R (s1 . n)

thus (s2 ") . n = (s2 . n) " by VALUED_1:10

.= (a #R (s1 . n)) " by A4

.= 1 / (a #R (s1 . n))

.= (1 / a) #R (s1 . n) by A1, Th79 ; :: thesis: verum

end;thus (s2 ") . n = (s2 . n) " by VALUED_1:10

.= (a #R (s1 . n)) " by A4

.= 1 / (a #R (s1 . n))

.= (1 / a) #R (s1 . n) by A1, Th79 ; :: thesis: verum

then A15: 1 <= 1 / a by A1, XCMPLX_1:106;

A16: a #R (lim s1) <> 0 by A1, Th81;

now :: thesis: for n being Nat holds s2 . n <> 0

then A17:
s2 is non-zero
by SEQ_1:5;let n be Nat; :: thesis: s2 . n <> 0

s2 . n = a #R (s1 . n) by A4;

hence s2 . n <> 0 by A1, Th81; :: thesis: verum

end;s2 . n = a #R (s1 . n) by A4;

hence s2 . n <> 0 by A1, Th81; :: thesis: verum

then A18: lim (s2 ") = (lim s2) " by A3, A6, SEQ_2:22;

s2 " is convergent by A3, A6, A17, SEQ_2:21;

then (lim s2) " = (1 / a) #R (lim s1) by A2, A15, A18, A14, Lm12

.= 1 / (a #R (lim s1)) by A1, Th79 ;

then 1 = (1 / (a #R (lim s1))) * (lim s2) by A6, XCMPLX_0:def 7;

then a #R (lim s1) = (a #R (lim s1)) * ((1 / (a #R (lim s1))) * (lim s2))

.= ((a #R (lim s1)) * (1 / (a #R (lim s1)))) * (lim s2)

.= 1 * (lim s2) by A16, XCMPLX_1:106 ;

hence lim s2 = a #R (lim s1) ; :: thesis: verum