avewright/proofwiki-math huggingface dataset:
Theorem: Number of Digits to Represent Integer in Given Number Base

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $b \in \Z$ be an integer such that $b > 1$.
Let $d$ denote the number of digits of $n$ when represented in base $b$.
Then:
:$d = \ceiling {\map {\log_b} {n + 1} }$
where $\ceiling {\, \cdot \,}$ denotes the ceiling function.

Proof:
Let $n$ have $d$ digits.
Then:
{{begin-eqn}}
{{eqn | l = b^{d - 1}
      | o = \le
      | m = n
      | mo= <
      | r = b^d
      | c = Basis Representation Theorem
}}
{{eqn | ll= \leadsto
      | l = b^{d - 1}
      | o = <
      | m = n + 1
      | mo= \le
      | r = b^d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = d - 1
      | o = <
      | m = \map {\log_b} {n + 1}
      | mo= \le
      | r = d
      | c = 
}}
{{eqn | ll= \leadsto
      | o = 
      | m = \ceiling {\map {\log_b} {n + 1} }
      | mo= =
      | r = d
      | c = Integer equals Ceiling iff Number between Integer and One Less
}}
{{end-eqn}}
{{qed}}
Category:Number Theory
7uk6ird8jwcsa8ian5bgrtxks94kyxo
Theorem: Number of Bits for Decimal Integer

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $n$ have $m$ digits when expressed in decimal notation.
Then $n$ may require as many as $\ceiling {\dfrac m {\log_{10} 2} }$ bits to represent it.

