avewright/proofwiki-math huggingface dataset:
Theorem: Necessary and Sufficient Condition for Integral Parametric Functional to be Independent of Parametric Representation

Let $x: \R \to \R$ and $y: \R \to \R$ be real functions.
Let $J \sqbrk {x, y}$ be a functional of the form:
:$\ds J \sqbrk {x, y} = \int_{t_0}^{t_1} \map \Phi {t, x, y, \dot x, \dot y} \rd t$
where $\dot y$ denotes the derivative of $y$ {{WRT|Differentiation}} $t$:
:$\dot y = \dfrac {\d y} {\d t}$
Then $J \sqbrk {x, y}$ depends only on the curve in the $x y$-plane defined by the parametric equations:
:$x = \map x t$, $y = \map y t$ 
and not on the choice of the parametric representation of the curve {{iff}} the integrand $\Phi$ does not involve $t$ explicitly 
and is a positive-homogeneous function of degree $1$ in $\dot x$ and $\dot y$.

Proof:
In the functional:
:$\ds \JJ \sqbrk y = \int_{x_0}^{x_1} \map F {x, y, y'} \rd x$
let the argument $y$ stand for a curve which is given in a parametric form. 
In other words, let the curve be described by the vector $\tuple {\map y t,\map x t}$ rather than $\paren {\map y x, x}$.
Then the functional can be rewritten as:
{{begin-eqn}}
{{eqn | l = \JJ \sqbrk y
      | r = \int_{t_0}^{t_1} F \sqbrk {\map x t, \map y t, \frac {\d \, \map y t} {\d \, \map x t} } \rd \map x t
}}
{{eqn | r = \int_{t_0}^{t_1} F \sqbrk {\map x t, \map y t, \frac {\frac {\d y} {\d t} } {\frac {\d x} {\d t} } } \frac {\d x} {\d t} \rd t
}}
{{eqn | r = \int_{t_0}^{t_1} F \sqbrk {\map x t, \map y t, \frac {\map {\dot y} t} {\map {\dot x} t} } \map {\dot x} t \rd t
}}
{{eqn | r = \int_{t_0}^{t_1} \map \Phi {x, y, \dot x, \dot y} \rd t
}}
{{end-eqn}}
The function on the {{RHS}} does not involve $t$ explicitly.
Suppose that it is positive-homogeneous of degree 1 in $\map {\dot x} t$ and $\map {\dot y} t$:
:$\map \Phi {x, y, \lambda \dot x, \lambda \dot y} = \lambda \map \Phi {x, y, \dot x, \dot y}$ for all $\lambda > 0$.
Now we will show that the value of such functional depends only on the curve in the $x y$-plane defined by the parametric equations $x = \map x t$ and $y = \map y t$, and not on the functions $\map x t$, $\map y t$ themselves. 
Let a new parameter $\tau$ be chosen such that $t = \map t \tau$, where $\dfrac {\d t} {\d \tau} > 0$.
Let the interval $\closedint {t_0} {t_1}$ be mapped onto $\closedint {\tau_0} {\tau_1}$.
Since $\Phi$ is positive-homogeneous of degree $1$ in $\dot x$ and $\dot y$, it follows that:
{{begin-eqn}}
{{eqn | l = \int_{\tau_0}^{\tau_1} \map \Phi {x, y, \frac {\d x} {\d \tau}, \frac {\d y} {\d \tau} } \rd \tau
      | r = \int_{\tau_0}^{\tau_1} \map \Phi {x, y, \dot x \frac {\d t} {\d \tau}, \dot y \frac {\d t} {\d \tau} } \rd \tau
      | c = Chain Rule for Derivatives: $\dfrac {\d x} {\d \tau} = \dfrac {\d x} {\d t} \dfrac {\d t} {\d \tau}$
}}
{{eqn | r = \int_{\tau_0}^{\tau_1} \map \Phi {x, y, \dot x, \dot y} \frac {\d t} {\d \tau} \rd \tau
}}
{{eqn | r = \int_{t_0}^{t_1} \map \Phi {x, y, \dot x, \dot y} \rd t
}}
{{end-eqn}}
{{qed}}
{{proof wanted|seems that only one condition is proven; check for the other one}}
Theorem: Intersection of Upper Section with Directed Set is Directed Set

Let $L = \struct {S, \preceq}$ be an ordered set.
Let $A, B$ be subsets of $S$ such that
:$A \cap B \ne \O$
and
:$A$ is an upper set,
:$B$ is a directed set.
Then $A \cap B$ is a directed set.

Proof:
Let $x, y \in A \cap B$.
By definition of intersection:
:$x, y \in A$ and $x, y \in B$
By definition of directed subset:
:$\exists z \in B: x \preceq z \land y \preceq z$
By definition of upper section:
:$z \in A$
Thus by definition of intersection:
:$z \in A \cap B$
Thus:
:$\exists z \in A \cap B: x \preceq z$ and $y \preceq z$
{{qed}}
Theorem: Convex Set is Contractible

Let $V$ be a topological vector space over $\R$ or $\C$.
Let $A\subset V$ be a convex subset.
Then $A$ is contractible.

Proof:
{{WIP|Lots of imprecision and incorrect grammar which needs to be resolved. Too much to do on the fly}}
Let $x_0 \in A$.
Define $H : A \times \closedint 0 1 \to A$ by:
:$\map H {x, t} = t x_0 + \paren {1 - t} x$
Note that by the definition of a convex set, $\Cdm H$ is also a convex set.
{{Proofread|Verify if the codomain of H is convex}}
Let $I_A$ be defined as the identity mapping: 
:$I_A: A \to A$
Such that:
:$I_A = \set {\tuple {x, x}: x \in A}$
Let $S$ and $T$ be sets. Let $x_0$ be defined as the constant map:
:$x_0: S \to T$ defined as:
:$0 \in T: x_0: S \to T: \forall x \in S: \map {x_0} x = 0$
{{Proofread|Verify if the definition is used correctly}}
The map $H$ yields a (free) homotopy between the identity map:
:$I_A$
and the constant map:
:$x_0$
{{Finish|Prove that the map H yields a homotopy between the identity map and the constant map}}
By the assumption of convexity for $A$, $H$ takes values in $A$.
Since $H$ is a polynomial separately in $x, t$, it is a continuous function.
And:
:$\map H {-, 0} = I_A$
:$\map H {-, 1} \equiv x_0$ (the constant function) 
Thus, $H: I_A \simeq c_{x_0}$.
{{Finish|Prove that the above statement implies that the identity map on A is homotopic to the constant map from A to A}}
It follows that, the identity map $\operatorname{id}_A$ is homotopic to the constant map $A \to A$.
Hence, by definition of a contractible space, this implies that:
:$A$ is contractible
as required.
{{qed}}
Category:Vector Spaces
Category:Topology
Category:Convex Sets (Vector Spaces)
oeqfc6bym78em4gret2eataiws5yly9
Theorem: Open Subgroup is Closed

Let $G$ be a topological group.
Let $H\leq G$ be an open subgroup.
Then $H$ is closed.

Proof:
By Right and Left Regular Representations in Topological Group are Homeomorphisms, the left cosets of $H$ are open.
By Left Coset Space forms Partition, the complement of $H$ is a union of left cosets of $H$.
Because the complement of $H$ is open, $H$ is closed.
{{qed}}
Category:Topology
Category:Group Theory
Category:Topological Groups
ppam4e1on2bq4v6hnwnnxn4ast6zz5o
Theorem: Topological Group is Hausdorff iff Identity is Closed

Let $G$ be a topological group.
Let $e$ be its identity element.
Then $G$ is a $T_2$ (Hausdorff) space {{iff}} $\set e$ is closed in $G$.

Proof:
=== Necessary Condition ===
Suppose $G$ is a $T_2$ (Hausdorff) space.
By $T_2$ Space is $T_1$ Space, $\set e$ is closed.
{{qed|lemma}}
Theorem: Topological Group is T1 iff T2

Let $G$ be a topological group.
Then $G$ is a $T_1$ space {{iff}} $G$ is a $T_2$ (Hausdorff) space.

Proof:
=== Necessary Condition ===
Follows directly from $T_2$ Space is $T_1$ Space.
{{qed|lemma}}
Theorem: Jensen's Inequality (Complex Analysis)

Let $D \subset \C$ be an open set with $0 \in D$.
Let $R > 0$ be such that $\map B {0, R} \subset D$.
Let $f: D \to \C$ be analytic with $\map f 0 \ne 0$.
Let $\cmod {\map f z} \le M$ for $\cmod z \le R$.
Let $0 < r <R$.
Then the number of zeroes of $f$, counted with multiplicity, for $\cmod z \le r$, is at most:
:$\dfrac {\map \log {M / \cmod {\map f 0} } } {\map \log {R / r} }$

Proof:
{{ProofWanted}}
{{Namedfor|Johan Jensen|cat = Jensen}}
Theorem: Complement of Subset with Property (S) is Closed under Directed Suprema

Let $L = \struct {S, \preceq}$ be an up-complete ordered set.
Let $X$ be a subset of $S$ with property (S).
Then $\relcomp S X$ is closed under directed suprema.

Proof:
Let $D$ be a directed subset of $S$ such that:
:$D \subseteq \relcomp S X$
{{AimForCont}}
:$\sup D \notin \relcomp S X$
By definition of relative complement:
:$\sup D \in X$
By definition of property (S):
:$\exists y \in D: \forall x \in D: y \preceq x \implies x \in X$
By definition of reflexivity:
:$y \in X$
By definitions of intersection and non-empty:
:$D \cap X \ne \O$
Thus this by Empty Intersection iff Subset of Complement contradicts:
:$D \subseteq \relcomp S X$
{{qed}}
Theorem: Lifting The Exponent Lemma for Sums

Let $x, y \in \Z$ be integers with $x + y \ne 0$.
Let $n \ge 1$ be an odd natural number.
Let $p$ be an odd prime.
Let:
:$p \divides x + y$
and:
:$p \nmid x y$
where $\divides$ and $\nmid$ denote divisibility and non-divisibility respectively.
Then:
:$\map {\nu_p} {x^n + y^n} = \map {\nu_p} {x + y} + \map {\nu_p} n$
where $\nu_p$ denotes $p$-adic valuation.
</onlyinclude>

Proof:
This follows from the Lifting The Exponent Lemma with $y$ replaced by $-y$.
{{qed}}
Theorem: Lifting The Exponent Lemma for p=2

Let $x, y \in \Z$ be distinct odd integers.
Let $n \ge 1$ be a natural number.
Let:
:$4 \divides x - y$
where $\divides$ denotes divisibility.
Then
:$\map {\nu_2} {x^n - y^n} = \map {\nu_2} {x - y} + \map {\nu_2} n$
where $\nu_2$ denotes $2$-adic valuation.

Proof:
Let $k = \map {\nu_2} n$.
Then $n = 2^k m$ with $2 \nmid m$.
By $p$-adic Valuation of Difference of Powers with Coprime Exponent:
:$\map {\nu_2} {x^n - y^n} = \map {\nu_2} {x^{2^k} - y^{2^k} }$
Note that:
:$x^{2^k} - y^{2^k} = \paren {x - y} \cdot \ds \prod_{i \mathop = 0}^{k - 1} \paren {x^{2^i} + y^{2^i} }$
By Square Modulo 4:
:$\map {\nu_2} {x^{2^i} + y^{2^i} } = 1$
for $i > 0$.
Because $4 \divides \paren {x - y}$, $4 \nmid \paren {x + y}$.
Thus:
:$\map {\nu_2} {x + y} = 1$
Thus:
{{begin-eqn}}
{{eqn | l = \map {\nu_2} {x^{2^k} - y^{2^k} }
      | r = \map {\nu_2} {x - y} + \sum_{i \mathop = 0}^{k - 1} \map {\nu_2} {x^{2^i} + y^{2^i} }
      | c = $p$-adic Valuation is Valuation: Valuation Axiom $\text V 1$
}}
{{eqn | r = \map {\nu_2} {x - y} + k
}}
{{end-eqn}}
{{qed}}
Theorem: Classification of Convex Polyhedra whose Faces are Regular Polygons

The convex polyhedra whose faces are all regular polygons are as follows:
:The $5$ Platonic solids
:The uniform prisms and uniform antiprisms, countably infinite in number
:The $13$ Archimedean polyhedra
:The $92$ Johnson polyhedra.

Proof:
The Platonic solids are the convex polyhedra all of whose faces are congruent and whose vertices are regular.
From Five Platonic Solids, there are $5$ of these.
The uniform prisms are made from two regular polygons of an arbitrary number of sides forming the bases, separated by as many squares as there are sides of the two bases, forming the lateral faces.
From Uniform Prisms are Countably Infinite, they form a countably infinite set.
Note that when the bases are themselves squares, the uniform prism is then a cube, and so has already been counted amongst the Platonic solids.
The uniform antiprisms are made from two regular polygons of an arbitrary number of sides forming the bases, separated by twice as many equilateral triangles as there are sides of the two bases, forming the lateral faces.
From Uniform Antiprisms are Countably Infinite, they form a countably infinite set.
Note that when the bases are themselves equilateral triangles, the uniform antiprism is then a regular octahedron, and so has already been counted amongst the Platonic solids.
The Archimedean polyhedra consist of all isogonal convex polyhedra whose faces are all regular polygons, excluding:
:the Platonic solids
:the uniform prisms
:the uniform antiprisms.
From Thirteen Archimedean Polyhedra, there are $13$ of these.
The Johnson polyhedra are all the other convex polyhedra whose faces are all regular polygons.
From 92 Johnson Polyhedra, there are $92$ of these.
{{qed}}
Theorem: Chinese Remainder Theorem/General Result

Let $n_1, n_2, \ldots, n_k$ be positive integers.
Let $b_1, b_2, \ldots, b_k$ be integers such that:
:$\forall i \ne j: \gcd \set {n_i, n_j} \divides b_i - b_j$
Then the system of linear congruences:
{{begin-eqn}}
{{eqn | l = x
      | o = \equiv
      | r = b_1
      | rr = \pmod {n_1}
}}
{{eqn | l = x
      | o = \equiv
      | r = b_2
      | rr = \pmod {n_2}
}}
{{eqn | o = \vdots
}}
{{eqn | l = x
      | o = \equiv
      | r = b_k
      | rr = \pmod {n_k}
}}
{{end-eqn}}
has a simultaneous solution which is unique modulo $\lcm \set {n_1, \ldots, n_k}$.

Proof:
=== Existence ===
We prove this by induction on $k$.
Theorem: Logarithm of Infinite Product of Complex Numbers

Let $\sequence {z_n}$ be a sequence of nonzero complex numbers.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|The infinite product $\ds \prod_{n \mathop {{=}} 1}^\infty z_n$ converges to $z \in \C_{\ne 0}$.}}
{{item|(2):|The series $\ds \sum_{n \mathop {{=}} 1}^\infty \log z_n$ converges to $\log z + 2 k \pi i$ for some integer $k \in \Z$.}}
{{end-itemize}}

