:: The Sum and Product of Finite Sequences of Real Numbers
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1990
:: Copyright (c) 1990 Association of Mizar Users

begin

registration

let n be Nat;
cluster Relation-like Function-like natural-valued V59() FinSequence-like FinSubsequence-like n -long set ;
existence
ex b₁ being FinSequence st
( b₁ is n -long & b₁ is natural-valued )

proof end;

end;

registration

cluster Relation-like Function-like real-valued V59() FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st b₁ is real-valued

proof end;

end;

definition

let F be real-valued Relation;
:: original: proj2
redefine func rng F -> Subset of REAL;
coherence
proj2 F is Subset of REAL by VALUED_0:def 3;

end;

registration

let D be non empty set ;
let F be Function of REAL,D;
let F1 be real-valued FinSequence;
cluster F1 * F -> FinSequence-like ;
coherence
F * F1 is FinSequence-like

proof end;

end;

registration

let r be real number ;
cluster <*r*> -> real-valued ;
coherence
<*r*> is real-valued

proof end;

end;

registration

let r1, r2 be real number ;
cluster <*r1,r2*> -> real-valued ;
coherence
<*r1,r2*> is real-valued

proof end;

end;

registration

let r1, r2, r3 be real number ;
cluster <*r1,r2,r3*> -> real-valued ;
coherence
<*r1,r2,r3*> is real-valued

proof end;

end;

registration

let r1, r2, r3, r4 be real number ;
cluster <*r1,r2,r3,r4*> -> real-valued ;
coherence
<*r1,r2,r3,r4*> is real-valued

proof end;

end;

registration

let j be Nat;
let r be real number ;
cluster j |-> r -> real-valued ;
coherence
j |-> r is real-valued ;

end;

registration

let f, g be real-valued FinSequence;
cluster f ^ g -> real-valued ;
coherence
f ^ g is real-valued

proof end;

end;

theorem :: RVSUM_1:1

canceled;

theorem :: RVSUM_1:2

canceled;

theorem :: RVSUM_1:3

0 is_a_unity_wrt addreal by BINOP_2:2, SETWISEO:22;

definition

redefine func diffreal equals :: RVSUM_1:def 1
addreal * ((id REAL),compreal);
compatibility
for b₁ being Element of bool [:[:REAL,REAL:],REAL:] holds
( b₁ = diffreal iff b₁ = addreal * ((id REAL),compreal) )

proof end;

correctness
;

end;

:: deftheorem defines diffreal RVSUM_1:def 1 :
diffreal = addreal * ((id REAL),compreal);

definition

func sqrreal -> UnOp of REAL means :Def2: :: RVSUM_1:def 2
for r being real number holds it . r = r ^2 ;
existence
ex b₁ being UnOp of REAL st
for r being real number holds b₁ . r = r ^2

proof end;

