:: Complex Sequences
::  by Agnieszka Banachowicz and Anna Winnicka
::
:: Received November 5, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies FUNCT_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, TARSKI, XCMPLX_0,
      VALUED_0, FUNCOP_1, COMPLEX1, CARD_1, XBOOLE_0, ARYTM_3, VALUED_1,
      ARYTM_1, COMSEQ_1, ZFMISC_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, COMPLEX1,
      RELAT_1, ZFMISC_1, FUNCT_1, NAT_1, RELSET_1, FUNCOP_1, VALUED_1;
 constructors PARTFUN1, FUNCOP_1, REAL_1, COMPLEX1, VALUED_1, RELSET_1,
      VALUED_0;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, MEMBERED,
      VALUED_0, VALUED_1, XCMPLX_0, XREAL_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve f for Function;
reserve n,k,n1 for Element of NAT;
reserve r,p for Complex;
reserve x,y for set;

definition
  mode Complex_Sequence is sequence of COMPLEX;
end;

reserve seq,seq1,seq2,seq3,seq9,seq19 for Complex_Sequence;

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

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

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

registration
  cluster non-zero for Complex_Sequence;
end;

theorem :: COMSEQ_1:3
  seq is non-zero iff for x st x in NAT holds seq.x<>0c;

theorem :: COMSEQ_1:4
  seq is non-zero iff for n holds seq.n<>0c;

theorem :: COMSEQ_1:5
  for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c};

theorem :: COMSEQ_1:6
  for r ex seq st rng seq={r};

theorem :: COMSEQ_1:7
  (seq1+seq2)+seq3=seq1+(seq2+seq3);

theorem :: COMSEQ_1:8
  (seq1(#)seq2)(#)seq3=seq1(#)(seq2(#)seq3);

theorem :: COMSEQ_1:9
  (seq1+seq2)(#)seq3=seq1(#)seq3+seq2(#)seq3;

theorem :: COMSEQ_1:10
  seq3(#)(seq1+seq2)=seq3(#)seq1+seq3(#)seq2;

theorem :: COMSEQ_1:11
  -seq=(-1r)(#)seq;

theorem :: COMSEQ_1:12
  r(#)(seq1(#)seq2)=r(#)seq1(#)seq2;

theorem :: COMSEQ_1:13
  r(#)(seq1(#)seq2)=seq1(#)(r(#)seq2);

theorem :: COMSEQ_1:14
  (seq1-seq2)(#)seq3=seq1(#)seq3-seq2(#)seq3;

theorem :: COMSEQ_1:15
  seq3(#)seq1-seq3(#)seq2=seq3(#)(seq1-seq2);

theorem :: COMSEQ_1:16
  r(#)(seq1+seq2)=r(#)seq1+r(#)seq2;

theorem :: COMSEQ_1:17
  (r*p)(#)seq=r(#)(p(#)seq);

theorem :: COMSEQ_1:18
  r(#)(seq1-seq2)=r(#)seq1-r(#)seq2;

theorem :: COMSEQ_1:19
  r(#)(seq1/"seq)=(r(#)seq1)/"seq;

theorem :: COMSEQ_1:20
  seq1-(seq2+seq3)=seq1-seq2-seq3;

theorem :: COMSEQ_1:21
  1r(#)seq=seq;

theorem :: COMSEQ_1:22
  --seq = seq;

theorem :: COMSEQ_1:23
  seq1 - (-seq2) = seq1 + seq2;

theorem :: COMSEQ_1:24
  seq1 - (seq2 - seq3) = seq1 - seq2 + seq3;

theorem :: COMSEQ_1:25
  seq1 + (seq2 - seq3) = seq1 + seq2 - seq3;

theorem :: COMSEQ_1:26
  (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2);

theorem :: COMSEQ_1:27
  seq is non-zero implies seq" is non-zero;

::$CT

theorem :: COMSEQ_1:29
  seq is non-zero & seq1 is non-zero iff seq(#)seq1 is non-zero;

theorem :: COMSEQ_1:30
  seq"(#)seq1"=(seq(#)seq1)";

theorem :: COMSEQ_1:31
  seq is non-zero implies (seq1/"seq)(#)seq=seq1;

theorem :: COMSEQ_1:32
  (seq9/"seq)(#)(seq19/"seq1)=(seq9(#)seq19)/"(seq(#)seq1);

theorem :: COMSEQ_1:33
  seq is non-zero & seq1 is non-zero implies seq/"seq1 is non-zero;

theorem :: COMSEQ_1:34
  (seq/"seq1)"=seq1/"seq;

theorem :: COMSEQ_1:35
  seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq;

theorem :: COMSEQ_1:36
  seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq;

theorem :: COMSEQ_1:37
  seq1 is non-zero implies seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1);

theorem :: COMSEQ_1:38
  r<>0c & seq is non-zero implies r(#)seq is non-zero;

theorem :: COMSEQ_1:39
  seq is non-zero implies -seq is non-zero;

theorem :: COMSEQ_1:40
  (r(#)seq)"=r"(#)seq";

theorem :: COMSEQ_1:41
  seq is non-zero implies (-seq)"=(-1r)(#)seq";

theorem :: COMSEQ_1:42
  seq is non-zero implies -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/" seq;

theorem :: COMSEQ_1:43
  seq1/"seq + seq19/"seq = (seq1+seq19) /" seq & seq1/"seq - seq19/"seq
  = (seq1-seq19) /" seq;

theorem :: COMSEQ_1:44
  seq is non-zero & seq9 is non-zero implies seq1/"seq + seq19/"seq9=(
seq1(#)seq9+seq19(#)seq)/"(seq(#)seq9) & seq1/"seq - seq19/"seq9=(seq1(#)seq9-
  seq19(#)seq)/"(seq(#)seq9);

theorem :: COMSEQ_1:45
  (seq19/"seq)/"(seq9/"seq1)=(seq19(#)seq1)/"(seq(#)seq9);

theorem :: COMSEQ_1:46
  |.seq(#)seq9.|=|.seq.|(#)|.seq9.|;

::$CT

theorem :: COMSEQ_1:48
  |. seq .| " = |. seq" .|;

theorem :: COMSEQ_1:49
  |.seq9/"seq.|=|.seq9.|/"|.seq.|;

theorem :: COMSEQ_1:50
  |.r(#)seq.|=|.r.|(#)|.seq.|;