Proof:
=== $(1)$ implies $(2)$ ===
Suppose $\ds \prod_{n \mathop = 1}^\infty z_n$ converges to $z$.
By Convergence of Series of Complex Numbers by Real and Imaginary Part, it suffices to show that:
:$\ds \sum_{n \mathop = 1}^\infty \Re \log z_n = \Re \log z$
:$\ds \sum_{n \mathop = 1}^\infty \Im \log z_n = \Im \log z + 2 k \pi$
Theorem: Equivalence of Definitions of Absolute Convergence of Product of Complex Numbers

Let $\sequence {a_n}$ be a sequence of complex numbers.
Let $\log$ denote the complex logarithm.
{{TFAE|def = Absolute Convergence of Product}}

Proof:
=== 1 iff 2 ===
Follows directly from Equivalence of Definitions of Absolute Convergence of Product.
{{qed}}
Theorem: Square of Quadratic Gauss Sum

Let $p$ be an odd prime.
Let $a$ be an integer coprime to $p$.
Let $\map g {a, p}$ denote the quadratic Gauss sum of $a$ and $p$.
Then:
:$\map g {a, p}^2 = \paren {\dfrac {-1} p} \cdot p$

Proof:
{{proof wanted}}
Category:Number Theory
sbtg7mjhsmx6mt58lwwambdm1bzoxea
Theorem: Absolutely Convergent Product is Convergent