uniqueness
for b₁, b₂ being UnOp of REAL st ( for r being real number holds b₁ . r = r ^2 ) & ( for r being real number holds b₂ . r = r ^2 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines sqrreal RVSUM_1:def 2 :
for b₁ being UnOp of REAL holds
( b₁ = sqrreal iff for r being real number holds b₁ . r = r ^2 );

theorem :: RVSUM_1:4

canceled;

theorem :: RVSUM_1:5

canceled;

theorem :: RVSUM_1:6

canceled;

theorem :: RVSUM_1:7

canceled;

theorem :: RVSUM_1:8

canceled;

theorem :: RVSUM_1:9

canceled;

theorem :: RVSUM_1:10

canceled;

theorem :: RVSUM_1:11

canceled;

theorem :: RVSUM_1:12

canceled;

theorem :: RVSUM_1:13

1 is_a_unity_wrt multreal by BINOP_2:7, SETWISEO:22;

theorem :: RVSUM_1:14

canceled;

theorem :: RVSUM_1:15

canceled;

theorem Th16: :: RVSUM_1:16

multreal is_distributive_wrt addreal

proof end;

theorem :: RVSUM_1:17

sqrreal is_distributive_wrt multreal

proof end;

definition

let x be real number ;
func x multreal -> UnOp of REAL equals :: RVSUM_1:def 3
multreal [;] (x,(id REAL));
coherence
multreal [;] (x,(id REAL)) is UnOp of REAL

proof end;

end;

:: deftheorem defines multreal RVSUM_1:def 3 :
for x being real number holds x multreal = multreal [;] (x,(id REAL));

Lm3: for r, r1 being real number holds (multreal [;] (r,(id REAL))) . r1 = r * r1

proof end;

theorem :: RVSUM_1:18

canceled;

theorem :: RVSUM_1:19

for r, r1 being real number holds (r multreal) . r1 = r * r1 by Lm3;

theorem :: RVSUM_1:20

for r being real number holds r multreal is_distributive_wrt addreal

proof end;

theorem Th21: :: RVSUM_1:21

compreal is_an_inverseOp_wrt addreal

proof end;

theorem Th22: :: RVSUM_1:22

addreal is having_an_inverseOp by Th21, FINSEQOP:def 2;

theorem Th23: :: RVSUM_1:23

the_inverseOp_wrt addreal = compreal by Th21, Th22, FINSEQOP:def 3;

theorem :: RVSUM_1:24

compreal is_distributive_wrt addreal by Th22, Th23, FINSEQOP:67;

Lm4: for F being real-valued FinSequence holds F is FinSequence of REAL

proof end;

definition

let F1, F2 be real-valued FinSequence;
:: original: +
redefine func F1 + F2 -> FinSequence of REAL equals :: RVSUM_1:def 4
addreal .: (F1,F2);
coherence
F1 + F2 is FinSequence of REAL by Lm4;
compatibility
for b₁ being FinSequence of REAL holds
( b₁ = F1 + F2 iff b₁ = addreal .: (F1,F2) )

proof end;

commutativity
for b₁ being FinSequence of REAL
for F1, F2 being real-valued FinSequence st b₁ = addreal .: (F1,F2) holds
b₁ = addreal .: (F2,F1)

proof end;

end;

:: deftheorem defines + RVSUM_1:def 4 :
for F1, F2 being real-valued FinSequence holds F1 + F2 = addreal .: (F1,F2);

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on REAL;
:: original: +
redefine func R1 + R2 -> Element of i -tuples_on REAL;
coherence
R1 + R2 is Element of i -tuples_on REAL by FINSEQ_2:140;

end;

theorem :: RVSUM_1:25

canceled;

theorem :: RVSUM_1:26

canceled;

theorem :: RVSUM_1:27

for s being set
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 + R2) . s = (R1 . s) + (R2 . s)

proof end;

theorem :: RVSUM_1:28

for F being real-valued FinSequence holds (<*> REAL) + F = <*> REAL

proof end;

theorem :: RVSUM_1:29

for r1, r2 being real number holds <*r1*> + <*r2*> = <*(r1 + r2)*>

proof end;

theorem :: RVSUM_1:30

for i being Nat
for r1, r2 being real number holds (i |-> r1) + (i |-> r2) = i |-> (r1 + r2)

proof end;

theorem :: RVSUM_1:31

canceled;

theorem :: RVSUM_1:32

for F1, F2, F3 being real-valued FinSequence holds F1 + (F2 + F3) = (F1 + F2) + F3 by RFUNCT_1:19;

theorem :: RVSUM_1:33

for i being Nat
for R being Element of i -tuples_on REAL holds R + (i |-> 0) = R by BINOP_2:2, FINSEQOP:57;

theorem :: RVSUM_1:34

canceled;

theorem :: RVSUM_1:35

for s being set
for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8;

definition

let F be real-valued FinSequence;
:: original: -
redefine func - F -> FinSequence of REAL equals :: RVSUM_1:def 5
compreal * F;
coherence
- F is FinSequence of REAL by Lm4;
compatibility
for b₁ being FinSequence of REAL holds
( b₁ = - F iff b₁ = compreal * F )

proof end;

end;

:: deftheorem defines - RVSUM_1:def 5 :
for F being real-valued FinSequence holds - F = compreal * F;

definition

let i be Nat;
let R be Element of i -tuples_on REAL;
:: original: -
redefine func - R -> Element of i -tuples_on REAL;
coherence
- R is Element of i -tuples_on REAL by FINSEQ_2:133;

end;

theorem :: RVSUM_1:36

for s being set
for F being real-valued FinSequence holds (- F) . s = - (F . s) by VALUED_1:8;

theorem :: RVSUM_1:37

- (<*> REAL) = <*> REAL ;

theorem :: RVSUM_1:38

for r being real number holds - <*r*> = <*(- r)*>

proof end;

theorem Th39: :: RVSUM_1:39

for i being Nat
for r being real number holds - (i |-> r) = i |-> (- r)

proof end;

theorem :: RVSUM_1:40

for i being Nat
for R being Element of i -tuples_on REAL holds R + (- R) = i |-> 0 by Th22, Th23, BINOP_2:2, FINSEQOP:77;

theorem :: RVSUM_1:41

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st R1 + R2 = i |-> 0 holds
R1 = - R2 by Th22, Th23, BINOP_2:2, FINSEQOP:78;

theorem :: RVSUM_1:42

canceled;

theorem :: RVSUM_1:43

