avewright/proofwiki-math huggingface dataset:
Theorem: Numbers whose Fourth Root equals Number of Divisors

There are $4$ positive integers whose $4$th root equals the number of its divisors:
{{begin-eqn}}
{{eqn | l = 1
      | r = 1^4
      | c = 
}}
{{eqn | l = 625
      | r = 5^4
      | c = 
}}
{{eqn | l = 6561
      | r = 9^4
      | c = 
}}
{{eqn | l = 4 \, 100 \, 625
      | r = 45^4
      | c = 
}}
{{end-eqn}}
{{OEIS|A143026}}

Proof:
{{begin-eqn}}
{{eqn | l = \map {\sigma_0} 1
      | r = 1
      | c = {{DCFLink|1}}
}}
{{eqn | l = \map {\sigma_0} {625}
      | r = 5
      | c = {{DCFLink|625}}
}}
{{eqn | l = \map {\sigma_0} {6561}
      | r = 9
      | c = {{DCFLink|6561}}
}}
{{eqn | l = \map {\sigma_0} {4 \, 100 \, 625}
      | r = 45
      | c = {{DCFLink|4,100,625|4 \, 100 \, 625}}
}}
{{end-eqn}}
Suppose $N = \map {\sigma_0} {N^4}$.
By Divisor Count Function is Odd Iff Argument is Square, $N$ must be odd.
The case $N = 1$ is trivial.
Suppose $N$ is a prime power.
Write $N = p^n$.
By Divisor Count Function of Power of Prime:
:$N = \map {\sigma_0} {p^{4 n} } = 4 n + 1$
By Bernoulli's Inequality:
:$N = p^n \ge 1 + n \paren {p - 1}$
This gives us the inequality:
:$4 n + 1 \ge 1 + n \paren {p - 1}$
which can be simplified to:
:$4 \ge p - 1$
The only odd primes satisfying the inequality are $3$ and $5$.
We have:
:$\map {\sigma_0} {3^4} = 5 > 3^1$
:$\map {\sigma_0} {3^8} = 9 = 3^2$
:$\map {\sigma_0} {3^{4 n} } = 4 n + 1 < 3^n$ for $n > 2$
:$\map {\sigma_0} {5^4} = 5 = 5^1$
:$\map {\sigma_0} {5^{4 n} } = 4 n + 1 < 5^n$ for $n > 1$
:$\map {\sigma_0} {p^{4 n} } = 4 n + 1 < p^n$ for any $p > 5$
Hence $625$ and $6561$ are the only prime powers satisfying the property.
Note that Divisor Count Function is Multiplicative.
To form an integer $N$ with our property, we must choose and multiply prime powers from the list above.
The product $625 \times 6561 = 4 \, 100 \, 625$ gives equality.
If we chose any $\tuple {p, n}$ with $\map {\sigma_0} {p^{4 n} } < p^n$, we must choose $3^4$ in order for equality to possibly hold.
Then $\map {\sigma_0} {3^4} = 5 \divides N$, so a tuple $\tuple {5, n}$ must be chosen.
If $\tuple {5, 1}$ was chosen, $5^2 \nmid N$.
But $\map {\sigma_0} {3^4 \times 5^4} = 25 \divides N$, which is a contradiction.
Suppose $\tuple {5, n}$ with $n \ge 2$ was chosen.
Then $\map {\sigma_0} {3^4 \times 5^{4 n} } = 20 n + 1 < 3 \times 5^n$, a contradiction.
Thus we have exhausted all cases.
{{qed}}
Theorem: Weak Existence of Matrix Logarithm

Let $T$ be a square matrix of order $n$.
Let $\norm {T - I} < 1$ in the norm on bounded linear operators, where $I$ the identity matrix.
Then there is a square matrix $S$ such that:
:$e^S = T$
where $e^S$ is the matrix exponential.