Let $\struct {\mathbb K, \norm {\,\cdot\,} }$ be a valued field.
Let $\mathbb K$ be complete.
Let the infinite product $\ds \prod_{n \mathop = 1}^\infty \paren {1 + a_n}$ be absolutely convergent.
Then it is convergent.

Proof:
Let $P_n$ and $Q_n$ denote the $n$th partial products of $\ds \prod_{n \mathop = 1}^\infty \paren {1 + a_n}$ and $\ds \prod_{n \mathop = 1}^\infty \paren {1 + \norm {a_n} }$ respectively.
We show that $\sequence {P_n}$ is Cauchy.
We have, for $m > n$:
{{begin-eqn}}
{{eqn | l = \norm {P_m - P_n}
      | r = \prod_{k \mathop = 1}^n \norm {1 + a_k} \cdot \norm {\prod_{k \mathop = n + 1}^m \paren {1 + a_k} - 1}
      | c = 
}}
{{eqn | o = }}
{{eqn | o = \le
      | r = \prod_{k \mathop = 1}^n \paren {1 + \norm {a_k} } \paren {\prod_{k \mathop = n + 1}^m \paren {1 + \norm {a_k} } - 1}
      | c = 
}}
{{eqn | o = }}
{{eqn | r = Q_m - Q_n
      | c = 
}}
{{end-eqn}}
Because $\sequence {Q_n}$ converges, $\sequence {Q_n}$ is Cauchy.
By the above inequality, $\sequence {P_n}$ is Cauchy.
Because $\mathbb K$ is complete, $\sequence {P_n}$ converges to some $a \in \mathbb K$.
By Absolutely Convergent Product Does not Diverge to Zero, the product converges.
{{qed}}
Category:Infinite Products
m4zibqgdhcfj6y9sr2er8czd27twrc6
Theorem: Complement of Closed under Directed Suprema Subset is Inaccessible by Directed Suprema

