Summation of i from 1 to n of Summation of j from 1 to i/Proof 1

Theorem

$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i a_{i j} = \sum_{j \mathop = 1}^n \sum_{i \mathop = j}^n a_{i j}$

$\ds \sum_{i \mathop = 1}^n \sum_{j \mathop = 1}^i$

can be expressed as:

$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}$

where:

$\map R i$ is the propositional function $1 \le i \le n$

$\map S {i, j}$ is the propositional function $1 \le j \le i$

We wish to find a propositional function $\map {S'} j$ which is to be:

there exists an $i$ such that both $1 \le i \le n$ and $1 \le j \le i$

This is satisfied by the propositional function:

$\map {S'} j := 1 \le j \le n$

Next we wish to find a propositional function $\map {R'} {i, j}$ which is to be:

both $1 \le i \le n$ and $1 \le j \le i$

This is satisfied by the propositional function:

$\map {R'} {i, j} := j \le i \le n$

$\blacksquare$