:: The Sum and Product of Finite Sequences of Complex Numbers
:: by Keiichi Miyajima and Takahiro Kato
::
:: Received January 12, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users

definition

let F be complex-valued Relation;
:: original: rng
redefine func rng F -> Subset of COMPLEX;
coherence
rng F is Subset of COMPLEX by VALUED_0:def 1;

end;

registration

let D be non empty set ;
let F be Function of COMPLEX,D;
let F1 be complex-valued FinSequence;

cluster F1 (#) F -> FinSequence-like ;

coherence
F * F1 is FinSequence-like

proof end;

end;

definition

func sqrcomplex -> UnOp of COMPLEX means :Def1: :: RVSUM_2:def 1
for c being Complex holds it . c = c ^2 ;

existence
ex b₁ being UnOp of COMPLEX st
for c being Complex holds b₁ . c = c ^2

proof end;

uniqueness
for b₁, b₂ being UnOp of COMPLEX st ( for c being Complex holds b₁ . c = c ^2 ) & ( for c being Complex holds b₂ . c = c ^2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines sqrcomplex RVSUM_2:def 1 :
for b₁ being UnOp of COMPLEX holds
( b₁ = sqrcomplex iff for c being Complex holds b₁ . c = c ^2 );

theorem :: RVSUM_2:1

sqrcomplex is_distributive_wrt multcomplex

proof end;

Lm1: for c, c1 being Complex holds (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1

proof end;

theorem :: RVSUM_2:2

for c being Complex holds c multcomplex is_distributive_wrt addcomplex

proof end;

Lm2: for F being complex-valued FinSequence holds F is FinSequence of COMPLEX

proof end;

definition

let F1, F2 be complex-valued FinSequence;

:: original: +
redefine func F1 + F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 2
addcomplex .: (F1,F2);

coherence
F1 + F2 is FinSequence of COMPLEX by Lm2;
compatibility
for b₁ being FinSequence of COMPLEX holds
( b₁ = F1 + F2 iff b₁ = addcomplex .: (F1,F2) )

proof end;

commutativity
for b₁ being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b₁ = addcomplex .: (F1,F2) holds
b₁ = addcomplex .: (F2,F1)

proof end;

end;

:: deftheorem defines + RVSUM_2:def 2 :
for F1, F2 being complex-valued FinSequence holds F1 + F2 = addcomplex .: (F1,F2);

definition

let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: +
redefine func R1 + R2 -> Element of i -tuples_on COMPLEX;
coherence
R1 + R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120;

end;

theorem :: RVSUM_2:3

for s being set
for i being Nat
for R1, R2 being b₂ -element FinSequence of COMPLEX holds (R1 + R2) . s = (R1 . s) + (R2 . s)

proof end;

theorem :: RVSUM_2:4

for F being complex-valued FinSequence holds (<*> COMPLEX) + F = <*> COMPLEX

proof end;

theorem :: RVSUM_2:5

for c1, c2 being Complex holds <*c1*> + <*c2*> = <*(c1 + c2)*>

proof end;

theorem :: RVSUM_2:6

for i being Nat
for c1, c2 being Complex holds (i |-> c1) + (i |-> c2) = i |-> (c1 + c2)

proof end;

definition

let F be complex-valued FinSequence;

:: original: -
redefine func - F -> FinSequence of COMPLEX equals :: RVSUM_2:def 3
compcomplex * F;

coherence
- F is FinSequence of COMPLEX by Lm2;
compatibility
for b₁ being FinSequence of COMPLEX holds
( b₁ = - F iff b₁ = compcomplex * F )

proof end;

end;

:: deftheorem defines - RVSUM_2:def 3 :
for F being complex-valued FinSequence holds - F = compcomplex * F;

definition

let i be Nat;
let R be i -element FinSequence of COMPLEX ;
:: original: -
redefine func - R -> Element of i -tuples_on COMPLEX;
coherence
- R is Element of i -tuples_on COMPLEX by FINSEQ_2:113;

end;

theorem :: RVSUM_2:7

for c being Complex holds - <*c*> = <*(- c)*>

proof end;

theorem Th8: :: RVSUM_2:8

for i being Nat
for c being Complex holds - (i |-> c) = i |-> (- c)

proof end;

theorem :: RVSUM_2:9

for i being Nat
for R, R1, R2 being b₁ -element FinSequence of COMPLEX st R1 + R = R2 + R holds
R1 = R2

proof end;

theorem Th10: :: RVSUM_2:10

for F1, F2 being complex-valued FinSequence holds - (F1 + F2) = (- F1) + (- F2)

proof end;

definition

let F1, F2 be complex-valued FinSequence;

:: original: -
redefine func F1 - F2 -> FinSequence of COMPLEX equals :: RVSUM_2:def 4
diffcomplex .: (F1,F2);

coherence
F1 - F2 is FinSequence of COMPLEX by Lm2;
compatibility
for b₁ being FinSequence of COMPLEX holds
( b₁ = F1 - F2 iff b₁ = diffcomplex .: (F1,F2) )

proof end;

end;

:: deftheorem defines - RVSUM_2:def 4 :
for F1, F2 being complex-valued FinSequence holds F1 - F2 = diffcomplex .: (F1,F2);

definition

let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: -
redefine func R1 - R2 -> Element of i -tuples_on COMPLEX;
coherence
R1 - R2 is Element of i -tuples_on COMPLEX by FINSEQ_2:120;

end;

theorem :: RVSUM_2:11

for s being set
for i being Nat
for R1, R2 being b₂ -element FinSequence of COMPLEX holds (R1 - R2) . s = (R1 . s) - (R2 . s)

proof end;

theorem :: RVSUM_2:12

for F being complex-valued FinSequence holds
( (<*> COMPLEX) - F = <*> COMPLEX & F - (<*> COMPLEX) = <*> COMPLEX )

proof end;

theorem :: RVSUM_2:13

for c1, c2 being Complex holds <*c1*> - <*c2*> = <*(c1 - c2)*>

proof end;

theorem :: RVSUM_2:14

for i being Nat
for c1, c2 being Complex holds (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)

proof end;

theorem :: RVSUM_2:15

for i being Nat
for R being b₁ -element FinSequence of COMPLEX holds R - (i |-> 0c) = R

proof end;

theorem :: RVSUM_2:16

for F1, F2 being complex-valued FinSequence holds - (F1 - F2) = F2 - F1

proof end;

theorem :: RVSUM_2:17

for F1, F2 being complex-valued FinSequence holds - (F1 - F2) = (- F1) + F2

proof end;

theorem :: RVSUM_2:18

for i being Nat
for R1, R2 being b₁ -element FinSequence of COMPLEX st R1 - R2 = i |-> 0c holds
R1 = R2

proof end;

theorem :: RVSUM_2:19

for i being Nat
for R, R1 being b₁ -element FinSequence of COMPLEX holds R1 = (R1 + R) - R

proof end;

theorem :: RVSUM_2:20

for i being Nat
for R, R1 being b₁ -element FinSequence of COMPLEX holds R1 = (R1 - R) + R

proof end;

notation

let F be complex-valued FinSequence;
let c be Complex;
synonym c * F for c (#) F;

end;

definition

let F be complex-valued FinSequence;
let c be Complex;

:: original: *
redefine func c * F -> FinSequence of COMPLEX equals :: RVSUM_2:def 5
(c multcomplex) * F;

coherence
c * F is FinSequence of COMPLEX by Lm2;
compatibility
for b₁ being FinSequence of COMPLEX holds
( b₁ = c * F iff b₁ = (c multcomplex) * F )

proof end;

end;

:: deftheorem defines * RVSUM_2:def 5 :
for F being complex-valued FinSequence
for c being Complex holds c * F = (c multcomplex) * F;

definition

let i be Nat;
let R be i -element FinSequence of COMPLEX ;
let c be Complex;
:: original: *
redefine func c * R -> Element of i -tuples_on COMPLEX;
coherence
c * R is Element of i -tuples_on COMPLEX by FINSEQ_2:113;

end;

theorem :: RVSUM_2:21

for c, c1 being Complex holds c * <*c1*> = <*(c * c1)*>

proof end;

theorem Th22: :: RVSUM_2:22

for i being Nat
for c1, c2 being Complex holds c1 * (i |-> c2) = i |-> (c1 * c2)

proof end;

theorem :: RVSUM_2:23

for c1, c2 being Complex
for F being complex-valued FinSequence holds (c1 + c2) * F = (c1 * F) + (c2 * F)

proof end;

theorem :: RVSUM_2:24

for i being Nat
for R being b₁ -element FinSequence of COMPLEX holds 0c * R = i |-> 0c

proof end;

notation

let F1, F2 be complex-valued FinSequence;
synonym mlt (F1,F2) for F1 (#) F2;

end;

definition

let F1, F2 be complex-valued FinSequence;

:: original: mlt
redefine func mlt (F1,F2) -> FinSequence of COMPLEX equals :: RVSUM_2:def 6
multcomplex .: (F1,F2);

coherence
mlt (F1,F2) is FinSequence of COMPLEX by Lm2;
compatibility
for b₁ being FinSequence of COMPLEX holds
( b₁ = mlt (F1,F2) iff b₁ = multcomplex .: (F1,F2) )

proof end;

commutativity
for b₁ being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b₁ = multcomplex .: (F1,F2) holds
b₁ = multcomplex .: (F2,F1)

proof end;

end;

:: deftheorem defines mlt RVSUM_2:def 6 :
for F1, F2 being complex-valued FinSequence holds mlt (F1,F2) = multcomplex .: (F1,F2);

definition

let i be Nat;
let R1, R2 be i -element FinSequence of COMPLEX ;
:: original: mlt
redefine func mlt (R1,R2) -> Element of i -tuples_on COMPLEX;
coherence
mlt (R1,R2) is Element of i -tuples_on COMPLEX by FINSEQ_2:120;

end;

theorem :: RVSUM_2:25

for F being complex-valued FinSequence holds mlt ((<*> COMPLEX),F) = <*> COMPLEX

proof end;

theorem :: RVSUM_2:26

for c1, c2 being Complex holds mlt (<*c1*>,<*c2*>) = <*(c1 * c2)*>

proof end;

theorem Th27: :: RVSUM_2:27

for i being Nat
for c being Complex
for R being b₁ -element FinSequence of COMPLEX holds mlt ((i |-> c),R) = c * R

proof end;

theorem :: RVSUM_2:28

for i being Nat
for c1, c2 being Complex holds mlt ((i |-> c1),(i |-> c2)) = i |-> (c1 * c2)

proof end;

theorem Th29: :: RVSUM_2:29

Sum (<*> COMPLEX) = 0c by BINOP_2:1, FINSOP_1:10;

registration

let f be empty FinSequence;

cluster Sum f -> zero ;

coherence
Sum f is zero by Th29;

end;

theorem :: RVSUM_2:30

for c being Complex holds Sum <*c*> = c

proof end;

theorem Th31: :: RVSUM_2:31

for c being Complex
for F being complex-valued FinSequence holds Sum (F ^ <*c*>) = (Sum F) + c

proof end;

theorem Th32: :: RVSUM_2:32

for F1, F2 being complex-valued FinSequence holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)

proof end;

theorem :: RVSUM_2:33

for c being Complex
for F being complex-valued FinSequence holds Sum (<*c*> ^ F) = c + (Sum F)

proof end;

theorem Th34: :: RVSUM_2:34

for c1, c2 being Complex holds Sum <*c1,c2*> = c1 + c2

proof end;

theorem :: RVSUM_2:35

for c1, c2, c3 being Complex holds Sum <*c1,c2,c3*> = (c1 + c2) + c3

proof end;

theorem Th36: :: RVSUM_2:36

for i being Nat
for c being Complex holds Sum (i |-> c) = i * c

proof end;

theorem :: RVSUM_2:37

for i being Nat holds Sum (i |-> 0c) = 0c

proof end;

theorem :: RVSUM_2:38

for c being Complex
for F being complex-valued FinSequence holds Sum (c * F) = c * (Sum F)

proof end;

theorem Th39: :: RVSUM_2:39

for F being complex-valued FinSequence holds Sum (- F) = - (Sum F)

proof end;

theorem Th40: :: RVSUM_2:40

for i being Nat
for R1, R2 being b₁ -element FinSequence of COMPLEX holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

proof end;

theorem :: RVSUM_2:41

for i being Nat
for R1, R2 being b₁ -element FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

proof end;

Lm3: for F being empty FinSequence holds Product F = 1

proof end;

theorem Th42: :: RVSUM_2:42

Product (<*> COMPLEX) = 1 by Lm3;

registration

let f be empty FinSequence;

reduce 1 * (Product f) to 1;

reducibility
1 * (Product f) = 1 by Th42;

end;

theorem :: RVSUM_2:43

for c being Complex
for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * (Product F)

proof end;

theorem :: RVSUM_2:44

for R being Element of 0 -tuples_on COMPLEX holds Product R = 1 by Lm3;

theorem :: RVSUM_2:45

for i, j being Nat
for c being Complex holds Product ((i + j) |-> c) = (Product (i |-> c)) * (Product (j |-> c))

proof end;

theorem :: RVSUM_2:46

for i, j being Nat
for c being Complex holds Product ((i * j) |-> c) = Product (j |-> (Product (i |-> c)))

proof end;

theorem :: RVSUM_2:47

for i being Nat
for c1, c2 being Complex holds Product (i |-> (c1 * c2)) = (Product (i |-> c1)) * (Product (i |-> c2))

proof end;

theorem Th48: :: RVSUM_2:48

for i being Nat
for R1, R2 being b₁ -element FinSequence of COMPLEX holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)

proof end;

theorem :: RVSUM_2:49

for i being Nat
for c being Complex
for R being b₁ -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * (Product R)

proof end;

theorem :: RVSUM_2:50

for x being complex-valued FinSequence holds len (- x) = len x

proof end;

theorem :: RVSUM_2:51

for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 + x2) = len x1

proof end;

theorem :: RVSUM_2:52

for x1, x2 being complex-valued FinSequence st len x1 = len x2 holds
len (x1 - x2) = len x1

proof end;

theorem :: RVSUM_2:53

for a being Real
for x being complex-valued FinSequence holds len (a * x) = len x

proof end;

theorem :: RVSUM_2:54

for x, y, z being complex-valued FinSequence st len x = len y & len y = len z holds
mlt ((x + y),z) = (mlt (x,z)) + (mlt (y,z))

proof end;