Let $L = \struct {S, \preceq}$ be an up-complete ordered set.
Let $X$ be a closed under directed suprema subset of $S$.
Then $\relcomp S X$ is inaccessible by directed suprema.

Proof:
Let $D$ be a directed subset of $S$ such that
:$\sup D \in \relcomp S X$
By definition of relative complement:
:$\sup D \notin X$
By definition of closed under directed suprema:
:$D \nsubseteq X$
By Complement of Complement:
:$D \nsubseteq \relcomp S {\relcomp S X}$
Thus by Empty Intersection iff Subset of Relative Complement:
:$D \cap \relcomp S X \ne \O$
{{qed}}
Theorem: Complement of Upper Section is Lower Section

Let $\struct {S, \preceq}$ be an ordered set.
Let $L$ be an upper section.
Then $S \setminus L$ is a lower section.

Proof:
This follows {{mutatis}} from the proof of Complement of Lower Section is Upper Section.
{{qed}}
Theorem: Closed Set iff Lower and Closed under Directed Suprema in Scott Topological Ordered Set

Let $T = \struct {S, \preceq, \tau}$ be a relational structure with Scott topology
where $\struct {S, \preceq}$ is an up-complete ordered set.
Let $A$ be a subset of $S$.
Then $A$ is closed {{iff}} $A$ is lower and closed under directed suprema.