for R1, R2 being complex-valued Function st - R1 = - R2 holds
R1 = R2

proof end;

theorem :: RVSUM_1:44

for i being Nat
for R1, R, R2 being Element of i -tuples_on REAL st R1 + R = R2 + R holds
R1 = R2

proof end;

theorem Th45: :: RVSUM_1:45

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

proof end;

definition

let F1, F2 be real-valued FinSequence;
:: original: -
redefine func F1 - F2 -> FinSequence of REAL equals :: RVSUM_1:def 6
diffreal .: (F1,F2);
coherence
F1 - F2 is FinSequence of REAL by Lm4;
compatibility
for b₁ being FinSequence of REAL holds
( b₁ = F1 - F2 iff b₁ = diffreal .: (F1,F2) )

proof end;

end;

:: deftheorem defines - RVSUM_1:def 6 :
for F1, F2 being real-valued FinSequence holds F1 - F2 = diffreal .: (F1,F2);

definition

let i be Nat;
let R1, R2 be Element of i -tuples_on REAL;
:: original: -
redefine func R1 - R2 -> Element of i -tuples_on REAL;
coherence
R1 - R2 is Element of i -tuples_on REAL by FINSEQ_2:140;

end;

theorem :: RVSUM_1:46

canceled;

theorem :: RVSUM_1:47

canceled;

theorem :: RVSUM_1:48

for s being set
for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (R1 - R2) . s = (R1 . s) - (R2 . s)

proof end;

theorem :: RVSUM_1:49

for F being real-valued FinSequence holds
( (<*> REAL) - F = <*> REAL & F - (<*> REAL) = <*> REAL )

proof end;

theorem :: RVSUM_1:50

for r1, r2 being real number holds <*r1*> - <*r2*> = <*(r1 - r2)*>

proof end;

theorem :: RVSUM_1:51

for i being Nat
for r1, r2 being real number holds (i |-> r1) - (i |-> r2) = i |-> (r1 - r2)

proof end;

theorem :: RVSUM_1:52

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

theorem :: RVSUM_1:53

for i being Nat
for R being Element of i -tuples_on REAL holds R - (i |-> 0) = R

proof end;

theorem :: RVSUM_1:54

for i being Nat
for R being Element of i -tuples_on REAL holds (i |-> 0) - R = - R by BINOP_2:2, FINSEQOP:57;

theorem :: RVSUM_1:55

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

theorem :: RVSUM_1:56

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

proof end;

theorem :: RVSUM_1:57

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

proof end;

theorem :: RVSUM_1:58

for i being Nat
for R being Element of i -tuples_on REAL holds R - R = i |-> 0 by Th22, Th23, BINOP_2:2, FINSEQOP:77;

theorem :: RVSUM_1:59

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st R1 - R2 = i |-> 0 holds
R1 = R2

proof end;

theorem :: RVSUM_1:60

for F1, F2, F3 being real-valued FinSequence holds (F1 - F2) - F3 = F1 - (F2 + F3) by RFUNCT_1:32;

theorem :: RVSUM_1:61

for F1, F2, F3 being real-valued FinSequence holds F1 + (F2 - F3) = (F1 + F2) - F3 by RFUNCT_1:35;

theorem :: RVSUM_1:62

for F1, F2, F3 being real-valued FinSequence holds F1 - (F2 - F3) = (F1 - F2) + F3 by RFUNCT_1:34;

theorem :: RVSUM_1:63

for i being Nat
for R1, R being Element of i -tuples_on REAL holds R1 = (R1 + R) - R

proof end;

theorem :: RVSUM_1:64

for i being Nat
for R1, R being Element of i -tuples_on REAL holds R1 = (R1 - R) + R

proof end;

notation

