let a, b be Real_Sequence; :: thesis: for c being Complex_Sequence st ( for n being Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds
( ( a is convergent & b is convergent ) iff c is convergent )
let c be Complex_Sequence; :: thesis: ( ( for n being Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ) implies ( ( a is convergent & b is convergent ) iff c is convergent ) )
assume A1: for n being Element of NAT holds
( Re (c . n) = a . n & Im (c . n) = b . n ) ; :: thesis: ( ( a is convergent & b is convergent ) iff c is convergent )
thus ( a is convergent & b is convergent implies c is convergent ) :: thesis: ( c is convergent implies ( a is convergent & b is convergent ) )

proof

assume that
A2: a is convergent and
A3: b is convergent ; :: thesis: c is convergent
consider a1 being real number such that
A4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((a . m) - a1) < p by A2, SEQ_2:def 6;
consider b1 being real number such that
A5: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((b . m) - b1) < p by A3, SEQ_2:def 6;
reconsider a1 = a1, b1 = b1 as Real by XREAL_0:def 1;
reconsider g = a1 + (b1 * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
take g ; :: according to COMSEQ_2:def 4 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.((c . b₃) - g).| ) )
for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p )
assume A6: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p
then consider n1 being Element of NAT such that
A7: for m being Element of NAT st n1 <= m holds
abs ((a . m) - a1) < p / 2 by A4;
consider n2 being Element of NAT such that
A8: for m being Element of NAT st n2 <= m holds
abs ((b . m) - b1) < p / 2 by A5, A6;
( n1 <= n1 + n2 & n2 <= n1 + n2 ) by NAT_1:11;
then consider n being Element of NAT such that
A9: n1 <= n and
A10: n2 <= n ;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p
for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p

proof

let m be Element of NAT ; :: thesis: ( n <= m implies |.((c . m) - g).| < p )
( Re (c . m) = a . m & Re g = a1 ) by A1, COMPLEX1:12;
then A11: Re ((c . m) - g) = (a . m) - a1 by COMPLEX1:19;
( Im (c . m) = b . m & Im g = b1 ) by A1, COMPLEX1:12;
then A12: Im ((c . m) - g) = (b . m) - b1 by COMPLEX1:19;
assume A13: n <= m ; :: thesis: |.((c . m) - g).| < p
then n2 <= m by A10, XXREAL_0:2;
then A14: abs ((b . m) - b1) < p / 2 by A8;
n1 <= m by A9, A13, XXREAL_0:2;
then abs ((a . m) - a1) < p / 2 by A7;
then A15: (abs ((a . m) - a1)) + (abs ((b . m) - b1)) < (p / 2) + (p / 2) by A14, XREAL_1:8;
|.((c . m) - g).| <= (abs (Re ((c . m) - g))) + (abs (Im ((c . m) - g))) by Th12;
hence |.((c . m) - g).| < p by A15, A11, A12, XXREAL_0:2; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
|.((c . m) - g).| < p ; :: thesis: verum

end;

hence for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= |.((c . b₃) - g).| ) ) ; :: thesis: verum

end;

assume c is convergent ; :: thesis: ( a is convergent & b is convergent )
then consider z being Element of COMPLEX such that
A16: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((c . m) - z).| < p by COMSEQ_2:def 4;
thus a is convergent :: thesis: b is convergent

proof

reconsider z = z as Element of COMPLEX ;
take Re z ; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((a . b₃) - (Re z)) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((a . b₂) - (Re z)) ) )
assume A17: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((a . b₂) - (Re z)) )
p is Real by XREAL_0:def 1;
then consider n being Element of NAT such that
A18: for m being Element of NAT st n <= m holds
|.((c . m) - z).| < p by A16, A17;
take n ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs ((a . b₁) - (Re z)) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs ((a . m) - (Re z)) )
assume n <= m ; :: thesis: not p <= abs ((a . m) - (Re z))
then A19: |.((c . m) - z).| < p by A18;
( Re (c . m) = a . m & Re ((c . m) - z) = (Re (c . m)) - (Re z) ) by A1, COMPLEX1:19;
then abs ((a . m) - (Re z)) <= |.((c . m) - z).| by Th13;
hence not p <= abs ((a . m) - (Re z)) by A19, XXREAL_0:2; :: thesis: verum

end;

take Im z ; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((b . b₃) - (Im z)) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((b . b₂) - (Im z)) ) )
assume A20: p > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((b . b₂) - (Im z)) )
p is Real by XREAL_0:def 1;
then consider n being Element of NAT such that
A21: for m being Element of NAT st n <= m holds
|.((c . m) - z).| < p by A16, A20;
take n ; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs ((b . b₁) - (Im z)) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs ((b . m) - (Im z)) )
assume n <= m ; :: thesis: not p <= abs ((b . m) - (Im z))
then A22: |.((c . m) - z).| < p by A21;
A23: Im ((c . m) - z) = (Im (c . m)) - (Im z) by COMPLEX1:19;
Im (c . m) = b . m by A1;
then abs ((b . m) - (Im z)) <= |.((c . m) - z).| by A23, Th13;
hence not p <= abs ((b . m) - (Im z)) by A22, XXREAL_0:2; :: thesis: verum