Proof:
=== Sufficient Condition ===
Assume that
:$A$ is closed.
By definition of closed set:
:$\relcomp S A \in \tau$
By definition of Scott topology:
:$\relcomp S A$ is upper and inaccessible by directed suprema.
By Complement of Complement:
:$\relcomp S {\relcomp S A} = A$
Thus by Complement of Upper Section is Lower Section:
:$A$ is a lower section.
Thus by Complement of Inaccessible by Directed Suprema Subset is Closed under Directed Suprema:
:$A$ is closed under directed suprema.
{{qed|lemma}}
Theorem: Complement of Inaccessible by Directed Suprema Subset is Closed under Directed Suprema

Let $L = \struct {S, \preceq}$ be an up-complete ordered set.
Let $X$ be an inaccessible by directed suprema subset of $S$.
Then $\relcomp S X$ is closed under directed suprema.

Proof:
Let $D$ be a directed subset of $S$ such that
:$D \subseteq \relcomp S X$
By Empty Intersection iff Subset of Relative Complement:
:$D \cap X = \O$
By definition of inaccessible by directed suprema:
:$\sup D \notin X$
Thus by definition of relative complement:
:$\sup D \in \relcomp S X$
{{qed}}
Theorem: Convergence of Complex Sequence in Polar Form

Let $z \ne 0$ be a complex number with modulus $r$ and argument $\theta$.
Let $\sequence {z_n}$ be a sequence of nonzero complex numbers.
Let $r_n$ be the modulus of $z_n$ and $\theta_n$ be an argument of $z_n$.
Then $z_n$ converges to $z$ {{iff}} the following hold:
:$(1): \quad r_n$ converges to $r$
:$(2): \quad$ There exists a sequence $\sequence {k_n}$ of integers such that $\theta_n + 2 k_n \pi$ converges to $\theta$.