Proof:
Define:
:$\ds S = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n \paren {T - I}^n$
$S$ converges since $\norm {T - I} < 1$.
We have that $\ds \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n \norm {T - I}^n$ is the Newton-Mercator Series.
This converges since $\norm {T - I} < 1$.
Hence the series for $S$ converges absolutely, and so $S$ is well defined.
Using the series definition for the matrix exponential: 
{{begin-eqn}} 
{{eqn | l = e^S
      | r = I + S + \frac 1 {2!} S^2 + \frac 1 {3!} S^3 + \cdots
}}
{{eqn | r = I + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n \paren {T - I}^n + \frac 1 {2!} \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n \paren {T - I}^n}^2 + \frac 1 {3!} \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n \paren {T - I}^n}^3 + \cdots
}}
{{eqn | ll= \leadsto
      | l = e^S
      | r = I + \paren {T - I} + c_2 \paren {T - I}^2 + c_3 \paren {T - I}^3 + \cdots
      | c = grouping terms by powers of $T - I$
}}
{{eqn | r = T + c_2 \paren {T - I}^2 + c_3 \paren {T - I}^3 + \cdots
}}
{{end-eqn}}
If $c_i = 0$ for $i \ge 2$, then $e^S = T$, and the result is shown.
The Newton-Mercator Series is a Taylor expansion for $\map \ln {1 + x}$.
When combined with the Power Series Expansion for Exponential Function, it gives: 
{{begin-eqn}}
{{eqn | l = e^{\map \ln {1 + x} }
      | r = 1 + \map \ln {1 + x} + \frac 1 {2!} \paren {\map \ln {1 + x} }^2 + \frac 1 {3!} \paren {\map \ln {1 + x} }^3 + \cdots
}}
{{eqn | r = 1 + \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n x^n + \frac 1 {2!} \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n x^n}^2 + \frac 1 {3!} \paren {\sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} } n x^n}^3 + \cdots
}}
{{eqn | r = 1 + x + c_2 x^2 + c_3 x^3 + \cdots
      | c = grouping terms by powers of $x$
}}
{{end-eqn}}
But $e^{\map \ln {1 + x} } = 1 + x$.
Thus:
:$1 + x = 1 + x + c_2 x^2 + c_3 x^3 + \cdots \implies c_i = 0$
for $i \ge 2$.
{{explain|Why does this prove the theorem?}}
{{qed}}
Theorem: Norm on Vector Space is Continuous Function

Let $V$ be a vector space with norm $\norm {\, \cdot \,}$.
The function $\norm {\, \cdot \,}: V \to \R$ is continuous.

Proof:
Let $x_n \to x$ in $V$.
Then we have:
:$\norm {x_n - x} \to 0$
By the Reverse Triangle Inequality:
:$\size {\norm {x_n} - \norm x} \le \norm {x_n - x}$
Hence:
:$\size {\norm {x_n} - \norm x} \to 0$
Thus:
:$\norm {x_n} \to \norm x$
Hence the result from the definition of a continuous real function.
{{qed}}
Category:Norm Theory
bnmisbj2hihk2myoxcz9e4lzdiezf6r
Theorem: Smallest 5 Consecutive Primes in Arithmetic Sequence

The smallest $5$ consecutive primes in arithmetic sequence are:
:$9 \, 843 \, 019 + 30 n$
for $n = 0, 1, 2, 3, 4$.
Note that while there are many longer arithmetic sequences of far smaller primes, those primes are not consecutive.

Proof:
{{begin-eqn}}
{{eqn | l = 9 \, 843 \, 019 + 0 \times 30
      | r = 9 \, 843 \, 019
      | c = which is the $654 \, 926$th prime
}}
{{eqn | l = 9 \, 843 \, 019 + 1 \times 30
      | r = 9 \, 843 \, 049
      | c = which is the $654 \, 927$th prime
}}
{{eqn | l = 9 \, 843 \, 019 + 2 \times 30
      | r = 9 \, 843 \, 079
      | c = which is the $654 \, 928$th prime
}}
{{eqn | l = 9 \, 843 \, 019 + 3 \times 30
      | r = 9 \, 843 \, 109
      | c = which is the $654 \, 929$th prime
}}
{{eqn | l = 9 \, 843 \, 019 + 4 \times 30
      | r = 9 \, 843 \, 139
      | c = which is the $654 \, 930$th prime
}}
{{end-eqn}}
But note that $9 \, 843 \, 019 + 5 \times 30 = 9 \, 843 \, 169 = 7^2 \times 200 \, 881$ and so is not prime.
Inspection of tables of primes (or a computer search) will reveal that this is the smallest such sequence.
{{qed}}
Theorem: Number of Ways to Tile Standard Chessboard with Dominoes

The number of ways to tile a standard ($8 \times 8$) chessboard with dominoes is $12 \, 988 \, 816$.