Proof:
Let $d$ be the number of bits that may be needed to represent $n$.
Let $n$ have $m$ digits.
Then:
:$n \le 10^m - 1$
and so:
{{begin-eqn}}
{{eqn | l = d
      | r = \ceiling {\map {\log_2} {\paren {10^m - 1} + 1} }
      | c = Number of Digits to Represent Integer in Given Number Base
}}
{{eqn | r = \ceiling {\map {\log_2} {10^m} }
      | c = 
}}
{{eqn | r = \ceiling {m \log_2 10}
      | c = 
}}
{{eqn | r = \ceiling {\dfrac m {\log_{10} 2} }
      | c = Reciprocal of Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Argument of x to the n Equals n Times The Argument

Let $z$ be a complex number.
Then:
:$\forall n \in \N_{>0}: \map \arg {z^n} = n \map \arg z$

Proof:
For $n = 1$
:$\map \arg {z^1} = 1 \cdot \map \arg z$
Assuming the result is true for $n = k$, we have:
{{begin-eqn}}
{{eqn | l = \map \arg {z^{k + 1} }
      | r = \map \arg {z z^k}
}}
{{eqn | r = \map \arg z + \map \arg {z^k}
      | c = Argument of Product equals Sum of Arguments
}}
{{eqn | r = \map \arg z + k \map \arg z
      | c = by our induction hypothesis
}}
{{eqn | r = \paren {k + 1} \map \arg z
}}
{{end-eqn}}
{{qed}}
q7sayp8wd0d8htaxqjuls43da5tek8v
Theorem: Exchange of Order of Summation/Example

Let the fiber of truth of both $R$ and $S$ be infinite.
Then it is not necessarily the case that:
:$\ds \sum_{\map R i} \sum_{\map S j} a_{i j} = \sum_{\map S j} \sum_{\map R i} a_{i j}$

Proof:
Proof by Counterexample:
{{proof wanted|No idea at the moment. Have to find a series of $a_{i j}$ which is conditionally convergent for a start.}}
Theorem: Sum of Geometric Sequence/Examples/Index to Minus 1

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Then the formula for Sum of Geometric Sequence:
:$\ds \sum_{j \mathop = 0}^n x^j = \frac {x^{n + 1} - 1} {x - 1}$
still holds when $n = -1$:
:$\ds \sum_{j \mathop = 0}^{-1} x^j = \frac {x^0 - 1} {x - 1}$

Proof:
The summation on the {{LHS}} is vacuous:
:$\ds \sum_{j \mathop = 0}^{-1} x^j = 0$
while on the {{RHS}} we have:
{{begin-eqn}}
{{eqn | l = \frac {x^{\paren {-1} + 1} - 1} {x - 1}
      | r = \frac {x^0 - 1} {x - 1}
      | c = 
}}
{{eqn | r = \frac 0 {x - 1}
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
as long as $x \ne 1$.
However, the theorem itself is based on the assumption that $n \ge 0$, so while the result is correct, the derivation to achieve it is not.
{{qed}}
Theorem: Sum of Geometric Sequence/Examples/Index to Minus 2

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Then the formula for Sum of Geometric Sequence:
:$\ds \sum_{j \mathop = 0}^n x^j = \frac {x^{n + 1} - 1} {x - 1}$
breaks down when $n = -2$:
:$\ds \sum_{j \mathop = 0}^{-2} x^j \ne \frac {x^{-1} - 1} {x - 1}$

Proof:
The summation on the {{LHS}} is vacuous:
:$\ds \sum_{j \mathop = 0}^{-2} x^j = 0$
while on the {{RHS}} we have:
{{begin-eqn}}
{{eqn | l = \frac {x^{\paren {-2} + 1} - 1} {x - 1}
      | r = \frac {x^{-1} - 1} {x - 1}
      | c = 
}}
{{eqn | r = \frac {1 / x - 1} {x - 1}
      | c = 
}}
{{eqn | r = \frac {\paren {1 - x} / x} {x - 1}
      | c = 
}}
{{eqn | r = \frac {1 - x} {x \paren {x - 1} }
      | c = 
}}
{{eqn | r = -\frac 1 x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Geometric Sequence/Examples/Common Ratio 1

Consider the Sum of Geometric Sequence defined on the standard number fields for all $x \ne 1$.
:$\ds \sum_{j \mathop = 0}^n a x^j = a \paren {\frac {1 - x^{n + 1} } {1 - x} }$
When $x = 1$, the formula reduces to:
:$\ds \sum_{j \mathop = 0}^n a 1^j = a \paren {n + 1}$

Proof:
When $x = 1$, the {{RHS}} is undefined:
:$a \paren {\dfrac {1 - 1^{n + 1} } {1 - 1} } = a \dfrac 0 0$
However, the {{LHS}} degenerates to:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^n a 1^j
      | r = \sum_{j \mathop = 0}^n a
      | c = 
}}
{{eqn | r = a \paren {n + 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Geometric Sequence/Examples/One Seventh from 1 to n

:$\ds \sum_{j \mathop = 0}^n \dfrac 1 {7^j} = \frac 7 6 \paren {1 - \frac 1 {7^{n + 1} } }$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^n \dfrac 1 {7^j}
      | r = \frac {1 - \frac 1 7^{n + 1} } {1 - \frac 1 7}
      | c = 
}}
{{eqn | r = \frac {7 - 7 \frac 1 7^{n + 1} } {7 - 1}
      | c = multiplying top and bottom by $7$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Sequence of n by 2 to the Power of n

:$\ds \sum_{j \mathop = 0}^n j \, 2^j = n \, 2^{n + 2} - \paren {n + 1} 2^{n + 1} + 2$

Proof:
From Sum of Arithmetic-Geometric Sequence:
:$\ds \sum_{j \mathop = 0}^n \paren {a + j d} r^j = \frac {a \paren {1 - r^{n + 1} } } {1 - r} + \frac {r d \paren {1 - \paren {n + 1} r^n + n r^{n + 1} } } {\paren {1 - r}^2}$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^n j \, 2^j
      | r = \frac {0 \paren {1 - 2^{n + 1} } } {1 - 2} + \frac {2 \times 1 \paren {1 - \paren {n + 1} 2^n + n 2^{n + 1} } } {\paren {1 - 2}^2}
      | c = putting $a = 0, d = 1, r = 2$
}}
{{eqn | r = 2 \paren {1 - \paren {n + 1} 2^n + n 2^{n + 1} }
      | c = initial simplification
}}
{{eqn | r = 2 - \paren {n + 1} 2^{n + 1} + n 2^{n + 2}
      | c = further simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Sequence of n by 2 to the Power of n

:$\ds \sum_{j \mathop = 0}^n j \, 2^j = n \, 2^{n + 2} - \paren {n + 1} 2^{n + 1} + 2$

Proof:
From Sum of Sequence of Power by Index:
:$\ds \sum_{j \mathop = 0}^n j x^j = \frac {n x^{n + 2} - \paren {n + 1} x^{n + 1} + x} {\paren {x - 1}^2}$
Hence:
{{begin-eqn}}
{{eqn | l = \ds \sum_{j \mathop = 0}^n j \, 2^j
      | r = \frac {n 2^{n + 2} - \paren {n + 1} 2^{n + 1} + 2} {\paren {2 - 1}^2}
      | c = putting $x = 2$
}}
{{eqn | r = n 2^{n + 2} - \paren {n + 1} 2^{n + 1} + 2
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Summation of Unity over Elements

Let $S \subseteq \Z$ be a set of integers.
Let:
:$n := \ds \sum_{j \mathop \in S} 1$
Then $n$ is equal to the cardinality of $S$.

Proof:
{{ProofWanted|It's hard to prove obvious things.}}
Theorem: Exchange of Order of Summation with Dependency on Both Indices/Example

Let $n \in \Z$ be an integer.
Let $R: \Z \to \set {\T, \F}$ be the propositional function on the set of integers defining:
:$\forall i \in \Z: \map R 1 := \paren {n = k i \text { for some } k \in \Z}$
Let $S: \Z \times \Z \to \set {\T, \F}$ be a propositional function on the Cartesian product of the set of integers with itself defining:
:$\forall i, j \in \Z: \map S {i, j} := \paren {1 \le j < i}$
Consider the summation:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j}$
Then:
:$\ds \sum_{\map R i} \sum_{\map S {i, j} } a_{i j} = \sum_{\map {S'} j} \sum_{\map {R'} {i, j} } a_{i j}$
where:
:$\map {S'} j$ denotes the propositional function:
::$\forall j \in \Z: \map {S'} j := \paren {1 < j \le n}$
:$\map {R'} {i, j}$ denotes the propositional function:
::$\forall i, j \in \Z: \map {R'} {i, j} := \paren {n = k i \text { for some } k \in \Z \text { and } i > j}$

Proof:
From Exchange of Order of Summation with Dependency on Both Indices:
:$\map {S'} j$ denotes the propositional function:
::there exists an $i$ such that both $\map R i$ and $\map S {i, j}$ hold
:$\map {R'} {i, j}$ denotes the propositional function:
::both $\map R i$ and $\map S {i, j}$ hold.
The definition of $\map {R'} {i, j}$ follows immediately:
:$\map R i := \paren {n = k i \text { for some } k \in \Z}$
and:
:$\map S {i, j} := \paren {1 \le j < i}$
Then:
{{begin-eqn}}
{{eqn | l = \map {S'} j
      | r = \paren {\exists i \in \Z: n = k i}
      | c = 
}}
{{eqn | o = 
      | ro= \land
      | r = \paren {1 \le j < i}
      | c = 
}}
{{end-eqn}}
By Absolute Value of Integer is not less than Divisors, it follows from $\map R i$ that $i \le n$.
That is, for $\map {S'} j$ to hold, $i \le n$.
But for all $j \in \Z$ such that $1 \le j < n$ it follows that $i = n$ fulfils the condition that $n = k i$.
Hence:
:$\map {S'} j := \paren {1 < j \le n}$
{{qed}}
Theorem: Hausdorff's Maximal Principle implies Zorn's Lemma

Hausdorff's Maximal Principle implies Zorn's Lemma.

Proof:
Let $\struct {\PP, \preceq}$ be a partially ordered set.
Hausdorff's Maximal Principle states that there is a maximal chain in $\struct {\PP, \preceq}$.
If this maximal chain has an upper bound in $\PP$, then such an upper bound is a maximal element of $\PP$ itself, by the maximality of the chain.
{{qed}}
Theorem: Zorn's Lemma Implies Zermelo's Well-Ordering Theorem

Zorn's Lemma implies Zermelo's Well-Ordering Theorem.

Proof:
Let $X$ be a set.
If $X = \O$ the theorem holds vacuously.
Assume $X$ is not empty.
Let $\WW$ be the collection of pairs $\tuple {W, \preceq}$ such that:
:$W \subseteq X$
:$\preceq$ well-orders $W$
Next, define the partial ordering $\preccurlyeq$ on $\WW$ by $\tuple {W, \preceq} \preccurlyeq \tuple {W', \preceq'}$ {{iff}}:
:$W \subseteq W'$
:$\preceq$ is the restriction of $\preceq'$ to $W$
:For all $w \in W$ and $w' \in W' \setminus W$: $w \preceq' w'$
To apply Zorn's Lemma, we need to show that every chain in $\WW$ has an upper bound.
Let $\CC \subseteq \WW$ be such a chain.
Then we claim $\bigcup \CC \in \WW$ and $\bigcup \CC$ is an upper bound for $\CC$, where we define $\bigcup \CC$ as:
:$\ds \bigcup \CC := \tuple { \bigcup_{ \tuple{W, \preceq} \in \CC } W, \bigcup_{ \tuple{W, \preceq} \in \CC } \preceq }$
First to show $\bigcup \CC \in \WW$.
By Union of Subsets is Subset: Set of Sets:
:$\ds \bigcup_{\tuple{W, \preceq} \mathop \in \CC} W \subseteq X$
Next, let $S \subseteq \bigcup_{\tuple {W, \preceq} \mathop \in \CC} W$ be non-empty.
Fix $s \in S$.
Then for some $\tuple {W, \preceq} \in \bigcup \CC$, we have $s \in W$.
Let $w$ be the smallest element of $S \cap W$ with respect to $\preceq$.
Now let $s' \in S$ be arbitrary.
If $s' \in W$, then $w \preceq s'$ and therefore $w \preceq_{\bigcup \CC} s'$.
If $s' \notin W$, then $s' \in W'$ for some $\tuple {W', \preceq'} \in \bigcup \CC$.
But since $\CC$ is a chain, we have:
:$\tuple {W, \preceq} \preccurlyeq \tuple {W', \preceq'}$
and therefore, $w \preceq' s'$ since $w \in W$ and $s' \in W' \setminus W$.
Then, by definition, $w \preceq_{\bigcup \CC} s'$.
Thus $w$ is the smallest element of $S$ and we conclude $\bigcup \CC$ is well-ordered.
Therefore $\bigcup \CC \in \WW$.
Now to show $\bigcup \CC$ is the sought upper bound of $\CC$.
We observe, for all $\tuple {W, \preceq} \in \CC$:
:$W \subseteq \bigcup_{\tuple {W, \preceq} \mathop \in \CC} W$ by Set is Subset of Union
:$\preceq$ is the restriction of $\preceq_{\bigcup \CC}$ to $W$
:For all $w \in W$ and $w' \in \bigcup \CC \setminus W$, $w \preceq_{\bigcup \CC} w'$
and conclude that:
:$\ds \tuple {W, \preceq} \preccurlyeq \bigcup \CC$
That is, $\ds \bigcup \CC$ is an upper bound of $\CC$.
Thus the hypotheses of Zorn's Lemma hold and we can conclude that $\WW$ has a maximal element.
Let $\tuple {E, \preceq}$ be the maximal element of $\WW$.
Suppose that $E \ne X$.
Then there exists $x_0 \in X \setminus E$. 
Define an ordering $\preceq'$ on $E \cup \set {x_0}$ as follows:
:$y \preceq' x$ {{iff}} $x = x_0$ or $x, y \in E$ and $y \preceq x$.
This is a well-order on $E \cup \set {x_0}$ with:
:$\struct {E, \preceq} \preccurlyeq \struct {E \cup \set {x_0}, \preceq'}$
This contradicts that $\tuple {E, \preceq}$ is the maximal element of $\WW$. 
So $E = X$. 
Hence $X$ is well-orderable.
{{qed}}
Theorem: Uncountable Sum as Series

Let $X$ be an uncountable set.
Let $f: X \to \closedint 0 {+\infty}$ be an extended real-valued function.
The uncountable sum:
:$\ds \sum_{x \mathop \in X} \map f x = \sup \set {\sum_{x \mathop \in F} \map f x : F \subseteq X, F \text{ finite} }$
is:
:if $f$ has uncountably infinite support, then $+\infty$ 
:Otherwise, can be expressed as a (possibly divergent) series.

Proof:
Define:
:$A_n = \set {x \in X: \map f x >\dfrac 1 n, n \in \N_{\ge 1} }$
Then $\sequence {A_n}_{n \mathop \in \N} \uparrow A$ is an exhausting sequence of sets, where:
:$A = \set {x \in X: \map f x > 0}$
Suppose $A$ is uncountable.
From Countable Union of Countable Sets is Countable, necessarily there is some $A_{n_0}$ which is uncountable.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{x \mathop \in X} \map f x
      | r = \sup \set {\sum_{x \mathop \in F} \map f x: F \subseteq X, F \text{ finite} }
}}
{{eqn | o = \ge
      | r = \sup \set {\sum_{x \mathop \in F} \map f x: F \subseteq A_{n_0}, F \text{ finite} }
}}
{{eqn | o = \ge 
      | r = \sup \set {\sum_{x \mathop \in F} \frac 1 {n_0} : F \subseteq A_{n_0}, F \text{ finite} }
}}
{{eqn | r = \sum_{n \mathop = 1}^{\infty} \frac 1 {n_0}
}}
{{eqn | r = +\infty
}}
{{end-eqn}}
Thus:
:$\ds \sum_{x \mathop \in X} \map f x = +\infty$
Otherwise, suppose then that $A$ is countably infinite.
Then there is a bijection $g: \N \to A$
Define $B_N = g \sqbrk {\set {1, 2, \ldots, N - 1, N} }$
Then every finite subset $F$ of $A$ is contained in some $B_N$.
This implies the inequality:
:$\ds \sum_{x \mathop \in F} \map f x \le \sum_{n \mathop = 1}^N \map f {\map g n} \le \sum_{x \mathop \in X} \map f x$
for each $F$ finite.
Taking the supremum of this inequality over $N$:
:$\ds \sum_{x \mathop \in F} \map f x \le \sum_{n \mathop = 1}^\infty \map f {\map g n} \le \sum_{x \mathop \in X} \map f x$
Taking the supremum of this inequality over $F$:
:$\ds \sum_{x \mathop \in X} \map f x \le \sum_{n \mathop = 1}^\infty \map f {\map g n} \le \sum_{x \mathop \in X} \map f x$
Thus:
:$\ds \sum_{x \mathop \in X} \map f x = \sum_{n \mathop = 1}^\infty \map f {\map g n}$ 
for some bijection $g: \N \to A$
{{qed}}
Theorem: Sum with Maximum is Maximum of Sum

Let $a, b, c \in \R$ be real numbers.
Then:
:$a + \max \set {b, c} = \max \set {a + b, a + c}$

Proof:
{{WLOG}}, there are two cases to consider:
:$(1): \quad b \ge c$
:$(2): \quad b < c$
First let $b \ge c$.
We have:
{{begin-eqn}}
{{eqn | l = b
      | o = \ge
      | r = c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + b
      | o = \ge
      | r = a + c
      | c = Addition of Real Numbers is Compatible with Usual Ordering
}}
{{eqn | ll= \leadsto
      | l = \max \set {a + b, a + c}
      | r = a + b
      | c = {{Defof|Maximum Element}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a + \max \set {b, c}
      | r = a + b
      | c = {{Defof|Maximum Element}}
}}
{{eqn | r = \max \set {a + b, a + c}
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Now let $b < c$.
We have:
{{begin-eqn}}
{{eqn | l = b
      | o = <
      | r = c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + b
      | o = <
      | r = a + c
      | c = Addition of Real Numbers is Compatible with Usual Ordering
}}
{{eqn | ll= \leadsto
      | l = \max \set {a + b, a + c}
      | r = a + c
      | c = {{Defof|Maximum Element}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = a + \max \set {b, c}
      | r = a + c
      | c = {{Defof|Maximum Element}}
}}
{{eqn | r = \max \set {a + b, a + c}
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Thus the result holds in both cases.
Hence the result, by Proof by Cases.
{{qed}}
Theorem: Sum of Indexed Suprema

Let $\sequence {a_i}_{i \mathop \in I}$ be a family of elements of the real numbers $\R$ indexed by $I$.
Let $\sequence {b_j}_{j \mathop \in J}$ be a family of elements of the real numbers $\R$ indexed by $J$.
Let $\map R i$ and $\map S j$ be propositional functions of $i \in I$, $j \in J$.
Let $\ds \sup_{\map R i} a_i$ and $\ds \sup_{\map S j} b_j$ be the indexed suprema on $\sequence {a_i}$ and $\sequence {b_j}$ respectively.
Then:
:$\ds \paren {\sup_{\map R i} a_i} + \paren {\sup_{\map S j} b_j} = \sup_{\map R i} \paren {\sup_{\map S j} \paren {a_i + b_j} }$

Proof:
{{improve|The results upon which this depends need to be enhanced to encompass the full supremum, not just the max}}
{{begin-eqn}}
{{eqn | l = \paren {\sup_{\map R i} a_i} + \paren {\sup_{\map S j} b_j}
      | r = \sup_{\map R i} \paren {a_i + \sup_{\map S j} b_j}
      | c = Sum with Maximum is Maximum of Sum
}}
{{eqn | r = \sup_{\map R i} \paren {\sup_{\map S j} \paren {a_i + b_j} }
      | c = Sum with Maximum is Maximum of Sum
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Indexed Suprema of Non-Negative Numbers

Let $\family {a_i}_{i \mathop \in I}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $I$.
Let $\family {b_j}_{j \mathop \in J}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $J$.
Let $\map R i$ and $\map S j$ be propositional functions of $i \in I$, $j \in J$.
Let $\ds \sup_{\map R i} a_i$ and $\ds \sup_{\map S j} b_j$ be the indexed suprema on $\family {a_i}$ and $\family {b_j}$ respectively.
Then:
:$\ds \paren {\sup_{\map R i} a_i} \paren {\sup_{\map S j} b_j} = \sup_{\map R i} \paren {\sup_{\map S j} \paren {a_i b_j} }$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {\sup_{\map R i} a_i} \paren {\sup_{\map S j} b_j}
      | r = \sup_{\map R i} \paren {a_i \times \sup_{\map S j} b_j}
      | c = Product with Supremum is Supremum of Product of Non-Negative Numbers
}}
{{eqn | r = \sup_{\map R i} \paren {\sup_{\map S j} \paren {a_i b_j} }
      | c = Product with Supremum is Supremum of Product of Non-Negative Numbers
}}
{{end-eqn}}
{{qed}}
Theorem: Change of Index Variable of Supremum

Let $\family {a_i}_{i \mathop \in I}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $I$.
Let $\map R i$ be a propositional functions of $i \in I$.
Let $\ds \sup_{\map R i} a_i$ be the indexed supremum on $\family {a_i}$.
Then:
:$\ds \sup_{\map R i} a_i = \sup_{\map R j} a_j$

Proof:
{{ProofWanted|If anybody is keen on proving obvious things}}
Theorem: Permutation of Indices of Supremum

Let $\family {a_i}_{i \mathop \in I}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $I$.
Let $\map R i$ be a propositional functions of $i \in I$.
Let $\ds \sup_{\map R i} a_i$ be the indexed supremum on $\family {a_i}$.
Then:
:$\ds \sum_{\map R i} a_i = \sum_{\map R {\map \pi i} } a_{\map \pi i}$
where $\pi$ is a permutation on the fiber of truth of $R$.

Proof:
{{begin-eqn}}
{{eqn | l = \sup_{\map R {\map \pi j} } a_{\map \pi j}
      | r = \sup_{j \mathop \in I} a_{\map \pi j} \sqbrk {\map R {\map \pi j} }
      | c = 
}}
{{eqn | r = \sup_{j \mathop \in I} \paren {\sup_{i \mathop \in I} a_i \sqbrk {\map R i} \sqbrk {i = \map \pi j} }
      | c = 
}}
{{eqn | r = \sup_{i \mathop \in I} a_i \sqbrk {\map R i} \sup_{j \mathop \in I} \sqbrk {i = \map \pi j}
      | c = 
}}
{{eqn | r = \sup_{i \mathop \in I} a_i \sqbrk {\map R i}
      | c = 
}}
{{eqn | r = \sup_{\map R i} a_i
      | c = 
}}
{{eqn | r = \sup_{\map R j} a_j
      | c = Change of Index Variable of Supremum
}}
{{end-eqn}}
{{qed}}
Theorem: Exchange of Order of Supremum Operators

Let $\family {a_i}_{i \mathop \in I}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $I$.
Let $\family {b_j}_{j \mathop \in J}$ be a family of elements of the non-negative real numbers $\R_{\ge 0}$ indexed by $J$.
Let $\map R i$ and $\map S j$ be propositional functions of $i \in I$, $j \in J$.
Let $\ds \sup_{\map R i} a_i$ and $\ds \sup_{\map S j} b_j$ be the indexed suprema on $\family {a_i}$ and $\family {b_j}$ respectively.
Then:
:$\ds \sup_{\map R i} \paren {\sup_{\map S j} a_{i j} } = \sup_{\map S j} \paren {\sup_{\map R i} a_{i j} }$

Proof:
For any chosen $i$ and $j$, we have:
:$\ds a_{ij} \le \sup_{\map R i} a_{ij}$
Taking the supremum over $\map S j$ yields:
:$\ds \sup_{\map S j} a_{ij} \le \sup_{\map S j} \sup_{\map R i} a_{ij}$
for all $i$.
Hence the {{RHS}} remains an upper bound after taking the supremum over $\map R i$ on the {{LHS}}.
That is:
:$\ds \sup_{\map R i} \paren {\sup_{\map S j} a_{ij} } \le \sup_{\map S j} \paren {\sup_{\map R i} a_{ij} }$
Applying the same argument with $\ds a_{ij} \le \sup_{\map S j} a_{ij}$, we obtain the reverse inequality.
{{qed}}
Theorem: Contour Integration by Substitution

Let $f$ be a holomorphic function on a simply connected domain $V \subseteq \mathbb C$.
Let $\gamma$ be a contour in $V$ starting at $z_1$ and ending at $z_2$.
Let $U$ be a connected domain.
Let $\phi: U \to V$ be a holomorphic function with $\phi^{-1} \sqbrk {\set {z_1, z_2} } \ne \O$.
Let $\omega$ be a contour in $U$ starting at $u_1$ and ending at $u_2$, such that $\map \phi {u_1} = z_1$ and $\map \phi {u_2} = z_2$.
Then the contour integral of $f$ over $\gamma$ satisfies the following substitution:
:$\ds \int_\gamma \map f z \rd z = \int_\omega \map f {\map \phi u} \map {\phi'} u \rd u$

Proof:
{{MissingLinks|relationship between holomorphic on s.c. domain and having a primitive}}
Because $V$ is simply connected, $f$ has a primitive.
Let one such primitive $F$ be established.
By the Fundamental Theorem of Calculus for Contour Integrals:
{{begin-eqn}}
{{eqn | l = I_1
      | r = \int_\gamma \map f z \rd z
      | c = 
}}
{{eqn | r = \map F {z_2} - \map F {z_1}
      | c = 
}}
{{end-eqn}}
Next, observe that $\map f {\map \phi u} \map {\phi'} u$ also has a primitive, that is $\map F {\map \phi u}$.
Again by the Fundamental Theorem of Calculus for Contour Integrals:
{{begin-eqn}}
{{eqn | l = I_2
      | r = \int_\omega \map f {\map \phi u} \map {\phi'} u \rd u
      | c = 
}}
{{eqn | r = \map F {\map \phi {u_2} } - \map F {\map \phi {u_1} }
      | c = 
}}
{{end-eqn}}
Because $\map \phi {u_1} = z_1$, we have that:
:$\map F {\map \phi {u_1} } = \map F {z_1}$
and likewise for $\map \phi {u_2}$. 
Thus $I_1 = I_2$.
{{qed}}
Category:Complex Analysis
qqcn55cra97yiiqqpdca84kxic39ffg
Theorem: Infimum of Set of Integers is Integer

Let $S \subset \Z$ be a non-empty subset of the set of integers.
Let $S$ be bounded below in the set of real numbers.
Then its infimum $\inf S$ is an integer.

Proof:
By Infimum of Set of Integers equals Smallest Element, $S$ has a smallest element $n \in \Z$, that is equals to the infimum of $S$.
{{qed}}
Theorem: Infimum of Set of Integers equals Smallest Element

Let $S \subset \Z$ be a non-empty subset of the set of integers.
Let $S$ be bounded below in the set of real numbers $\R$.
Then $S$ has a smallest element, and it is equal to the infimum $\sup S$.

Proof:
By Set of Integers Bounded Below by Real Number has Smallest Element, $S$ has a smallest element, say $n \in S$.
By Smallest Element is Infimum, $n$ is the infimum of $S$.
{{qed}}
Theorem: Greatest Element is Supremum

Let $\struct {S, \preceq}$ be an ordered set.
Let $T \subseteq S$.
Let $T$ have a greatest element $M$.
Then $M$ is the supremum of $T$ in $S$.

Proof:
Let $M$ be the greatest element of $T$.
Then by definition:
:$\forall x \in T: x \preceq M$
By definition of supremum, it is necessary to show that:
:$(1): \quad M$ is an upper bound of $T$ in $S$
:$(2): \quad M \preceq U$ for all upper bounds $U$ of $T$ in $S$.
By Greatest Element is Upper Bound, $M$ is an upper bound of $T$ in $S$.
It remains to be shown that:
:$M \preceq U$ for all upper bounds $U$ of $T$ in $S$.
Let $U \in S$ be an upper bound of $T$ in $S$.
By definition of upper bound:
:$\forall t \in T: t \preceq U$
We have that $M \in T$.
Therefore:
:$M \preceq U$
Hence the result.
{{qed}}