Proof:
Suppose $r_n \to r$ and $\theta_n + 2 k_n \pi \to \theta$.
We have, by Complex Modulus of Difference of Complex Numbers:
{{begin-eqn}}
{{eqn  | l = \cmod {z_n - z}^2
       | r = r_n^2 + r^2 - 2 r r_n \, \map \cos {\theta_n + 2 k_n \pi - \theta}
       | c =
}}
{{end-eqn}}
Because Cosine Function is Continuous:
:$\map \cos {\theta_n + 2 k_n \pi - \theta} \to 1$
It follows that:
:$\cmod {z_n - z}^2 \to 0$
Conversely, suppose $z_n \to z$.
By Modulus of Limit, $r_n \to r$.
We have, by Complex Modulus of Difference of Complex Numbers:
{{begin-eqn}}
{{eqn  | l = \map \cos {\theta_n - \theta}
       | r = \frac {r_n^2 + r^2 - \cmod {z_n - z}^2} {2 r r_n} \to 1
       | c =
}}
{{end-eqn}}
By Convergence of Cosine of Sequence, there exists a sequence $\sequence {k_n}$ of integers such that $\theta_n + 2 k_n \pi$ converges to $\theta$.
{{qed}}
Category:Complex Analysis
rr4ie42o8rulamqw9yn0tbeajutdxgj
Theorem: Complex Modulus of Sum of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\theta_1$ and $\theta_2$ be arguments of $z_1$ and $z_2$, respectively.
Then:
:$\cmod {z_1 + z_2}^2 = \cmod {z_1}^2 + \cmod {z_2}^2 + 2 \cmod {z_1} \cmod {z_2} \, \map \cos {\theta_1 - \theta_2}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 + z_2}^2
      | r = \paren {z_1 + z_2} \paren {\overline {z_1} + \overline {z_2} }
      | c = Modulus in Terms of Conjugate and Sum of Complex Conjugates
}}
{{eqn | r = z_1 \overline {z_1} + z_2 \overline {z_2} + z_1\overline {z_2} + \overline {z_1} z_2
      | c = 
}}
{{eqn | r = \cmod {z_1}^2 + \cmod {z_2}^2 + 2 \, \map \Re {z_1 \overline {z_2} }
      | c = Modulus in Terms of Conjugate and Sum of Complex Number with Conjugate
}}
{{eqn | r = \cmod {z_1}^2 + \cmod {z_2}^2 + 2 \, \cmod {z_1} \cmod {z_2} \map \cos {\theta_1 - \theta_2}
      | c = Product of Complex Numbers in Polar Form and Argument of Complex Conjugate equals Negative of Argument
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus of Sum of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\theta_1$ and $\theta_2$ be arguments of $z_1$ and $z_2$, respectively.
Then:
:$\cmod {z_1 + z_2}^2 = \cmod {z_1}^2 + \cmod {z_2}^2 + 2 \cmod {z_1} \cmod {z_2} \, \map \cos {\theta_1 - \theta_2}$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 + z_2}^2
      | r = \paren {\cmod {z_1} \cos \theta_1 + \cmod {z_2} \cos \theta_2}^2 + \paren {\cmod {z_1} \sin \theta_1 + \cmod {z_2} \sin \theta_2}^2
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = 2 \cmod {z_1} \cmod {z_2} \cos \theta_1 \cos \theta_2 + \cmod {z_1}^2 \cos^2 \theta_1 + \cmod {z_2}^2 \cos^2 \theta_2
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = 2 \cmod {z_1} \cmod {z_2} \sin \theta_1 \sin \theta_2 + \cmod {z_1}^2 \sin^2 \theta_1 + \cmod {z_2}^2 \sin^2 \theta_2
      | c = 
}}
{{eqn | r = 2 \cmod {z_1} \cmod {z_2} \paren {\cos \theta_1 \cos \theta_2 + \sin \theta_1 \sin \theta_2} + \cmod {z_1}^2 + \cmod {z_2}^2
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \cmod {z_1}^2 + \cmod {z_2}^2 + 2 \cmod {z_1} \cmod {z_2} \, \map \cos {\theta_1 - \theta_2}
      | c = Cosine of Difference
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus of Difference of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\theta_1$ and $\theta_2$ be arguments of $z_1$ and $z_2$, respectively.
Then:
:$\cmod {z_1 - z_2}^2 = \cmod {z_1}^2 + \cmod {z_2}^2 - 2 \cmod {z_1} \cmod {z_2} \map \cos {\theta_1 - \theta_2}$

Proof:
By Complex Argument of Additive Inverse, $\theta_2 + \pi$ is an argument of $-z_2$.
We have:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 - z_2}^2
      | r = \cmod {z_1}^2 + \cmod {-z_2}^2 + 2 \cmod {z_1} \cmod {-z_2} \map \cos {\theta_1 - \theta_2 - \pi}
      | c = Complex Modulus of Sum of Complex Numbers
}}
{{eqn | r = \cmod {z_1}^2 + \cmod {z_2}^2 - 2 \cmod {z_1} \cmod {z_2} \map \cos {\theta_1 - \theta_2}
      | c = Complex Modulus of Additive Inverse
}}
{{end-eqn}}
{{qed}}
Theorem: Uniform Absolute Convergence of Infinite Product of Complex Functions