Proof:
Follows directly from Kasteleyn's Formula for $m = n = 8$:
:$\ds \prod_{j \mathop = 1}^{\ceiling {\frac 8 2} } \prod_{k \mathop = 1}^{\ceiling {\frac 8 2} } \paren {4 \cos^2 \frac {\pi j} {8 + 1} + 4 \cos^2 \frac {\pi k} {8 + 1} } = 12 \, 988 \, 816$
{{qed}}
{{explain|The above really needs to be evaluated step by step, preferably using {{TL|eqn}} template}}
Theorem: Smallest Triplet of Primitive Pythagorean Triangles with Same Area

The smallest set of $3$ primitive Pythagorean triangles which all have the same area are:
:the $4485-5852-7373$ triangle
:the $3059-8580-9109$ triangle
:the $1380-19 \, 019-19 \, 069$ triangle.
That area is $13 \, 123 \, 110$.

Proof:
We have that:
:the $4485-5852-7373$ triangle $T_1$ is Pythagorean
:the $3059-8580-9109$ triangle $T_2$ is Pythagorean
:the $1380-19 \, 019-19 \, 069$ triangle $T_3$ is Pythagorean.
Then from Area of Triangle, their areas $A_1$, $A_2$ and $A_3$ respectively are given by:
{{begin-eqn}}
{{eqn | l = A_1
      | r = \dfrac {4485 \times 5852} 2
      | c = 
}}
{{eqn | r = \dfrac {\paren {3 \times 5 \times 13 \times 23} \times \paren {2^2 \times 7 \times 11 \times 19} } 2
      | c = 
}}
{{eqn | r = 2 \times 3 \times 5 \times 7 \times 11 \times 13 \times 19 \times 23
      | c = 
}}
{{eqn | r = 13 \, 123 \, 110
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = A_2
      | r = \dfrac {3059 \times 8580} 2
      | c = 
}}
{{eqn | r = \dfrac {\paren {7 \times 19 \times 23} \times \paren {2^2 \times 3 \times 5 \times 11 \times 13} } 2
      | c = 
}}
{{eqn | r = 2 \times 3 \times 5 \times 7 \times 11 \times 13 \times 19 \times 23
      | c = 
}}
{{eqn | r = 13 \, 123 \, 110
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = A_3
      | r = \dfrac {1380 \times 19 \, 019} 2
      | c = 
}}
{{eqn | r = \dfrac {\paren {2^2 \times 3 \times 5 \times 23} \times \paren {7 \times 11 \times 13 \times 19} } 2
      | c = 
}}
{{eqn | r = 2 \times 3 \times 5 \times 7 \times 11 \times 13 \times 19 \times 23
      | c = 
}}
{{eqn | r = 13 \, 123 \, 110
      | c = 
}}
{{end-eqn}}
{{ProofWanted|It remains to be shown that this is the smallest such triple.}}
Theorem: Squares whose Digits form Consecutive Integers

The sequence of integers whose squares have a decimal representation consisting of the concatenation of $2$ consecutive integers, either increasing or decreasing begins:
:$91, 428, 573, 727, 846, 7810, 9079, 9901, 36 \, 365, 63 \, 636, 326 \, 734, 673 \, 267, 733 \, 674, \ldots$
This sequence can be divided into two subsequences: 
Those where the consecutive integers are increasing:
:$428, 573, 727, 846, 7810, 36 \, 365, 63 \, 636, 326 \, 734, 673 \, 267, \ldots$
{{OEIS|A030467}}
Those where the consecutive integers are decreasing:
:$91, 9079, 9901, 733 \, 674, 999 \, 001, 88 \, 225 \, 295, \ldots$
{{OEIS|A054216}}

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 91^2
      | r = 8281
      | c = 
}}
{{eqn | l = 428^2
      | r = 183 \, 184
      | c = 
}}
{{eqn | l = 573^2
      | r = 328 \, 329
      | c = 
}}
{{eqn | l = 727^2
      | r = 528 \, 529
      | c = 
}}
{{eqn | l = 846^2
      | r = 715 \, 716
      | c = 
}}
{{eqn | l = 7810^2
      | r = 6099 \, 6100
      | c = 
}}
{{eqn | l = 9079^2
      | r = 82 \, 428 \, 241
      | c = 
}}
{{eqn | l = 9901^2
      | r = 98 \, 029 \, 801
      | c = 
}}
{{eqn | l = 36 \, 365^2
      | r = 13224 \, 13225
      | c = 
}}
{{eqn | l = 63 \, 636^2
      | r = 40495 \, 40496
      | c = 
}}
{{eqn | l = 326 \, 734^2
      | r = 106755 \, 106756
      | c = 
}}
{{end-eqn}}
They can be determined by inspection.
{{qed}}
Theorem: Squares whose Digits form Consecutive Decreasing Integers

