:: The Sum and Product of Finite Sequences of Complex Numbers
:: by Keiichi Miyajima and Takahiro Kato
::
:: Copyright (c) 2010-2019 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;
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 b1 being UnOp of COMPLEX st
for c being Complex holds b1 . c = c ^2
proof end;
uniqueness
for b1, b2 being UnOp of COMPLEX st ( for c being Complex holds b1 . c = c ^2 ) & ( for c being Complex holds b2 . c = c ^2 ) holds
b1 = b2
proof end;
end;

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

theorem :: RVSUM_2:1
proof end;

Lm1: for c, c1 being Complex holds (multcomplex [;] (c,())) . 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
coherence
F1 + F2 is FinSequence of COMPLEX
by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = F1 + F2 iff b1 = addcomplex .: (F1,F2) )
proof end;
commutativity
for b1 being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b1 = addcomplex .: (F1,F2) holds
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 b2 -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 () + 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 b1 being FinSequence of COMPLEX holds
( b1 = - F iff b1 = 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 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 b1 -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 b1 being FinSequence of COMPLEX holds
( b1 = F1 - F2 iff b1 = 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 b2 -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
( () - F = <*> COMPLEX & F - () = <*> 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 b1 -element FinSequence of COMPLEX holds R - () = 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 b1 -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 b1 -element FinSequence of COMPLEX holds R1 = (R1 + R) - R
proof end;

theorem :: RVSUM_2:20
for i being Nat
for R, R1 being b1 -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
() * F;
coherence
c * F is FinSequence of COMPLEX
by Lm2;
compatibility
for b1 being FinSequence of COMPLEX holds
( b1 = c * F iff b1 = () * F )
proof end;
end;

:: deftheorem defines * RVSUM_2:def 5 :
for F being complex-valued FinSequence
for c being Complex holds c * F = () * 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 b1 -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 b1 being FinSequence of COMPLEX holds
( b1 = mlt (F1,F2) iff b1 = multcomplex .: (F1,F2) )
proof end;
commutativity
for b1 being FinSequence of COMPLEX
for F1, F2 being complex-valued FinSequence st b1 = multcomplex .: (F1,F2) holds
b1 = 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 ((),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 b1 -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

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 () = 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 b1 -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 b1 -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 () = 1 by Lm3;

registration
let f be empty FinSequence;
reduce 1 * () to 1;
reducibility
1 * () = 1
by Th42;
end;

theorem :: RVSUM_2:43
for c being Complex
for F being complex-valued FinSequence holds Product (<*c*> ^ F) = c * ()
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 b1 -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 b1 -element FinSequence of COMPLEX holds Product (c * R) = (Product (i |-> c)) * ()
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;