The abstract of the Mizar article:

The Sum and Product of Finite Sequences of Real Numbers

by

Czeslaw Bylinski

Received May 11, 1990

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
   0 is_a_unity_wrt addreal;

theorem :: RVSUM_1:4
   the_unity_wrt addreal = 0;

theorem :: RVSUM_1:5
   addreal has_a_unity;

theorem :: RVSUM_1:6
   addreal is commutative;

theorem :: RVSUM_1:7
   addreal is associative;

definition
 func diffreal -> BinOp of REAL equals
:: RVSUM_1:def 1
  addreal*(id REAL,compreal);
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
   multreal is_distributive_wrt addreal;

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
   r multreal is_distributive_wrt addreal;

theorem :: RVSUM_1:21
   compreal is_an_inverseOp_wrt addreal;

theorem :: RVSUM_1:22
   addreal has_an_inverseOp;

theorem :: RVSUM_1:23
   the_inverseOp_wrt addreal = compreal;

theorem :: RVSUM_1:24
     compreal is_distributive_wrt addreal;

:: Some Functors on the i-tuples on Real


definition let F1,F2;
  func F1 + F2 -> FinSequence of REAL equals
:: RVSUM_1:def 4
 addreal.:(F1,F2);
 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
 addreal $$ F;
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;