The sequence of integers whose squares have a decimal representation consisting of the concatenation of $2$ consecutive decreasing integers begins:
:$91, 9079, 9901, 733 \, 674, 999 \, 001, 88 \, 225 \, 295, 99 \, 990 \, 001, \ldots$
{{OEIS|A030467}}

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 91^2
      | r = 8281
      | c = 
}}
{{eqn | l = 9079^2
      | r = 82 \, 428 \, 241
      | c = 
}}
{{eqn | l = 9901^2
      | r = 98 \, 029 \, 801
      | c = 
}}
{{eqn | l = 733 \, 674^2
      | r = 538 \, 277 \, 538 \, 276
      | c = 
}}
{{eqn | l = 999 \, 001^2
      | r = 998 \, 002 \, 998 \, 001
      | c = 
}}
{{end-eqn}}
They can be determined by inspection.
{{qed}}
Theorem: Numbers n whose Euler Phi value Divides n + 1

The following integers $n$ satisfy the equation:
:$\exists k \in \Z: k \, \map \phi n = n + 1$
where $\phi$ denotes the Euler $\phi$ function:
:$83 \, 623 \, 935, 83 \, 623 \, 935 \times 83 \, 623 \, 937$

Proof:
From {{EulerPhiLink|83,623,935|83 \, 623 \, 935}}:
:$\map \phi {83 \, 623 \, 935} = 41 \, 811 \, 968$
and then:
{{begin-eqn}}
{{eqn | l = 2 \times 41 \, 811 \, 968
      | r = 83 \, 623 \, 936
      | c = 
}}
{{eqn | r = 1 + 83 \, 623 \, 935
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Then we have that $83 \, 623 \, 937$ is the $868 \, 421$st prime number.
From Euler Phi Function of Prime:
:$\map \phi {83 \, 623 \, 937} = 83 \, 623 \, 936$
{{begin-eqn}}
{{eqn | l = \map \phi {83 \, 623 \, 935 \times 83 \, 623 \, 937}
      | r = \map \phi {83 \, 623 \, 935} \times \map \phi {83 \, 623 \, 937}
      | c = Euler Phi Function is Multiplicative
}}
{{eqn | r = 41 \, 811 \, 968 \times 83 \, 623 \, 936
      | c = from above
}}
{{end-eqn}}
Then we have that:
{{begin-eqn}}
{{eqn | l = 83 \, 623 \, 935 \times 83 \, 623 \, 937
      | r = \paren {83 \, 623 \, 936 - 1} \times \paren {83 \, 623 \, 936 + 1}
      | c = 
}}
{{eqn | r = 83 \, 623 \, 936^2 - 1^2
      | c = Difference of Two Squares
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = 2 \times \map \phi {83 \, 623 \, 935 \times 83 \, 623 \, 937}
      | r = 2 \times 41 \, 811 \, 968 \times 83 \, 623 \, 936
      | c = 
}}
{{eqn | r = 83 \, 623 \, 936^2
      | c = 
}}
{{eqn | r = 83 \, 623 \, 935 \times 83 \, 623 \, 937 + 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Polynomial is Linear Combination of Monomials

Let $R$ be a commutative ring with unity.
Let $R \sqbrk X$ be a polynomial ring over $R$ in the variable $X$.
Let $P \in R \sqbrk X$.
Then $P$ is a linear combination of the monomials of $R \sqbrk X$, with coefficients in $R$.
{{explain|this needs to be made more precise}}

Proof:
Let $S \subset R \sqbrk X$ be the subset of all elements that are linear combinations of monomials.
Let $\iota: S \to R \sqbrk X$ denote the inclusion mapping.
Suppose for the moment that $S$ is a commutative ring with unity.
Then by Universal Property of Polynomial Ring, there exists a ring homomorphism $g: R \sqbrk X \to S$ with $\map g X = X$.
By Inclusion Mapping on Subring is Homomorphism, $\iota: S \to R \sqbrk X$ is a ring homomorphism.
By Composition of Ring Homomorphisms is Ring Homomorphism, $\iota \circ g: R \sqbrk X \to R \sqbrk X$ is a ring homomorphism.
By construction, $\map {\paren {\iota \circ g} } X = X$.
By Universal Property of Polynomial Ring, there exists a unique ring homomorphism $h : R \sqbrk X \to R \sqbrk X$ with $\map h X = X$.
We have that $\iota \circ g$ is such a ring homomorphism.
By Identity Mapping is Ring Automorphism, the identity mapping $I$ on $R \sqbrk X$ is one too.
By uniqueness, $\iota \circ g = I$.
By Identity Mapping is Surjection and Surjection if Composite is Surjection, $\iota$ is a surjection.
By Inclusion Mapping is Surjection iff Identity, $S = R \sqbrk X$.
It remains to show that $S$ is a commutative ring with unity.
{{finish}}
Theorem: Sum over Disjoint Union of Finite Sets

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S$ and $T$ be finite disjoint sets.
Let $S \cup T$ be their union.
Let $f: S \cup T \to \mathbb A$ be a mapping.
Then we have the equality of summations over finite sets:
:$\ds \sum_{u \mathop \in S \mathop \cup T} \map f u = \sum_{s \mathop \in S} \map f s + \sum_{t \mathop \in T} \map f t$

Proof:
Note that by Union of Finite Sets is Finite, the union $S \cup T$ is finite.
Let $m$ be the cardinality of $S$ and $n$ be the cardinality of $T$.
Let $\N_{< m}$ denote an initial segment of the natural numbers.
Let $\sigma: \N_{<m} \to S$ and $\tau: \N_{<n} \to T$ be bijections.
Let $\alpha: \N_{< n} \to \closedint m {m + n - 1}$ be the mapping defined as:
:$\map \alpha k = k + m$
By Translation of Integer Interval is Bijection, $\alpha$ is a bijection.
By Composite of Bijections is Bijection and Disjoint Union of Bijections is Bijection, the union:
:$\sigma \cup \paren {\tau \circ \alpha} : \N_{<m} \cup \closedint m {m + n - 1} \to S \cup T$ is a bijection.
By Union of Integer Intervals, $\N_{<m} \cup \closedint m {m + n - 1} = \N_{< m + n}$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{u \mathop \in S \mathop \cup T} \map f u
      | r = \sum_{i \mathop = 0}^{m + n - 1} \map {f \circ \paren {\sigma \cup \paren {\tau \circ \alpha} } } i
      | c = {{Defof|Summation}}
}}
{{eqn | r = \sum_{i \mathop = 0}^{m - 1} \map {f \circ \paren {\sigma \cup \paren {\tau \circ \alpha} } } i + \sum_{i \mathop = m}^{m + n - 1} \map {f \circ \paren {\sigma \cup \paren {\tau \circ \alpha} } } i
      | c = Indexed Summation over Adjacent Intervals
}}
{{eqn | r = \sum_{i \mathop = 0}^{m - 1} \map {\paren {f \circ \sigma} } i + \sum_{i \mathop = m}^{m + n - 1} \map {\paren {g \circ \tau \circ \alpha} } i
      | c = Restriction of Union of Mappings to Component of Domain
}}
{{eqn | r = \sum_{i \mathop = 0}^{m - 1} \map {\paren {f \circ \sigma} } i + \sum_{i \mathop = 0}^{n - 1} \map {\paren {g \circ \tau} } i
      | c = Definition of $\alpha$, Indexed Summation over Translated Interval
}}
{{eqn | r = \sum_{s \mathop \in S} \map f s + \sum_{t \mathop \in T} \map g t
      | c = {{Defof|Summation}}
}}
{{end-eqn}}
{{qed}}
Theorem: Finite Summation does not Change under Permutation

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S$ be a finite set.
Let $f: S \to \mathbb A$ be a mapping.
Let $\sigma: S \to S$ be a permutation.
Then we have the equality of summations over finite sets:
:$\ds \sum_{s \mathop \in S} \map f s = \sum_{s \mathop \in S} \map f {\map \sigma s}$

Proof:
This is a special case of Change of Variables in Summation over Finite Set.
{{qed}}
Category:Summations
glofy0i42m26o45ix2z326ih5804vid
Theorem: Summation over Finite Set is Well-Defined

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S$ be a finite set.
Let $f: S \to \mathbb A$ be a mapping.
Let $n$ be the cardinality of $S$.
let $\N_{<n}$ be an initial segment of the natural numbers.
Let $g, h: \N_{<n} \to S$ be bijections.
Then we have an equality of indexed summations of the compositions $f \circ g$ and $f \circ h$:
:$\ds \sum_{i \mathop = 0}^{n - 1} \map f {\map g i} = \sum_{i \mathop = 0}^{n - 1} \map f {\map h i}$
That is, the definition of summation over a finite set does not depend on the choice of the bijection $g: S \to \N_{< n}$.

Proof:
By Inverse of Bijection is Bijection, $h^{-1} : \N_{<n} \to S$ is a bijection.
By Composite of Bijections is Bijection, the composition $h^{-1}\circ g$ is a permutation of $\N_{<n}$.
By Indexed Summation does not Change under Permutation, we have an equality of indexed summations:
:$\ds \sum_{i \mathop = 0}^{n - 1} \map {\paren {f \circ h} } i = \sum_{i \mathop = 0}^{n - 1} \map {\paren {f \circ h} \circ \paren {h^{-1} \circ g} } i$
By Composition of Mappings is Associative and Composite of Bijection with Inverse is Identity Mapping, the {{RHS}} equals $\ds \sum_{i \mathop = 0}^{n - 1} \map f {\map g i}$.
{{qed}}
Theorem: Change of Variables in Summation over Finite Set

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $S$ and $T$ be finite sets.
Let $f: S \to \mathbb A$ be a mapping.
Let $g: T \to S$ be a bijection.
Then we have an equality of summations over finite sets:
:$\ds \sum_{s \mathop \in S} \map f s = \sum_{t \mathop \in T} \map f {\map g t}$

Proof:
Let $n$ be the cardinality of $S$ and $T$.
Let $\N_{<n}$ be an initial segment of the natural numbers.
Let $h : \N_{<n} \to T$ be a bijection.
By definition of summation:
:$\ds \sum_{t \mathop \in T} \map f {\map g t} = \sum_{i \mathop = 0}^{n - 1} \map f {\map g {\map h i} }$
By Composite of Bijections is Bijection, the composition $g \circ h : \N_{<n} \to S$ is a bijection.
By definition of summation:
:$\ds \sum_{s \mathop\in S} \map f s = \ds \sum_{i \mathop = 0}^{n - 1} \map f {\map g {\map h i} }$
{{qed}}
Theorem: Indexed Summation does not Change under Permutation

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a$ and $b$ be integers.
Let $\closedint a b$ be the integer interval between $a$ and $b$.
Let $f: \closedint a b \to \mathbb A$ be a mapping.
Let $\sigma: \closedint a b \to \closedint a b$ be a permutation.
Then we have an equality of indexed summations:
:$\ds \sum_{i \mathop = a}^b \map f i = \sum_{i \mathop = a}^b \map f {\map \sigma i}$

Proof:
Let $a > b$.
Then by definition of indexed summation, both sides are $0$.
Let $a \le b$.
Theorem: Indexed Summation over Translated Interval

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a$ and $b$ be integers.
Let $\closedint a b$ be the integer interval between $a$ and $b$.
Let $f: \closedint a b \to \mathbb A$ be a mapping.
Let $c\in\Z$ be an integer.
Then we have an equality of indexed summations:
:$\ds \sum_{i \mathop = a}^b f(i) = \sum_{i \mathop = a + c}^{b + c} \map f {i - c}$

Proof:
The proof goes by induction on $b$.
Theorem: Indexed Summation over Adjacent Intervals

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a, b, c$ be integers.
Let $\closedint a c$ denote the integer interval between $a$ and $c$.
Let $b \in \closedint {a - 1} c$.
Let $f : \closedint a c \to \mathbb A$ be a mapping.
Then we have an equality of indexed summations:
:$\ds \sum_{i \mathop = a}^c \map f i = \sum_{i \mathop = a}^b \map f i + \sum_{i \mathop = b + 1}^c \map f i$

Proof:
The proof goes by induction on $b$.
Theorem: Indexed Summation over Interval of Length Two

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a \in \Z$ be an integer.
Let $f: \set {a, a + 1} \to \mathbb A$ be a real-valued function.
Then the indexed summation:
:$\ds \sum_{i \mathop = a}^{a + 1} \map f i = \map f a + \map f {a + 1}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = a}^{a + 1} \map f i
      | r = \sum_{i \mathop = a}^a \map f i + \map f {a + 1}
      | c = {{Defof|Indexed Summation}}
}}
{{eqn | l = 
      | r = \map f a + \map f {a + 1}
      | c = Indexed Summation over Interval of Length One
}}
{{end-eqn}}
{{qed}}
Category:Summations
78xilf6b035pq7lcw7s29wx7invkrca
Theorem: Indexed Summation over Interval of Length One

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a \in \Z$ be an integer.
Let $f: \set a \to \mathbb A$ be a mapping on the singleton $\set a$.
Then the indexed summation:
:$\ds \sum_{i \mathop = a}^a \map f i = \map f a$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = a}^a \map f i
      | r = \sum_{i \mathop = a}^{a - 1} \map f i + \map f a
      | c = {{Defof|Indexed Summation}}
}}
{{eqn | l = 
      | r = 0 + \map f a
      | c = {{Defof|Indexed Summation}}, $a - 1 < a$
}}
{{eqn | l = 
      | r = \map f a
      | c = Identity Element of Addition on Numbers
}}
{{end-eqn}}
{{qed}}
Theorem: Change of Variables in Indexed Summation

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a, b, c, d$ be integers.
Let $\closedint a b$ denote the integer interval between $a$ and $b$.
Let $f: \closedint a b \to \mathbb A$ be a mapping.
Let $g: \closedint c d \to \closedint a b$ be a bijection.
Then we have an equality of indexed summations:
:$\ds \sum_{i \mathop = a}^b \map f i = \sum_{i \mathop = c}^d \map f {\map g i}$

