Go backward to 4.7.1 Minimum and MaximumGo up to 4.7 Arithmetic NotionsGo forward to 4.7.3 Binomials |

Frequently we want to construct the sum of a collection of values.

(The value of this term is 0, ifsum_{x, F}T).

( forallx: ~F)=> ( sum_{x, F}T) = 0;( forally:F[x<-y]=> ( sum_{x, F}T) =T[x<-y] + (sum_{x, F /\ x != y}T)).

Please note that the value of the term is only defined if there do not exist infinitely many

Usually `F` contains the condition `x` in **N**, which is
therefore not written explicitly. Also the variable `x` is usually not
written but has to be deduced from the context.

(sum_{1 <= i <= n}i^{2}) = (sum_{i, (i in N /\ 1 <= i /\ i <= n)}i^{2});

(sum_{1 <= i <= 5}i^{2}) = 1^{2}+2^{2}+3^{2}+4^{2}+5^{2};

(sum_{1 <= i <= 0}i^{5}) = 0;

(sum_{1 <= i <= 9}(x-i)^{2}) = (x-1)^{2}+ (sum_{2 <= i <= 9}(x-i)^{2})

(sum_{1 <= i <= n}x^{i}) = (sum_{1 <= i <= n /\ even(i)}x^{i}) + (sum_{1 <= i <= n /\ odd(i)}x^{i})

(In general, for any finite sequencesum_{0 <= i <= 5}a_{i}*10^{i}) = 709213.

(denotes the value of this sequence in the decimal number system. Likewise, for any finite sequencesum_{0 <= i < length(d)}d_{i}*10^{i})

(denotes the value of this sequence in the binary number system, e.g., the value of [0, 1, 1, 0, 1] issum_{0 <= i < length(b)}b_{i}*2^{i})

1*2^{4}+0*2^{3}+1*2^{2}+1*2^{1}+0*2^{0}=22.

The quantifier may also bind multiple variables.

(sum_{1 <= i <= 5, 1 <= j <= 3}i*j) = 1*1+1*2+1*3+ (sum_{2 <= i <= 5, 1 <= j <= 3}i*j)

(sum_{1 <= i <= 3, 1 <= j <= i}i*j) = 1*1 + 2*1 + 2*2 + 3*1 + 3*2 +3*3.

We have a number of important identities.

(sum_{i, F}T) * (sum_{j, G}U) = (sum_{i, F}(sum_{j, G}T*U)).

(sum_{i, F}(sum_{j, G}T)) = (sum_{j, G}(sum_{i, F}T)) = (sum_{i, j, F /\ G}T).

(Furthermore, if termsum_{i, F}T) + (sum_{i, H}T) = (sum_{i, F \/ H}T) + (sum_{i, F /\ H}T).

(sum_{i, F}C*T) =C*(sum_{i, F}T).

(sum_{i, F}C) =n*C(wherenis the number ofifor whichFholds).

(sum_{1 <= i <= n}x^{i}) * (sum_{1 <= j <= m}x^{j}) = (sum_{1 <= i <= n}(sum_{1 <= j <= m}x^{i+j})) = (sum_{1 <= i <= n /\ 1 <= j <= m}x^{i+j}).

(sum_{1 <= i <= n}(sum_{1 <= j <= m}i*x^{j})) = (sum_{1 <= i <= n}(i*(sum_{1 <= j <= m}x^{j}))).

Likewise we often wish to construct the product of a collection of values.

(The value of this term is 1, ifprod_{x, F}T).

( forallx: ~F)=> ( prod_{x, F}T) = 1;( forally:F[x<-y]=> ( prod_{x, F}T) =T[x<-y] + (prod_{x, F /\ x != y}T)).

The same remarks apply as for the definition of the sum quantifier.

(prod_{1 <= i <= 0}i^{5}) = 1;

(prod_{0 <= i <= 5}a_{i}) =a_{0}*a_{1}*a_{2}*a_{3}*a_{4}*a_{5}

(prod_{0 <= i <= 100}a_{i}) =a_{0}*a_{1}*a_{2}* (prod_{3 <= i <= 100}a_{i})

(prod_{0 <= i <= 100}a_{i}) = (prod_{0 <= i <= 50}a_{i}) * (prod_{51 <= i <= 100}a_{i})

(prod_{1 <= i <= 3, 1 <= j <= i}i+j) = (1+1)*(2+1)*(2+2)*(3+1)*(3+2)*(3+3).

We have the following identities.

(prod_{i, F}(prod_{j, G}T)) = (prod_{j, G}(prod_{i, F}T)) = (prod_{i, j, F /\ G}T).

(Furthermore, if termprod_{i, F}T) * (prod_{i, H}T) = (prod_{i, F \/ H}T) * (prod_{i, F /\ H}T).

(prod_{i, F}C*T) =C^{n}(prod_{i, F}T) (wherenis the number ofifor whichFholds).

(prod_{i, F}C) =C^{n}(wherenis the number ofifor whichFholds)

With the help of the product quantifier we can now formulate the uniqueness of
prime number composition stated in Section *Natural Numbers*.

A prime number factorization offorallninN_{>0}: (existsp: pf(n,p) /\ (forallq: pf(n,q) =>p=q)).

pf( n,p) : <=>p:N->N×N/\( foralliinN:p(i)_{0}is prime /\p(i)_{0}<p(i+1)_{0}) /\( existskinN:n= (prod_{0 <= i <= k}p(i)_{0}^{p(i)1}) /\foralli>k:p(i)_{1}= 0)

[<2, 2>, <3, 1>, <5, 2>, <7, 0>, <11, 0>, <13, 0>, ...].Likewise, 1 has the prime number factorization

[<2, 0>, <3, 0>, <5, 0>, <7, 0>, <11, 0>, <13, 0>, ...].

Author: Wolfgang Schreiner

Last Modification: October 4, 1999