let F be real-valued FinSequence;
let r be real number ;
synonym r * F for r (#) F;

end;

theorem :: RVSUM_1:65

canceled;

theorem :: RVSUM_1:66

for s being set
for r being real number
for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;

definition

let F be real-valued FinSequence;
let r be real number ;
:: original: *
redefine func r * F -> FinSequence of REAL equals :: RVSUM_1:def 7
(r multreal) * F;
coherence
r * F is FinSequence of REAL by Lm4;
compatibility
for b₁ being FinSequence of REAL holds
( b₁ = r * F iff b₁ = (r multreal) * F )

proof end;

end;

:: deftheorem defines * RVSUM_1:def 7 :
for F being real-valued FinSequence
for r being real number holds r * F = (r multreal) * F;

definition

let i be Nat;
let R be Element of i -tuples_on REAL;
let r be real number ;
:: original: *
redefine func r * R -> Element of i -tuples_on REAL;
coherence
r * R is Element of i -tuples_on REAL by FINSEQ_2:133;

end;

theorem :: RVSUM_1:67

for s being set
for r being real number
for F being real-valued FinSequence holds (r * F) . s = r * (F . s) by VALUED_1:6;

theorem :: RVSUM_1:68

for r being real number holds r * (<*> REAL) = <*> REAL ;

theorem :: RVSUM_1:69

for r, r1 being real number holds r * <*r1*> = <*(r * r1)*>

proof end;

theorem Th70: :: RVSUM_1:70

for i being Nat
for r1, r2 being real number holds r1 * (i |-> r2) = i |-> (r1 * r2)

proof end;

theorem :: RVSUM_1:71

for r1, r2 being real number
for F being real-valued FinSequence holds (r1 * r2) * F = r1 * (r2 * F) by RFUNCT_1:29;

theorem :: RVSUM_1:72

for r1, r2 being real number
for F being real-valued FinSequence holds (r1 + r2) * F = (r1 * F) + (r2 * F)

proof end;

theorem :: RVSUM_1:73

for r being real number
for F1, F2 being real-valued FinSequence holds r * (F1 + F2) = (r * F1) + (r * F2) by RFUNCT_1:28;

theorem :: RVSUM_1:74

for F being real-valued FinSequence holds 1 * F = F by RFUNCT_1:33;

theorem :: RVSUM_1:75

for i being Nat
for R being Element of i -tuples_on REAL holds 0 * R = i |-> 0

proof end;

theorem :: RVSUM_1:76

for F being real-valued FinSequence holds (- 1) * F = - F ;

notation

let F be real-valued FinSequence;
synonym sqr F for F ^2 ;

end;

definition

let F be real-valued FinSequence;
:: original: sqr
redefine func sqr F -> FinSequence of REAL equals :: RVSUM_1:def 8
sqrreal * F;
compatibility
for b₁ being FinSequence of REAL holds
( b₁ = sqr F iff b₁ = sqrreal * F )

proof end;

coherence
sqr F is FinSequence of REAL by Lm4;

end;

:: deftheorem defines sqr RVSUM_1:def 8 :
for F being real-valued FinSequence holds sqr F = sqrreal * F;

definition

let i be Nat;
let R be Element of i -tuples_on REAL;
:: original: sqr
redefine func sqr R -> Element of i -tuples_on REAL;
coherence
sqr R is Element of i -tuples_on REAL by FINSEQ_2:133;

end;

theorem :: RVSUM_1:77

canceled;

theorem :: RVSUM_1:78

canceled;

theorem :: RVSUM_1:79

canceled;

theorem :: RVSUM_1:80

canceled;

theorem :: RVSUM_1:81

for r being real number holds sqr <*r*> = <*(r ^2)*>

proof end;

theorem :: RVSUM_1:82

for i being Nat
for r being real number holds sqr (i |-> r) = i |-> (r ^2)

proof end;

theorem Th83: :: RVSUM_1:83

for F being real-valued FinSequence holds sqr (- F) = sqr F

proof end;

theorem Th84: :: RVSUM_1:84

for r being real number
for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F)

proof end;

notation

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

end;

definition

let F1, F2 be real-valued FinSequence;
:: original: mlt
redefine func mlt (F1,F2) -> FinSequence of REAL equals :: RVSUM_1:def 9
multreal .: (F1,F2);
coherence
mlt (F1,F2) is FinSequence of REAL by Lm4;
compatibility
for b₁ being FinSequence of REAL holds
( b₁ = mlt (F1,F2) iff b₁ = multreal .: (F1,F2) )

proof end;

commutativity
for b₁ being FinSequence of REAL
for F1, F2 being real-valued FinSequence st b₁ = multreal .: (F1,F2) holds
b₁ = multreal .: (F2,F1)

proof end;

end;

:: deftheorem defines mlt RVSUM_1:def 9 :
for F1, F2 being real-valued FinSequence holds mlt (F1,F2) = multreal .: (F1,F2);

theorem :: RVSUM_1:85

canceled;

theorem :: RVSUM_1:86

for s being set
for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;

definition

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

end;

theorem :: RVSUM_1:87

for s being set
for F1, F2 being real-valued FinSequence holds (mlt (F1,F2)) . s = (F1 . s) * (F2 . s) by VALUED_1:5;

theorem :: RVSUM_1:88

for F being real-valued FinSequence holds mlt ((<*> REAL),F) = <*> REAL

proof end;

theorem :: RVSUM_1:89

for r1, r2 being real number holds mlt (<*r1*>,<*r2*>) = <*(r1 * r2)*>

proof end;

theorem :: RVSUM_1:90

canceled;

theorem :: RVSUM_1:91

canceled;