Proof:
Because $g : \closedint c d \to \closedint a b$ is a bijection, these sets are equivalent.
By Cardinality of Integer Interval, $\closedint a b$ has cardinality $b - a + 1$.
Thus:
:$b - a + 1 = d - c + 1$
Thus
:$c - a = d - b$
By Indexed Summation over Translated Interval:
:$\ds \sum_{i \mathop = c}^d \map f {\map g i} = \sum_{i \mathop = a}^b \map f {\map g {i + c - a} }$
By Translation of Integer Interval is Bijection, the mapping $T : \closedint a b \to \closedint c d$ defined as:
:$\map T k = k + c - a$
is a bijection.
By Composite of Bijections is Bijection, $g \circ T$ is a permutation of $\closedint a b$.
We have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = c}^d \map f {\map g i}
      | r = \sum_{i \mathop = a}^b \map f {\map g {i + c - a} }
      | c = Indexed Summation over Translated Interval
}}
{{eqn | r = \sum_{i \mathop = a}^b \map f {\map g {\map T i} }
      | c = Definition of $T$
}}
{{eqn | r = \sum_{i \mathop = a}^b \map f i
      | c = Indexed Summation does not Change under Permutation
}}
{{end-eqn}}
{{qed}}
Theorem: Translation of Integer Interval is Bijection

Let $a, b, c \in \Z$ be integers.
Let $\closedint a b$ denote the integer interval between $a$ and $b$.
Then the mapping $T: \closedint a b \to \closedint {a + c} {b + c}$ defined as:
:$\map T k = k + c$
is a bijection.

Proof:
Note that if $k \in \closedint a b$, then indeed $k + c \in \closedint {a + c} {b + c}$.
Theorem: Indexed Summation without First Term

Let $\mathbb A$ be one of the standard number systems $\N, \Z, \Q, \R, \C$.
Let $a$ and $b$ be integers with $a \le b$.
Let $\closedint a b$ be the integer interval between $a$ and $b$.
Let $f: \closedint a b \to \mathbb A$ be a mapping.
Then we have an equality of indexed summations:
:$\ds \sum_{i \mathop = a}^b \map f i = \map f a + \sum_{i \mathop = a + 1}^b \map f {\map \sigma i}$
{{explain|What is $\sigma$?}}

Proof:
The proof goes by induction on $b$.