:: Complex Sequences
:: by Agnieszka Banachowicz and Anna Winnicka
::
:: Received November 5, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users


definition
mode Complex_Sequence is sequence of COMPLEX;
end;

theorem Th1: :: COMSEQ_1:1
for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of COMPLEX ) ) )
proof end;

theorem Th2: :: COMSEQ_1:2
for f being Function holds
( f is Complex_Sequence iff ( dom f = NAT & ( for n being Element of NAT holds f . n is Element of COMPLEX ) ) )
proof end;

scheme :: COMSEQ_1:sch 1
ExComplexSeq{ F1( set ) -> Complex } :
ex seq being Complex_Sequence st
for n being Nat holds seq . n = F1(n)
proof end;

registration
cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEX ) non-zero V44() for Element of bool [:NAT,COMPLEX:];
existence
ex b1 being Complex_Sequence st b1 is non-zero
proof end;
end;

theorem Th3: :: COMSEQ_1:3
for seq being Complex_Sequence holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0c )
proof end;

theorem Th4: :: COMSEQ_1:4
for seq being Complex_Sequence holds
( seq is non-zero iff for n being Element of NAT holds seq . n <> 0c )
proof end;

theorem :: COMSEQ_1:5
for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c} by ORDINAL1:def 15, ZFMISC_1:34;

theorem :: COMSEQ_1:6
for r being Complex ex seq being Complex_Sequence st rng seq = {r}
proof end;

theorem Th7: :: COMSEQ_1:7
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3)
proof end;

theorem Th8: :: COMSEQ_1:8
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3)
proof end;