theorem Th92: :: RVSUM_1:92

for i being Nat
for r being real number
for R being Element of i -tuples_on REAL holds mlt ((i |-> r),R) = r * R

proof end;

theorem :: RVSUM_1:93

for i being Nat
for r1, r2 being real number holds mlt ((i |-> r1),(i |-> r2)) = i |-> (r1 * r2)

proof end;

theorem :: RVSUM_1:94

for r being real number
for F1, F2 being real-valued FinSequence holds r * (mlt (F1,F2)) = mlt ((r * F1),F2) by RFUNCT_1:24;

theorem :: RVSUM_1:95

canceled;

theorem :: RVSUM_1:96

for i being Nat
for r being real number
for R being Element of i -tuples_on REAL holds r * R = mlt ((i |-> r),R) by Th92;

theorem :: RVSUM_1:97

for F being real-valued FinSequence holds sqr F = mlt (F,F) ;

theorem Th98: :: RVSUM_1:98

for F1, F2 being real-valued FinSequence holds sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)

proof end;

theorem Th99: :: RVSUM_1:99

for F1, F2 being real-valued FinSequence holds sqr (F1 - F2) = ((sqr F1) - (2 * (mlt (F1,F2)))) + (sqr F2)

proof end;

theorem :: RVSUM_1:100

for F1, F2 being real-valued FinSequence holds sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2))

proof end;

notation

let F be Relation;
synonym complex-yielding F for complex-valued ;

end;

registration

cluster -> complex-valued FinSequence of COMPLEX ;
coherence
for b₁ being FinSequence of COMPLEX holds b₁ is complex-yielding ;
cluster Relation-like Function-like complex-valued real-valued V59() FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st
( b₁ is real-valued & b₁ is complex-yielding )

proof end;

end;

definition

let F be complex-valued FinSequence;
canceled;
func Sum F -> complex number means :Def11: :: RVSUM_1:def 11
ex f being FinSequence of COMPLEX st
( f = F & it = addcomplex $$ f );
existence
ex b₁ being complex number ex f being FinSequence of COMPLEX st
( f = F & b₁ = addcomplex $$ f )

proof end;

uniqueness
for b₁, b₂ being complex number st ex f being FinSequence of COMPLEX st
( f = F & b₁ = addcomplex $$ f ) & ex f being FinSequence of COMPLEX st
( f = F & b₂ = addcomplex $$ f ) holds
b₁ = b₂ ;

end;

:: deftheorem RVSUM_1:def 10 :
canceled;

:: deftheorem Def11 defines Sum RVSUM_1:def 11 :
for F being complex-valued FinSequence
for b₂ being complex number holds
( b₂ = Sum F iff ex f being FinSequence of COMPLEX st
( f = F & b₂ = addcomplex $$ f ) );

registration

let F be real-valued FinSequence;
cluster Sum F -> complex real ;
coherence
Sum F is real

proof end;

end;

theorem Th101: :: RVSUM_1:101

for F being FinSequence of REAL holds Sum F = addreal $$ F

proof end;

definition

let F be FinSequence of COMPLEX ;
:: original: Sum
redefine func Sum F -> Element of COMPLEX equals :: RVSUM_1:def 12
addcomplex $$ F;
coherence
Sum F is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = Sum F iff b₁ = addcomplex $$ F ) by Def11;

end;

:: deftheorem defines Sum RVSUM_1:def 12 :
for F being FinSequence of COMPLEX holds Sum F = addcomplex $$ F;

definition

let F be FinSequence of REAL ;
:: original: Sum
redefine func Sum F -> Element of REAL equals :: RVSUM_1:def 13
addreal $$ F;
coherence
Sum F is Element of REAL by XREAL_0:def 1;
compatibility
for b₁ being Element of REAL holds
( b₁ = Sum F iff b₁ = addreal $$ F ) by Th101;

end;

:: deftheorem defines Sum RVSUM_1:def 13 :
for F being FinSequence of REAL holds Sum F = addreal $$ F;

theorem Th102: :: RVSUM_1:102

Sum (<*> REAL) = 0 by BINOP_2:2, FINSOP_1:11;

theorem :: RVSUM_1:103

for r being real number holds Sum <*r*> = r

proof end;

theorem Th104: :: RVSUM_1:104

for r being real number
for F being real-valued FinSequence holds Sum (F ^ <*r*>) = (Sum F) + r

proof end;

theorem Th105: :: RVSUM_1:105

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

proof end;

theorem :: RVSUM_1:106

for r being real number
for F being real-valued FinSequence holds Sum (<*r*> ^ F) = r + (Sum F)

proof end;

theorem Th107: :: RVSUM_1:107