Let $X$ be a compact metric space.
Let $\sequence {f_n}$ be a sequence of continuous functions $X \to \C$.
Let $\ds \sum_{n \mathop = 1}^\infty f_n$ converge uniformly absolutely on $X$.
Then:
:$\map f x = \ds \prod_{n \mathop = 1}^\infty \paren {1 + \map {f_n} x}$ converges uniformly absolutely on $X$
:$f$ is continuous
:there exists $n_0 \in \N$ such that $\ds \prod_{n \mathop = n_0}^\infty \paren {1 + \map {f_n} x}$ has no zeroes.

Proof:
=== Lemma ===
{{:Uniform Absolute Convergence of Infinite Product of Complex Functions/Lemma}}{{qed|lemma}}
Because $\ds \sum_{n \mathop = 1}^\infty f_n$ converges uniformly, there exists $n_0 > 0$ such that $\size {\map {f_n} x} < \dfrac 1 2$ for $n \ge n_0$ and $x \in X$.
Then:
:$\map \Re {1 + \map {f_n} x} > 0$
By Bounds for Complex Logarithm:
:$\size {\map \log {1 + \map {f_n} x} } \le \dfrac 3 2 \size {\map {f_n} x}$
:$\size {\map \log {1 + \size {\map {f_n} x} } } \le \dfrac 3 2 \size {\map {f_n} x}$
for $n \ge n_0$.
By Comparison Test for Uniformly Convergent Series:
:$g = \ds \sum_{n \mathop = n_0}^\infty \map \log {1 + f_n}$
and:
:$h = \ds \sum_{n \mathop = n_0}^\infty \map \log {1 + \size {f_n} }$
converge uniformly.
By Uniform Limit Theorem, $g$ and $h$ are continuous.
By Continuous Function on Compact Subspace of Euclidean Space is Bounded, $g$ and $h$ are bounded
By Exponential of Series Equals Infinite Product:
:$\map \exp g = \ds \prod_{n \mathop = n_0}^\infty \paren {1 + f_n}$
:$\map \exp h = \ds \prod_{n \mathop = n_0}^\infty \paren {1 + \size {f_n} }$
By the lemma, the products converge uniformly.
By Uniform Limit Theorem, $\map \exp g$ is continuous.
Because the second product converges uniformly, the first converges uniformly absolutely.
By Image of Complex Exponential Function, $\map \exp g$ has no zeroes.
{{qed}}
Category:Infinite Products
6u1mqutm4xxtzr475aakfrj9hmf1w6s
Theorem: Empty Intersection iff Subset of Relative Complement

Let $S$ be a set.
Let $A, B$ be subset of $S$.
Then $A \cap B = \O \iff A \subseteq \relcomp S B$

Proof:
:$A \cap B = \O$
{{iff}}
:$\forall x \in S: x \notin A \cap B$ by Empty Set as Subset
{{iff}}
:$\forall x \in S: \neg \paren {x \in A \land x \in B}$ by definition of intersection
{{iff}}
:$\forall x \in S: x \notin A \lor x \notin B$ by De Morgan's Laws (Logic)/Disjunction of Negations
{{iff}}
:$\forall x \in S: x \in A \implies x \notin B$ by Rule of Material Implication
{{iff}}
:$\forall x \in S: x \in A \implies x \in \relcomp S B$ by definition of relative complement
{{iff}}
:$A \subseteq \relcomp S B$ by Subset in Subsets.
{{qed}}
Theorem: Subset in Subsets

Let $S, B$ be sets.
Let $A$ be subset of $S$.
Then:
:$A \subseteq B \iff \forall x \in S: x \in A \implies x \in B$

Proof:
=== Sufficient Condition ===
Follows by definition of subset.