Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### The Sum and Product of Finite Sequences of Real Numbers

by
Czeslaw Bylinski

MML identifier: RVSUM_1
[ Mizar article, MML identifier index ]

```environ

vocabulary FINSEQ_1, FINSEQ_2, ARYTM_1, FUNCT_1, RELAT_1, BINOP_1, VECTSP_1,
SETWISEO, SQUARE_1, ARYTM, FUNCOP_1, FINSEQOP, RLVECT_1, RVSUM_1, CARD_3,
BOOLE;
notation TARSKI, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1,
NAT_1, SQUARE_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1,
VECTSP_1, SETWISEO, FINSEQ_1, FINSEQ_2, FINSEQ_4, SEQ_1, FINSEQOP,
SETWOP_2;
constructors REAL_1, NAT_1, SQUARE_1, BINOP_1, VECTSP_1, SETWISEO, FINSEQOP,
FINSOP_1, FINSEQ_4, SEQ_2, MEMBERED, PARTFUN1, XBOOLE_0;
clusters RELSET_1, FINSEQ_2, NAT_1, MEMBERED, ZFMISC_1, FUNCT_1, PARTFUN1,
FUNCT_2, XBOOLE_0, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve i,j,k for Nat;
reserve x,x1,x2,x3,r,r1,r2,r3 for Element of REAL;
reserve F,F',F1,F2 for FinSequence of REAL;
reserve R,R1,R2,R3 for Element of i-tuples_on REAL;

:: Auxiliary theorems

canceled 2;

theorem :: RVSUM_1:3

theorem :: RVSUM_1:4

theorem :: RVSUM_1:5

theorem :: RVSUM_1:6

theorem :: RVSUM_1:7

definition
func diffreal -> BinOp of REAL equals
:: RVSUM_1:def 1
end;

canceled;

theorem :: RVSUM_1:9
diffreal.(r1,r2) = r1 - r2;

definition
func sqrreal -> UnOp of REAL means
:: RVSUM_1:def 2
for r holds it.r = r^2;
end;

canceled;

theorem :: RVSUM_1:11
multreal is commutative;

theorem :: RVSUM_1:12
multreal is associative;

theorem :: RVSUM_1:13
1 is_a_unity_wrt multreal;

theorem :: RVSUM_1:14
the_unity_wrt multreal = 1;

theorem :: RVSUM_1:15
multreal has_a_unity;

theorem :: RVSUM_1:16

theorem :: RVSUM_1:17
sqrreal is_distributive_wrt multreal;

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

canceled;

theorem :: RVSUM_1:19
(r multreal).x = r*x;

theorem :: RVSUM_1:20

theorem :: RVSUM_1:21

theorem :: RVSUM_1:22

theorem :: RVSUM_1:23

theorem :: RVSUM_1:24

:: Some Functors on the i-tuples on Real

definition let F1,F2;
func F1 + F2 -> FinSequence of REAL equals
:: RVSUM_1:def 4
commutativity;
end;

canceled;

theorem :: RVSUM_1:26
i in dom (F1+F2) implies (F1+F2).i = F1.i + F2.i;

definition let i,R1,R2;
redefine func R1 + R2 -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:27
(R1+R2).j = R1.j + R2.j;

theorem :: RVSUM_1:28
<*>REAL + F = <*>REAL;

theorem :: RVSUM_1:29
<*r1*> + <*r2*> = <*r1+r2*>;

theorem :: RVSUM_1:30
(i|->r1) + (i|->r2) = i|->(r1+r2);

canceled;

theorem :: RVSUM_1:32
R1 + (R2 + R3) = R1 + R2 + R3;

theorem :: RVSUM_1:33
R + (i|->(0 qua Real)) = R;

definition let F;
func -F -> FinSequence of REAL equals
:: RVSUM_1:def 5
compreal*F;
involutiveness;
end;

theorem :: RVSUM_1:34
dom F = dom -F;

theorem :: RVSUM_1:35
(-F).i = -F.i;

definition let i,R;
redefine func -R -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:36
r = R.j implies (-R).j = -r;

theorem :: RVSUM_1:37
-(<*>REAL) = <*>REAL;

theorem :: RVSUM_1:38
-<*r*> = <*-r*>;

theorem :: RVSUM_1:39
-(i|->r) = i|->-r;

theorem :: RVSUM_1:40
R + -R = (i|->0);

theorem :: RVSUM_1:41
R1 + R2 = (i|->0) implies R1 = -R2;

canceled;

theorem :: RVSUM_1:43
-R1 = -R2 implies R1 = R2;

theorem :: RVSUM_1:44
R1 + R = R2 + R implies R1 = R2;

theorem :: RVSUM_1:45
-(R1 + R2) = -R1 + -R2;

definition let F1,F2;
func F1 - F2 -> FinSequence of REAL equals
:: RVSUM_1:def 6
diffreal.:(F1,F2);
end;

canceled;

theorem :: RVSUM_1:47
i in dom (F1-F2) implies (F1-F2).i = F1.i - F2.i;

definition let i,R1,R2;
redefine func R1 - R2 -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:48
(R1-R2).j = R1.j - R2.j;

theorem :: RVSUM_1:49
<*>REAL - F = <*>REAL & F - <*>REAL = <*>REAL;

theorem :: RVSUM_1:50
<*r1*> - <*r2*> = <*r1-r2*>;

theorem :: RVSUM_1:51
(i|->r1) - (i|->r2) = i|->(r1-r2);

theorem :: RVSUM_1:52
R1 - R2 = R1 + - R2;

theorem :: RVSUM_1:53
R - (i|->(0 qua Real)) = R;

theorem :: RVSUM_1:54
(i|->(0 qua Real)) - R = -R;

theorem :: RVSUM_1:55
R1 - -R2 = R1 + R2;

theorem :: RVSUM_1:56
-(R1 - R2) = R2 - R1;

theorem :: RVSUM_1:57
-(R1 - R2) = -R1 + R2;

theorem :: RVSUM_1:58
R - R = (i|->0);

theorem :: RVSUM_1:59
R1 - R2 = (i|->0) implies R1 = R2;

theorem :: RVSUM_1:60
R1 - R2 - R3 = R1 - (R2 + R3);

theorem :: RVSUM_1:61
R1 + (R2 - R3) = R1 + R2 - R3;

theorem :: RVSUM_1:62
R1 - (R2 - R3) = R1 - R2 + R3;

theorem :: RVSUM_1:63
R1 = R1 + R - R;

theorem :: RVSUM_1:64
R1 = R1 - R + R;

definition let r be real number; let F;
func r*F -> FinSequence of REAL equals
:: RVSUM_1:def 7
(r multreal)*F;
end;

theorem :: RVSUM_1:65
dom(r*F) = dom F;

theorem :: RVSUM_1:66
(r*F).i = r*(F.i);

definition let i; let r be real number; let R;
redefine func r*R -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:67
(r*R).j = r*(R.j);

theorem :: RVSUM_1:68
r*(<*>REAL) = <*>REAL;

theorem :: RVSUM_1:69
r*<*r1*> = <*r*r1*>;

theorem :: RVSUM_1:70
r1*(i|->r2) = i|->(r1*r2);

theorem :: RVSUM_1:71
(r1*r2)*R = r1*(r2*R);

theorem :: RVSUM_1:72
(r1 + r2)*R = r1*R + r2*R;

theorem :: RVSUM_1:73
r*(R1+R2) = r*R1 + r*R2;

theorem :: RVSUM_1:74
1*R = R;

theorem :: RVSUM_1:75
0*R = (i|->0);

theorem :: RVSUM_1:76
(-1)*R = -R;

definition let F;
func sqr F -> FinSequence of REAL equals
:: RVSUM_1:def 8
sqrreal*F;
end;

theorem :: RVSUM_1:77
dom(sqr F) = dom F;

theorem :: RVSUM_1:78
(sqr F).i = (F.i)^2;

definition let i,R;
redefine func sqr R -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:79
(sqr R).j = (R.j)^2;

theorem :: RVSUM_1:80
sqr (<*>REAL) = <*>REAL;

theorem :: RVSUM_1:81
sqr <*r*> = <*r^2*>;

theorem :: RVSUM_1:82
sqr(i |-> r) = i |-> r^2;

theorem :: RVSUM_1:83
sqr -R = sqr R;

theorem :: RVSUM_1:84
sqr (r*R) = r^2* sqr R;

definition let F1,F2;
func mlt(F1,F2) -> FinSequence of REAL equals
:: RVSUM_1:def 9
multreal.:(F1,F2);
commutativity;
end;

canceled;

theorem :: RVSUM_1:86
i in dom mlt(F1,F2) implies mlt(F1,F2).i = F1.i * F2.i;

definition let i,R1,R2;
redefine func mlt(R1,R2) -> Element of i-tuples_on REAL;
end;

theorem :: RVSUM_1:87
mlt(R1,R2).j = R1.j * R2.j;

theorem :: RVSUM_1:88
mlt(<*>REAL,F) = <*>REAL;

theorem :: RVSUM_1:89
mlt(<*r1*>,<*r2*>) = <*r1*r2*>;

canceled;

theorem :: RVSUM_1:91
mlt(R1,mlt(R2,R3)) = mlt(mlt(R1,R2),R3);

theorem :: RVSUM_1:92
mlt(i|->r,R) = r*R;

theorem :: RVSUM_1:93
mlt(i|->r1,i|->r2) = i|->(r1*r2);

theorem :: RVSUM_1:94
r*mlt(R1,R2) = mlt(r*R1,R2);

canceled;

theorem :: RVSUM_1:96
r*R = mlt(i|->r,R);

theorem :: RVSUM_1:97
sqr(R) = mlt(R,R);

theorem :: RVSUM_1:98
sqr(R1 + R2) = sqr R1 + 2*mlt(R1,R2) + sqr R2;

theorem :: RVSUM_1:99
sqr(R1 - R2) = sqr R1 - 2*mlt(R1,R2) + sqr R2;

theorem :: RVSUM_1:100
sqr mlt(R1,R2) = mlt(sqr R1,sqr R2);

:: Finite sum of Finite Sequence of Real Numbers

definition let F be FinSequence of REAL;
func Sum(F) -> Real equals
:: RVSUM_1:def 10
end;

canceled;

theorem :: RVSUM_1:102
Sum(<*> REAL) = 0;

theorem :: RVSUM_1:103
Sum <*r*> = r;

theorem :: RVSUM_1:104
Sum(F^<*r*>) = Sum F + r;

theorem :: RVSUM_1:105
Sum(F1^F2) = Sum F1 + Sum F2;

theorem :: RVSUM_1:106
Sum(<*r*>^F) = r + Sum F;

theorem :: RVSUM_1:107
Sum<*r1,r2*> = r1 + r2;

theorem :: RVSUM_1:108
Sum<*r1,r2,r3*> = r1 + r2 + r3;

theorem :: RVSUM_1:109
for R being Element of 0-tuples_on REAL holds Sum R = 0;

theorem :: RVSUM_1:110
Sum(i |-> r) = i*r;

theorem :: RVSUM_1:111
Sum(i |-> (0 qua Real)) = 0;

theorem :: RVSUM_1:112
(for j st j in Seg i holds R1.j <= R2.j) implies Sum R1 <= Sum R2;

theorem :: RVSUM_1:113
(for j st j in Seg i holds R1.j <= R2.j) &
(ex j st j in Seg i & R1.j < R2.j)
implies Sum R1 < Sum R2;

theorem :: RVSUM_1:114
(for i st i in dom F holds 0 <= F.i) implies 0 <= Sum F;

theorem :: RVSUM_1:115
(for i st i in dom F holds 0 <= F.i) &
(ex i st i in dom F & 0 < F.i)
implies 0 < Sum F;

theorem :: RVSUM_1:116
0 <= Sum sqr F;

theorem :: RVSUM_1:117
Sum(r*F) = r*(Sum F);

theorem :: RVSUM_1:118
Sum -F = -(Sum F);

theorem :: RVSUM_1:119
Sum(R1 + R2) = Sum R1 + Sum R2;

theorem :: RVSUM_1:120
Sum(R1 - R2) = Sum R1 - Sum R2;

theorem :: RVSUM_1:121
Sum sqr R = 0 implies R = i |-> 0;

theorem :: RVSUM_1:122
(Sum mlt(R1,R2))^2 <= (Sum sqr R1)*(Sum sqr R2);

:: The Product of Finite Sequences of Real Numbers

definition let F be FinSequence of REAL;
func Product (F) -> Real equals
:: RVSUM_1:def 11
multreal \$\$ F;
end;

canceled;

theorem :: RVSUM_1:124
Product (<*> REAL) = 1;

theorem :: RVSUM_1:125
Product <*r*> = r;

theorem :: RVSUM_1:126
Product (F^<*r*>) = Product F * r;

theorem :: RVSUM_1:127
Product (F1^F2) = Product F1 * Product F2;

theorem :: RVSUM_1:128
Product (<*r*>^F) = r * Product F;

theorem :: RVSUM_1:129
Product <*r1,r2*> = r1 * r2;

theorem :: RVSUM_1:130
Product <*r1,r2,r3*> = r1 * r2 * r3;

theorem :: RVSUM_1:131
for R being Element of 0-tuples_on REAL holds Product R = 1;

theorem :: RVSUM_1:132
Product (i|->(1 qua Real)) = 1;

theorem :: RVSUM_1:133
(ex k st k in dom F & F.k = 0) iff Product F = 0;

theorem :: RVSUM_1:134
Product ((i+j)|->r) = (Product (i|->r))*(Product (j|->r));

theorem :: RVSUM_1:135
Product ((i*j)|->r) = Product (j|->(Product (i|->r)));

theorem :: RVSUM_1:136
Product (i|->(r1*r2)) = (Product (i|->r1))*(Product (i|->r2));

theorem :: RVSUM_1:137
Product mlt(R1,R2) = Product R1 * Product R2;

theorem :: RVSUM_1:138
Product (r*R) = Product (i|->r) * Product R;

theorem :: RVSUM_1:139
Product sqr R = (Product R)^2;
```