for r1, r2 being real number holds Sum <*r1,r2*> = r1 + r2

proof end;

theorem Th108: :: RVSUM_1:108

for r1, r2, r3 being real number holds Sum <*r1,r2,r3*> = (r1 + r2) + r3

proof end;

theorem :: RVSUM_1:109

for R being Element of 0 -tuples_on REAL holds Sum R = 0 by Th102;

theorem Th110: :: RVSUM_1:110

for i being Nat
for r being real number holds Sum (i |-> r) = i * r

proof end;

theorem Th111: :: RVSUM_1:111

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

proof end;

theorem Th112: :: RVSUM_1:112

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) holds
Sum R1 <= Sum R2

proof end;

theorem Th113: :: RVSUM_1:113

for i being Nat
for R1, R2 being Element of i -tuples_on REAL st ( for j being Nat st j in Seg i holds
R1 . j <= R2 . j ) & ex j being Nat st
( j in Seg i & R1 . j < R2 . j ) holds
Sum R1 < Sum R2

proof end;

theorem Th114: :: RVSUM_1:114

for F being real-valued FinSequence st ( for i being Nat st i in dom F holds
0 <= F . i ) holds
0 <= Sum F

proof end;

theorem Th115: :: RVSUM_1:115

for F being real-valued FinSequence st ( for i being Nat st i in dom F holds
0 <= F . i ) & ex i being Nat st
( i in dom F & 0 < F . i ) holds
0 < Sum F

proof end;

theorem Th116: :: RVSUM_1:116

for F being real-valued FinSequence holds 0 <= Sum (sqr F)

proof end;

theorem Th117: :: RVSUM_1:117

for r being real number
for F being real-valued FinSequence holds Sum (r * F) = r * (Sum F)

proof end;

theorem Th118: :: RVSUM_1:118

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

proof end;

theorem Th119: :: RVSUM_1:119

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 + R2) = (Sum R1) + (Sum R2)

proof end;

theorem Th120: :: RVSUM_1:120

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Sum (R1 - R2) = (Sum R1) - (Sum R2)

proof end;

theorem :: RVSUM_1:121

for i being Nat
for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds
R = i |-> 0

proof end;

theorem :: RVSUM_1:122

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds (Sum (mlt (R1,R2))) ^2 <= (Sum (sqr R1)) * (Sum (sqr R2))

proof end;

definition

let F be complex-valued FinSequence;
func Product F -> complex number means :Def14: :: RVSUM_1:def 14
ex f being FinSequence of COMPLEX st
( f = F & it = multcomplex $$ f );
existence
ex b₁ being complex number ex f being FinSequence of COMPLEX st
( f = F & b₁ = multcomplex $$ f )

proof end;

uniqueness
for b₁, b₂ being complex number st ex f being FinSequence of COMPLEX st
( f = F & b₁ = multcomplex $$ f ) & ex f being FinSequence of COMPLEX st
( f = F & b₂ = multcomplex $$ f ) holds
b₁ = b₂ ;

end;

:: deftheorem Def14 defines Product RVSUM_1:def 14 :
for F being complex-valued FinSequence
for b₂ being complex number holds
( b₂ = Product F iff ex f being FinSequence of COMPLEX st
( f = F & b₂ = multcomplex $$ f ) );

registration

let F be real-valued FinSequence;
cluster Product F -> complex real ;
coherence
Product F is real

proof end;

end;

theorem Th123: :: RVSUM_1:123

for F being FinSequence of REAL holds Product F = multreal $$ F

proof end;

definition

let F be FinSequence of COMPLEX ;
:: original: Product
redefine func Product F -> Element of COMPLEX equals :: RVSUM_1:def 15
multcomplex $$ F;
coherence
Product F is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = Product F iff b₁ = multcomplex $$ F ) by Def14;

end;

:: deftheorem defines Product RVSUM_1:def 15 :
for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F;

definition

let F be FinSequence of REAL ;
:: original: Product
redefine func Product F -> Element of REAL equals :: RVSUM_1:def 16
multreal $$ F;
coherence
Product F is Element of REAL by XREAL_0:def 1;
compatibility
for b₁ being Element of REAL holds
( b₁ = Product F iff b₁ = multreal $$ F ) by Th123;

end;

:: deftheorem defines Product RVSUM_1:def 16 :
for F being FinSequence of REAL holds Product F = multreal $$ F;

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

proof end;

theorem Th124: :: RVSUM_1:124

Product (<*> REAL) = 1 by Lm5;

registration

let r be complex number ;
cluster <*r*> -> complex-valued ;
coherence
<*r*> is complex-yielding

proof end;

end;

registration