theorem Th9: :: COMSEQ_1:9
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 + seq2) (#) seq3 = (seq1 (#) seq3) + (seq2 (#) seq3)
proof end;

theorem :: COMSEQ_1:10
for seq1, seq2, seq3 being Complex_Sequence holds seq3 (#) (seq1 + seq2) = (seq3 (#) seq1) + (seq3 (#) seq2) by Th9;

theorem :: COMSEQ_1:11
for seq being Complex_Sequence holds - seq = (- 1r) (#) seq ;

theorem Th12: :: COMSEQ_1:12
for r being Complex
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = (r (#) seq1) (#) seq2
proof end;

theorem Th13: :: COMSEQ_1:13
for r being Complex
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2)
proof end;

theorem Th14: :: COMSEQ_1:14
for seq1, seq2, seq3 being Complex_Sequence holds (seq1 - seq2) (#) seq3 = (seq1 (#) seq3) - (seq2 (#) seq3)
proof end;

theorem :: COMSEQ_1:15
for seq1, seq2, seq3 being Complex_Sequence holds (seq3 (#) seq1) - (seq3 (#) seq2) = seq3 (#) (seq1 - seq2) by Th14;

theorem Th16: :: COMSEQ_1:16
for r being Complex
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 + seq2) = (r (#) seq1) + (r (#) seq2)
proof end;

theorem Th17: :: COMSEQ_1:17
for r, p being Complex
for seq being Complex_Sequence holds (r * p) (#) seq = r (#) (p (#) seq)
proof end;

theorem Th18: :: COMSEQ_1:18
for r being Complex
for seq1, seq2 being Complex_Sequence holds r (#) (seq1 - seq2) = (r (#) seq1) - (r (#) seq2)
proof end;

theorem :: COMSEQ_1:19
for r being Complex
for seq, seq1 being Complex_Sequence holds r (#) (seq1 /" seq) = (r (#) seq1) /" seq
proof end;

theorem :: COMSEQ_1:20
for seq1, seq2, seq3 being Complex_Sequence holds seq1 - (seq2 + seq3) = (seq1 - seq2) - seq3
proof end;

theorem :: COMSEQ_1:21
for seq being Complex_Sequence holds 1r (#) seq = seq
proof end;

theorem :: COMSEQ_1:22
for seq being Complex_Sequence holds - (- seq) = seq ;

theorem :: COMSEQ_1:23
for seq1, seq2 being Complex_Sequence holds seq1 - (- seq2) = seq1 + seq2 ;

theorem :: COMSEQ_1:24
for seq1, seq2, seq3 being Complex_Sequence holds seq1 - (seq2 - seq3) = (seq1 - seq2) + seq3
proof end;

theorem :: COMSEQ_1:25
for seq1, seq2, seq3 being Complex_Sequence holds seq1 + (seq2 - seq3) = (seq1 + seq2) - seq3
proof end;

theorem :: COMSEQ_1:26
for seq1, seq2 being Complex_Sequence holds
( (- seq1) (#) seq2 = - (seq1 (#) seq2) & seq1 (#) (- seq2) = - (seq1 (#) seq2) ) by Th12;

theorem Th27: :: COMSEQ_1:27
for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero
proof end;

theorem :: COMSEQ_1:28
canceled;

::$CT
theorem Th28: :: COMSEQ_1:29
for seq, seq1 being Complex_Sequence holds
( ( seq is non-zero & seq1 is non-zero ) iff seq (#) seq1 is non-zero )
proof end;

theorem Th29: :: COMSEQ_1:30
for seq, seq1 being Complex_Sequence holds (seq ") (#) (seq1 ") = (seq (#) seq1) "
proof end;

theorem :: COMSEQ_1:31
for seq, seq1 being Complex_Sequence st seq is non-zero holds
(seq1 /" seq) (#) seq = seq1
proof end;

theorem :: COMSEQ_1:32
for seq, seq1, seq9, seq19 being Complex_Sequence holds (seq9 /" seq) (#) (seq19 /" seq1) = (seq9 (#) seq19) /" (seq (#) seq1)
proof end;

theorem :: COMSEQ_1:33
for seq, seq1 being Complex_Sequence st seq is non-zero & seq1 is non-zero holds
seq /" seq1 is non-zero
proof end;

theorem Th33: :: COMSEQ_1:34
for seq, seq1 being Complex_Sequence holds (seq /" seq1) " = seq1 /" seq
proof end;

theorem :: COMSEQ_1:35
for seq, seq1, seq2 being Complex_Sequence holds seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq
proof end;

theorem :: COMSEQ_1:36
for seq, seq1, seq2 being Complex_Sequence holds seq2 /" (seq /" seq1) = (seq2 (#) seq1) /" seq
proof end;

theorem Th36: :: COMSEQ_1:37
for seq, seq1, seq2 being Complex_Sequence st seq1 is non-zero holds
seq2 /" seq = (seq2 (#) seq1) /" (seq (#) seq1)
proof end;

theorem Th37: :: COMSEQ_1:38
for r being Complex
for seq being Complex_Sequence st r <> 0c & seq is non-zero holds
r (#) seq is non-zero
proof end;

theorem :: COMSEQ_1:39
for seq being Complex_Sequence st seq is non-zero holds
- seq is non-zero by Th37;

theorem Th39: :: COMSEQ_1:40
for r being Complex
for seq being Complex_Sequence holds (r (#) seq) " = (r ") (#) (seq ")
proof end;

theorem Th40: :: COMSEQ_1:41
for seq being Complex_Sequence st seq is non-zero holds
(- seq) " = (- 1r) (#) (seq ")
proof end;

theorem :: COMSEQ_1:42
for seq, seq1 being Complex_Sequence st seq is non-zero holds
( - (seq1 /" seq) = (- seq1) /" seq & seq1 /" (- seq) = - (seq1 /" seq) )
proof end;

theorem :: COMSEQ_1:43
for seq, seq1, seq19 being Complex_Sequence holds
( (seq1 /" seq) + (seq19 /" seq) = (seq1 + seq19) /" seq & (seq1 /" seq) - (seq19 /" seq) = (seq1 - seq19) /" seq )
proof end;

theorem :: COMSEQ_1:44
for seq, seq1, seq9, seq19 being Complex_Sequence st seq is non-zero & seq9 is non-zero holds
( (seq1 /" seq) + (seq19 /" seq9) = ((seq1 (#) seq9) + (seq19 (#) seq)) /" (seq (#) seq9) & (seq1 /" seq) - (seq19 /" seq9) = ((seq1 (#) seq9) - (seq19 (#) seq)) /" (seq (#) seq9) )
proof end;

theorem :: COMSEQ_1:45
for seq, seq1, seq9, seq19 being Complex_Sequence holds (seq19 /" seq) /" (seq9 /" seq1) = (seq19 (#) seq1) /" (seq (#) seq9)
proof end;

theorem Th45: :: COMSEQ_1:46
for seq, seq9 being Complex_Sequence holds |.(seq (#) seq9).| = |.seq.| (#) |.seq9.|
proof end;

theorem :: COMSEQ_1:47
canceled;

::$CT
theorem Th46: :: COMSEQ_1:48
for seq being Complex_Sequence holds |.seq.| " = |.(seq ").|
proof end;

theorem :: COMSEQ_1:49
for seq, seq9 being Complex_Sequence holds |.(seq9 /" seq).| = |.seq9.| /" |.seq.|
proof end;

theorem :: COMSEQ_1:50
for r being Complex
for seq being Complex_Sequence holds |.(r (#) seq).| = |.r.| (#) |.seq.|
proof end;