let r1, r2 be complex number ;
cluster <*r1,r2*> -> complex-valued ;
coherence
<*r1,r2*> is complex-yielding

proof end;

end;

registration

let r1, r2, r3 be complex number ;
cluster <*r1,r2,r3*> -> complex-valued ;
coherence
<*r1,r2,r3*> is complex-yielding

proof end;

end;

theorem Th125: :: RVSUM_1:125

for r being complex number holds Product <*r*> = r

proof end;

registration

let f, g be complex-valued FinSequence;
cluster f ^ g -> complex-valued ;
coherence
f ^ g is complex-yielding

proof end;

end;

theorem Th126: :: RVSUM_1:126

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

proof end;

theorem Th127: :: RVSUM_1:127

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

proof end;

theorem :: RVSUM_1:128

for r being real number
for F being real-valued FinSequence holds Product (<*r*> ^ F) = r * (Product F)

proof end;

theorem Th129: :: RVSUM_1:129

for r1, r2 being complex number holds Product <*r1,r2*> = r1 * r2

proof end;

theorem :: RVSUM_1:130

for r1, r2, r3 being complex number holds Product <*r1,r2,r3*> = (r1 * r2) * r3

proof end;

theorem :: RVSUM_1:131

for R being Element of 0 -tuples_on REAL holds Product R = 1 by Lm5;

theorem :: RVSUM_1:132

for i being Nat holds Product (i |-> 1) = 1

proof end;

Lm6: for p being complex-valued FinSequence st len p <> 0 holds
ex q being complex-valued FinSequence ex d being complex number st p = q ^ <*d*>

proof end;

theorem :: RVSUM_1:133

for F being complex-valued FinSequence holds
( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )

proof end;

theorem :: RVSUM_1:134

for i, j being Nat
for r being real number holds Product ((i + j) |-> r) = (Product (i |-> r)) * (Product (j |-> r))

proof end;

theorem :: RVSUM_1:135

for i, j being Nat
for r being real number holds Product ((i * j) |-> r) = Product (j |-> (Product (i |-> r)))

proof end;

theorem :: RVSUM_1:136

for i being Nat
for r1, r2 being real number holds Product (i |-> (r1 * r2)) = (Product (i |-> r1)) * (Product (i |-> r2))

proof end;

theorem Th137: :: RVSUM_1:137

for i being Nat
for R1, R2 being Element of i -tuples_on REAL holds Product (mlt (R1,R2)) = (Product R1) * (Product R2)

proof end;

theorem :: RVSUM_1:138

for i being Nat
for r being real number
for R being Element of i -tuples_on REAL holds Product (r * R) = (Product (i |-> r)) * (Product R)

proof end;

theorem :: RVSUM_1:139

for i being Nat
for R being Element of i -tuples_on REAL holds Product (sqr R) = (Product R) ^2 by Th137;

begin

theorem :: RVSUM_1:140

for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F ;

theorem :: RVSUM_1:141

for i, j being Nat
for z being Element of COMPLEX holds Product ((i + j) |-> z) = (Product (i |-> z)) * (Product (j |-> z))

proof end;

theorem :: RVSUM_1:142

for i, j being Nat
for z being Element of COMPLEX holds Product ((i * j) |-> z) = Product (j |-> (Product (i |-> z))) by SETWOP_2:38;

theorem :: RVSUM_1:143

for i being Nat
for z1, z2 being Element of COMPLEX holds Product (i |-> (z1 * z2)) = (Product (i |-> z1)) * (Product (i |-> z2))

proof end;

begin

theorem Th5: :: RVSUM_1:144

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

proof end;

theorem Th6: :: RVSUM_1:145

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

proof end;

theorem Th7: :: RVSUM_1:146

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

proof end;

theorem Th8: :: RVSUM_1:147

for a being real number
for x being real-valued FinSequence holds len (a * x) = len x

proof end;

theorem Th9: :: RVSUM_1:148

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

proof end;

begin

definition

let x1, x2 be real-valued FinSequence;
func |(x1,x2)| -> real number equals :: RVSUM_1:def 17
Sum (mlt (x1,x2));
correctness
coherence
Sum (mlt (x1,x2)) is real number ;
;
commutativity
for b₁ being real number
for x1, x2 being real-valued FinSequence st b₁ = Sum (mlt (x1,x2)) holds
b₁ = Sum (mlt (x2,x1)) ;

end;

:: deftheorem defines |( RVSUM_1:def 17 :
for x1, x2 being real-valued FinSequence holds |(x1,x2)| = Sum (mlt (x1,x2));

definition

let x1, x2 be real-valued FinSequence;
:: original: |(
redefine func |(x1,x2)| -> Element of REAL ;
correctness
coherence
|(x1,x2)| is Element of REAL ;
;
commutativity
for x1, x2 being real-valued FinSequence holds |(x1,x2)| = |(x2,x1)| ;

end;

theorem Th11: :: RVSUM_1:149

for x being real-valued FinSequence holds |(x,x)| >= 0

proof end;

theorem Th19: :: RVSUM_1:150

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

proof end;

theorem Th20: :: RVSUM_1:151

for x, y being real-valued FinSequence
for a being real number st len x = len y holds
|((a * x),y)| = a * |(x,y)|

proof end;

theorem Th22: :: RVSUM_1:152

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

proof end;

theorem :: RVSUM_1:153

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

proof end;

theorem Th25: :: RVSUM_1:154

for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds
|((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|

proof end;

theorem :: RVSUM_1:155

for x, y being real number
for x1, x2, x3 being real-valued FinSequence st len x1 = len x2 & len x2 = len x3 holds
|(((x * x1) + (y * x2)),x3)| = (x * |(x1,x3)|) + (y * |(x2,x3)|)

proof end;

theorem Th29: :: RVSUM_1:156

for x1, x2, y1, y2 being real-valued FinSequence st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|

proof end;

theorem Th30: :: RVSUM_1:157

for x1, x2, y1, y2 being real-valued FinSequence st len x1 = len x2 & len x2 = len y1 & len y1 = len y2 holds
|((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|

proof end;

theorem :: RVSUM_1:158

for x, y being real-valued FinSequence st len x = len y holds
|((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|

proof end;

theorem :: RVSUM_1:159

for x, y being real-valued FinSequence st len x = len y holds
|((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|

proof end;

theorem Th40: :: RVSUM_1:160

for n being Nat
for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|

proof end;

theorem Th41: :: RVSUM_1:161

for n being Nat
for p1, p2 being Element of n -tuples_on REAL
for x being real number holds |((x * p1),p2)| = x * |(p1,p2)|

proof end;

theorem Th43: :: RVSUM_1:162

for n being Nat
for p1, p2 being Element of n -tuples_on REAL holds |((- p1),p2)| = - |(p1,p2)|

proof end;

theorem :: RVSUM_1:163

for n being Nat
for p1, p2 being Element of n -tuples_on REAL holds |((- p1),(- p2))| = |(p1,p2)|

proof end;

theorem Th46: :: RVSUM_1:164

for n being Nat
for p1, p2, p3 being Element of n -tuples_on REAL holds |((p1 - p2),p3)| = |(p1,p3)| - |(p2,p3)|

proof end;

theorem :: RVSUM_1:165

for n being Nat
for x, y being real number
for p1, p2, p3 being Element of n -tuples_on REAL holds |(((x * p1) + (y * p2)),p3)| = (x * |(p1,p3)|) + (y * |(p2,p3)|)

proof end;

theorem Th50: :: RVSUM_1:166

for n being Nat
for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 + p2),(q1 + q2))| = ((|(p1,q1)| + |(p1,q2)|) + |(p2,q1)|) + |(p2,q2)|

proof end;

theorem Th51: :: RVSUM_1:167

for n being Nat
for p1, p2, q1, q2 being Element of n -tuples_on REAL holds |((p1 - p2),(q1 - q2))| = ((|(p1,q1)| - |(p1,q2)|) - |(p2,q1)|) + |(p2,q2)|

proof end;

theorem :: RVSUM_1:168

for n being Nat
for p, q being Element of n -tuples_on REAL holds |((p + q),(p + q))| = (|(p,p)| + (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem Th53: :: RVSUM_1:169

for n being Nat
for p, q being Element of n -tuples_on REAL holds |((p - q),(p - q))| = (|(p,p)| - (2 * |(p,q)|)) + |(q,q)|

proof end;

theorem :: RVSUM_1:170

for n being Nat
for p, q being Element of n -tuples_on REAL holds |(p,q)| <= |(p,p)| + |(q,q)|

proof end;

definition

let p, q be real-valued FinSequence;
pred p,q are_orthogonal means :Def3: :: RVSUM_1:def 18
|(p,q)| = 0 ;
symmetry
for p, q being real-valued FinSequence st |(p,q)| = 0 holds
|(q,p)| = 0 ;

end;

:: deftheorem Def3 defines are_orthogonal RVSUM_1:def 18 :
for p, q being real-valued FinSequence holds
( p,q are_orthogonal iff |(p,q)| = 0 );

theorem :: RVSUM_1:171

for n being Nat
for a being real number
for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal

proof end;

theorem :: RVSUM_1:172

for r1, r2, r3, r4 being real number holds Sum <*r1,r2,r3,r4*> = ((r1 + r2) + r3) + r4

proof end;