avewright/proofwiki-math huggingface dataset:
Theorem: Ray from Interior of Compact Convex Set Meets Boundary Exactly Once

Let $A \subseteq \R^n$ be a compact convex subspace of real Euclidean $n$-space.
Let $\bsx_0 \in A^\circ$ be an interior point of $A$.
Then, for every $\bsy \in \R^n \setminus \bszero$, there is a unique $t \in \R_{> 0}$ such that:
:$\bsx_0 + t \bsy \in \partial A$

Proof:
By Compact Subspace of Metric Space is Bounded:
:$A$ is bounded
Then, by Ray from Bounded Set Meets Boundary, there is some $t \in \R_{\ge 0}$ such that:
:$\bsx_0 + t \bsy \in \partial A$
But, if $t = 0$, then:
:$\bsx_0 \in \partial A$
contradicting the definition of boundary, since $\bsx_0 \in A^\circ$.
Thus, $t > 0$.
Now, suppose that $t' \in \R_{> 0}$ also satisfies:
:$\bsx_0 + t' \bsy \in \partial A$
{{WLOG}}, suppose $t' \le t$.
By definition of interior point, there is some $\epsilon > 0$ such that:
:$\map {B_\epsilon} {\bsx_0} \subseteq A$
Let $\epsilon' = \dfrac {t - t'} t \epsilon$.
{{AimForCont}} $t' < t$.
Then, $\epsilon' > 0$.
Let $\bsx' \in \map {B_{\epsilon'}} {\bsx_0 + t' \bsy}$ be arbitrary.
Define:
:$\bsx = \bsx_0 + \dfrac t {t - t'} \paren {\bsx' - \paren {\bsx_0 + t' \bsy}}$
We have:
{{begin-eqn}}
{{eqn | l = \norm {\bsx - \bsx_0}
      | r = \frac t {t - t'} \norm {\bsx' - \paren {\bsx_0 + t' \bsy} }
      | c = {{NormAxiomVector|2}}
}}
{{eqn | o = <
      | r = \frac t {t - t'} \epsilon'
      | $\bsx' \in \map {B_{\epsilon'} } {\bsx_0 + t' \bsy}$
}}
{{eqn | r = \frac t {t - t'} \frac {t - t'} t \epsilon
      | c = Definition of $\epsilon'$
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
Therefore:
:$\bsx \in \map {B_\epsilon} {\bsx_0} \subseteq A$
Finally:
{{begin-eqn}}
{{eqn | l = \frac {t - t'} t \bsx
      | r = \frac {t - t'} t \bsx_0 + \bsx' - \paren {\bsx_0 + t' \bsy}
}}
{{eqn | ll = \leadsto
      | l = \bsx'
      | r = \frac {t - t'} t \bsx - \frac {t - t'} t \bsx_0 + \bsx_0 + t' \bsy
}}
{{eqn | r = \frac {t - t'} t \bsx + \frac {t'} t \bsx_0 + t' \bsy
}}
{{eqn | r = \paren {1 - \frac {t'} t} \bsx + \frac {t'} t \paren {\bsx_0 + t \bsy}
}}
{{end-eqn}}
As $0 < t' < t$, it follows that:
:$0 < \dfrac {t'} t < 1$
Additionally, by Compact Subspace of Hausdorff Space is Closed:
:$\partial A \subseteq A$
Therefore:
:$\bsx_0 + t \bsy \in A$
So, by definition of convex:
:$\bsx' \in A$
As $\bsx' \in \map {B_{\epsilon'}} {\bsx_0 + t' \bsy}$ was arbitrary, it follows that:
:$\map {B_{\epsilon'}} {\bsx_0 + t' \bsy} \subseteq A$
Therefore, by definition:
:$\bsx_0 + t' \bsy \in A^\circ$
But we assumed that:
:$\bsx_0 + t' \bsy \in \partial A$
which is a contradiction.
Therefore, by Proof by Contradiction:
:$t' = t$
{{qed}}
Category:Convex Sets (Vector Spaces)
nkzylhv8rsbkiwbr68zy96qd4f7iswi
Theorem: Center of Mass of System of Particles in Cartesian Plane

Let $B$ be a system of $n$ discrete particles embedded in a cartesian plane, each with:
:mass $m_i$
:position $\tuple {x_i, y_i}$
where $i \in \set {1, 2, \ldots, n}$.
Then the coordinates $\tuple {\bar x, \bar y}$ of the center of mass of $B$ are given by:
{{begin-eqn}}
{{eqn | l = M \bar x
      | r = \sum_{i \mathop = 1}^n m_i x_i
}}
{{eqn | l = M \bar y
      | r = \sum_{i \mathop = 1}^n m_i y_i
}}
{{end-eqn}}
where:
:$\ds M = \sum_{i \mathop = 1}^n m_i$

Proof:
{{ProofWanted|straightforward but utterly tedious}}
Theorem: Center of Mass/Examples/Uniform Lamina

Let $\LL$ be a uniform lamina embedded in a cartesian plane in the shape of the area between the curve $\map f x$, the straight lines $x = a$ and $x = b$, and the $x$-axis.
Let the area of $\LL$ be $A$.
Then the coordinates $\tuple {\bar x, \bar y}$ of the center of mass of $B$ are given by:
{{begin-eqn}}
{{eqn | l = A \bar x
      | r = \int_a^b x y \rd x
}}
{{eqn | l = A \bar y
      | r = \dfrac 1 2 \int_a^b y^2 \rd y
}}
{{end-eqn}}

Proof:
{{ProofWanted|straightforward but I have other things I want to do}}
Theorem: Center of Gravity equals Center of Mass if it exists

Let $B$ be a body in a gravitational field $\mathbf G$.
Let $B$ have a center of gravity $P$.
Then the center of mass of $B$ is also $P$.

Proof:
Let $Q$ denote the center of mass of $B$
First suppose that $\mathbf G$ is uniform.
From Center of Gravity in Uniform Gravitational Field is Center of Mass:
:$P = Q$
{{qed|lemma}}
Now suppose that $\mathbf G$ is non-uniform.
There are two possibilities:
:$(1): \quad$ $B$ is barycentric
:$(2): \quad$ $B$ is not barycentric.
If $(1)$, then from Center of Gravity of Barycentric Body is Center of Mass:
:$P = Q$
If $(2)$, then from Center of Gravity in Non-Uniform Gravitational Field, the forces on $B$ induced by $\mathbf G$ consist of:
:a single force $\mathbf F$
:a couple $C$ whose plane is perpendicular to the line of action of $\mathbf F$.
The line of action of $\mathbf F$ does not necessarily pass through some fixed point as $B$ rotates in $\mathbf G$.
Hence $B$ has no center of gravity.
All cases are covered, and the result follows.
{{qed}}
Theorem: Centripetal Force on Body in Circular Path

Let $B$ be a body of mass $m$ constrained to move at constant speed $v$ in a circular path $C$ or radius $r$.
Let $\mathbf F$ denote the centripetal force on $B$.
Then:
:$(1): \quad$ The direction of $\mathbf F$ is towards the center of $C$
:$(2): \quad$ The magnitude of $\mathbf F$ is given by:
::::$\size {\mathbf F} = \dfrac {m v^2} r$
:::or:
::::$\size {\mathbf F} = m r \omega^2$
:::where $\omega$ denotes the angular speed of $B$.

Proof:
Let $\mathbf r$ be the position vector of $B$ {{WRT}} the center of $C$.
Let $\mathbf v$ be the velocity of $B$.
Let $\mathbf a$ be the acceleration of $B$.
We have:
{{begin-eqn}}
{{eqn | l = \mathbf F
      | r = m \mathbf a
      | c = Newton's Second Law
}}
{{eqn | r = m \paren {-\frac {\size {\mathbf v}^2 \mathbf r} {\size {\mathbf r}^2} }
      | c = Acceleration of Particle moving in Circle at Constant Speed
}}
{{eqn | r = -\paren {\frac {m \size {\mathbf v}^2} {\size {\mathbf r}^2} } \mathbf r
}}
{{end-eqn}}
Note that all quantities in the parentheses are positive numbers:
:$m$ is mass, which is always positive in Newtonian mechanics
:$\size {\mathbf v}$ and $\size {\mathbf r}$ are vector lengths, which are non-negative
The fact that $\mathbf r$ is being multiplied by a negative number means that the force vector points from $B$ to the center of $C$.
So, $(1)$ is true:
{{qed|lemma}}
Taking the magnitude of both sides gives:
{{begin-eqn}}
{{eqn | l = \size {\mathbf F}
      | r = \size {-\paren {\frac {m \size {\mathbf v}^2} {\size {\mathbf r}^2} } \mathbf r}
}}
{{eqn | r = \paren {\frac {m \size {\mathbf v}^2} {\size {\mathbf r}^2} } \size {\mathbf r}
}}
{{eqn | r = \frac {m \size {\mathbf v}^2} {\size {\mathbf r} }
}}
{{eqn | r = \frac {m v^2} r
      | c = $v = \size {\mathbf v}$ and $r = \size {\mathbf r}$
}}
{{end-eqn}}
{{qed|lemma}}
From the Angular Speed of Particle in Circular Motion at Constant Speed:
:$\omega = \dfrac v r$
Substituting into the equation for $\size {\mathbf F}$ results in:
{{begin-eqn}}
{{eqn | l = \size {\mathbf F}
      | r = \frac {m v^2} r
}}
{{eqn | r = \frac {m r v^2} {r^2}
      | c = Multiply by $\dfrac r r$
}}
{{eqn | r = m r \omega^2
}}
{{end-eqn}}
{{qed}}
Theorem: Center of Mass Operation is Associative

Let $S$ denote the set of massy particles in ordinary space.
Let $\circ$ denote the binary operation defined as:
:$\forall x, y \in S: x \circ y =$ the center of mass of $x$ and $y$
Then $\circ$ is an associative operation.

Proof:
{{ProofWanted|Apparently it's equivalent to Ceva's Theorem.}}
Theorem: Maximal Ergodic Theorem

Let $\struct {X, \BB, \mu, T}$ be a measure-preserving dynamical system.
Let $g : X \to \overline \R$ be a $\mu$-integrable function.
Let $\alpha \in \R$.
Let:
:$\ds E_\alpha := \set {x \in X : \sup_{n \ge 1} \frac 1 n \sum_{i \mathop = 0}^{n-1} \map g {T^i x} > \alpha }$
Then:
:$\ds \alpha \map \mu {E_\alpha} \le \int_{E_\alpha} g \rd \mu$

Proof:
Let $\map {L^1} \mu$ be a real-valued $L^1$ space with respect to $\mu$.
Consider $U_T : \map {L^1} \mu \to \map {L^1} \mu$ defined by:
:$f \mapsto f \circ T$
Observe:
{{begin-eqn}}
{{eqn | l = E_\alpha
      | r = \bigcup_{N \mathop =1}^\infty F_N
}}
{{end-eqn}}
where:
:$\ds F_N := \set {\max_{1 \le n \le N} \sum_{i \mathop = 0}^{n-1} \map {U_T^i} {g - \alpha} > 0 }$
Moreover, $F_N \subseteq F_{N+1}$ for all $N$.
Thus:
{{begin-eqn}}
{{eqn | l = \int_{E_\alpha} \paren {g - \alpha} \rd \mu
      | r = \lim_{N \mathop \to \infty} \int_{F_N} \paren {g - \alpha}\rd \mu
      | c = Lebesgue's Dominated Convergence Theorem
}}
{{eqn | o = \ge
      | r = 0
      | c = Maximal Inequality for Positive Operators
}}
{{end-eqn}}
{{finish|Details}}
Theorem: Join of Compact Spaces is Compact

Let $A, B$ be compact topological spaces.
Then:
:$A \ast B$ is compact
where $A \ast B$ denotes the join of $A$ and $B$.

Proof:
By Closed Real Interval is Compact Space:
:$\closedint 0 1$
is compact.
Thus, by Topological Product of Compact Spaces:
:$A \times B \times \closedint 0 1$
is compact.
Therefore, by Quotient Space of Compact Space is Compact:
:$A \ast B = \paren {A \times B \times \closedint 0 1} / \RR$
is compact.
{{qed}}
Category:Compact Topological Spaces
Category:Quotient Spaces (Topology)
64jc0vtd1kaq34lw5jdlr2qzv9b83mi
Theorem: Characteristic Function of Normal Distribution/Corollary

The characteristic function of the standard normal distribution is:
:$\map \phi t = e^{-\frac 1 2 t^2}$

Proof:
Recall Characteristic Function of Normal Distribution:
{{:Characteristic Function of Normal Distribution}}
The standard normal distribution is the normal distribution with $\mu = 0$ and $\sigma = 1$.
Hence:
{{begin-eqn}}
{{eqn | l = \map \phi t
      | r = e^{i t \times 0 - \frac 1 2 t^2 \times 1^2}
      | c = 
}}
{{eqn | r = e^{0 - \frac 1 2 t^2}
      | c = 
}}
{{eqn | r = e^{-\frac 1 2 t^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Median of Logistic Distribution

Let $X$ be a continuous random variable with a '''logistic distribution''':
:$\map {f_X} x = \dfrac {\map \exp {-\dfrac {\paren {x - \mu} } s} } {s \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^2}$
for $\mu \in \R, s \in \R_{>0}$.
The median of $X$ is $\mu$.

Proof:
From the definition of the logistic distribution, $X$ has probability density function:
:$\map {f_X} x = \dfrac {\map \exp {-\dfrac {\paren {x - \mu} } s} } {s \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^2}$
Note that $f_X$ is non-zero, sufficient to ensure a unique median.
{{explain|Why does being non-zero ensure a unique median? This needs a page of its own, as it's used elsewhere as well.}}
By the definition of a median, to prove that $\mu$ is the median of $X$ we must verify: 
:$\ds \map \Pr {X < \mu} = \int_{-\infty}^\mu \map {f_X} x \rd x = \frac 1 2$
We have:
{{begin-eqn}}
{{eqn | l = \int_{-\infty}^\mu \map {f_X} x \rd x
      | r = \frac 1 s  \int_{-\infty}^\mu \dfrac {\map \exp {-\dfrac {\paren {x - \mu} } s} } {\paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^2} \rd x
}}
{{end-eqn}}
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-1}
      | c = Integration by Substitution
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = -\paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-2} \paren {-\frac 1 s \map \exp {-\dfrac {\paren {x - \mu} } s} }
      | c = Power Rule for Derivatives, Chain Rule for Derivatives and {{Corollary|Derivative of Exponential Function|1}}
}}
{{end-eqn}}
and also:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to -\infty} \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-1}
      | r = 0
      | c = 
}}
{{eqn | l = \lim_{x \mathop \to \mu} \paren {1 + \map \exp {-\dfrac {\paren {x - \mu} } s} }^{-1}
      | r = \dfrac 1 2
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | r = \int_0^{\frac 1 2} \rd u
      | c = 
}}
{{eqn | r = \bigintlimits u 0 {\frac 1 2}
      | c = Integral of Constant
}}
{{eqn | r = \frac 1 2
}}
{{end-eqn}}
{{qed}}
Category:Logistic Distribution
Category:Medians
gdwe2a18lnf9qlfyrj1bj4itdlepydj
Theorem: Expansion of Characteristic Polynomial of Matrix

Let $R$ be a commutative ring with unity.
Let $R \sqbrk x$ be the polynomial ring in one variable over $R$.
Let $\mathbf A$ be a square matrix over $R$ of order $n > 0$.
Let $\map {p_{\mathbf A} } x$ be the characteristic polynomial of $\mathbf A$.
Then $\map {p_{\mathbf A} } x$ can be expressed as:
:$\map {p_{\mathbf A} } x = x^n + a_{n - 1} x^{n - 1} + \cdots + a_0$
where:
{{begin-eqn}}
{{eqn | l = a_{n - 1}
      | r = -\map \tr {\mathbf A}
      | c = where $\map \tr {\mathbf A}$ denotes the trace of $\mathbf A$
}}
{{eqn | l = a_0
      | r = \paren {-1}^n \map \det {\mathbf A}
      | c = where $\map \det {\mathbf A}$ denotes the determinant of $\mathbf A$
}}
{{end-eqn}}

Proof:
We have that the eigenvalues of $\mathbf A$ are the roots of $\map {p_{\mathbf A} } x$.
From Sum of Roots of Polynomial, the sum of the roots of $\map {p_{\mathbf A} } x$ is $-\dfrac {a_{n - 1} } {a_n}$
From Characteristic Polynomial of Matrix is Monic, $a_n = 1$.
Thus, from Trace of Matrix is Sum of Eigenvalues:
:$-a_{n - 1} = \map \tr {\mathbf A}$
or
:$a_{n - 1} = -\map \tr {\mathbf A}$
{{qed|lemma}}
From Product of Roots of Polynomial, the product of the roots of $\map {p_{\mathbf A} } x$ is $\dfrac {\paren {-1}^n a_0} {a_n}$.
From Characteristic Polynomial of Matrix is Monic, $a_n = 1$.
From Determinant Equals Product of Eigenvalues:
:$\map \det {\mathbf A} = \paren {-1}^n a_0$
or
:$a_0 = \paren {-1}^n \map \det {\mathbf A}$
{{qed}}
Theorem: Chinese Remainder Theorem/Construction of Solution

Recall the Chinese Remainder Theorem:
{{:Chinese Remainder Theorem}}

Proof:
First we demonstrate that $x$ is a solution.
By construction:
{{begin-eqn}}
{{eqn | q = \forall j \in \set {1, 2, \ldots, r}
      | l = n_j
      | o = \divides
      | r = y_i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_i
      | o = \equiv
      | r = 0
      | rr= \pmod {n_i}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = b_i y_i z_i
      | o = \equiv
      | r = 0
      | rr= \pmod {n_i}
      | c = 
}}
{{end-eqn}}
For each $i \in \set {1, 2, \ldots, r}$, we have:
{{begin-eqn}}
{{eqn | l = x
      | o = \equiv
      | r = \sum_{i \mathop = 1}^r b_i y_i z_i
      | rr= \pmod {n_i}
      | c =
}}
{{eqn | o = \equiv
      | r = b_i y_i z_i
      | rr= \pmod {n_i}
      | c = from $(1)$: all terms vanish except for one
}}
{{eqn | o = \equiv
      | r = b_i
      | rr= \pmod {n_i}
      | c = as $y_i z_i \equiv 1$
}}
{{end-eqn}}
Hence:
:$\forall i \in \set {1, 2, \ldots, r}: x \equiv b_i \pmod {n_i}$
Thus $x$ is a solution as required.
{{qed|lemma}}
Now we demonstrate uniqueness up to congruence modulo $N$:
Now suppose there exist $u, v \in \Z$ which are both solutions.
Then:
{{begin-eqn}}
{{eqn | q = \forall j \in \set {1, 2, \ldots, r}
      | l = u
      | o = \equiv
      | r = b_i
      | rr= \pmod {n_i}
      | c = 
}}
{{eqn | l = v
      | o = \equiv
      | r = b_i
      | rr= \pmod {n_i}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u - v
      | o = \equiv
      | r = b_i
      | rr= \pmod {n_i}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall j \in \set {1, 2, \ldots, r}
      | l = n_1
      | o = \divides
      | r = u - v
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \prod_{i \mathop = 1}^r n_i
      | o = \divides
      | r = u - v
      | c = as $n_1, n_2, \ldots, n_r$ are pairwise coprime
}}
{{eqn | ll= \leadsto
      | l = u
      | o = \equiv
      | r = v
      | rr= \pmod {\prod_{i \mathop = 1}^r n_i}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u
      | o = \equiv
      | r = v
      | rr= \pmod N
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Chinese Remainder Theorem
612cz3ix0tupdxztrd94i9e3ulnz7rh
Theorem: Maximal Radical implies Primary Ideal

Let $R$ be a commutative ring with unity.
Let $\mathfrak a$ be an ideal of $R$.
Let $\map \Rad {\mathfrak a}$ be the radical of $\mathfrak a$.
Suppose that $\map \Rad {\mathfrak a}$ is a maximal ideal.
Then $\mathfrak a$ is a primary ideal.

Proof:
Consider the quotient ring $R / \mathfrak a$.
By {{Defof|Nilradical of Ring|index=1}} and {{Defof|Radical of Ideal of Ring|index=1}}:
:$\Nil {R / \mathfrak a} = \map \Rad {\mathfrak a} / \mathfrak a$
On the other hand, {{hypothesis}}, $\map \Rad {\mathfrak a} / \mathfrak a$ is a maximal ideal of $R / \mathfrak a$.
Thus, in view of {{Defof|Nilradical of Ring|index=1}}:
:$\Nil {R / \mathfrak a}$
is the only maximal ring in $R / \mathfrak a$.
In view of Proper Ideal of Ring is Contained in Maximal Ideal, {{Defof|Primary Ideal|index=2}} follows.
{{finish|More details}}
Category:Radical of Ideals
Category:Primary Ideals
Category:Prime Ideals of Rings
2429a0dq0gbyu9o1y3oez5x60c2lvin
Theorem: Positive Definite Matrix has Cholesky Factorization

Let $\mathbf A$ be a positive definite matrix.
Then there exists a Cholesky factorization of $\mathbf A$.

Proof:
{{tidy}}
{{Proofread}}
From the Spectral Theorem for Real Symmetric Matrices, there exists an orthogonal matrix $\Omega$ such that $\Omega^T \mathbf A \Omega$ is diagonal.
Let $\Omega^T \mathbf A \Omega = \map {\mathrm {diag} } {\lambda_1, \ldots, \lambda_n}$
Then, $\lambda_1, \cdots, \lambda_n$ are eigenvalues of $\mathbf A$, so they are positive because $\mathbf A$ is positive definite
{{explain|Why are they eigenvalues?}}
Let $\mathbf B = \map {\mathrm {diag} } {\sqrt {\lambda_1}, \ldots, \sqrt {\lambda_n} } \times \Omega^T$
Observe that $\mathbf A = \mathbf B^T \mathbf B$
By QR factorization, we can write:
:$\mathbf B = \mathbf Q \mathbf R$
where :
:$\mathbf Q$ is orthogonal
:$\mathbf R$ is upper triangular
Then, $\mathbf A = \mathbf B ^T \mathbf B = \mathbf R^T \mathbf Q^T \mathbf Q \mathbf R$
Because $\mathbf Q^T \mathbf Q = I_n$, we have $\mathbf A = \mathbf R^T \mathbf R$
{{qed}}
Theorem: Ring of Continuous Mappings is Subring of All Mappings

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\struct {R, +, *, \tau_{_R} }$ be a topological ring.
Let $\struct {R^S, +, *}$ be the ring of mappings from $S$ to $R$.
Let $\struct{\map C {S, R}, +, *}$ be the ring of continuous mappings from $S$ to $R$.
Then:
:$\struct{\map C {S, R}, +, *}$ is a subring of $\struct {R^S, +, *}$

Proof:
From Structure Induced by Ring Operations is Ring:
:$\struct {R^S, +, *}$ is a ring.
From Structure Induced by Ring Operations is Ring:
:$\forall f \in R^S :$ the additive inverse of $f$ is the pointwise negation $-f$, defined by:
::$\forall s \in S: \map {\paren {-f} } s := - \map f s$
From the Subring Test:
:$\struct{\map C {S, R}, +, *}$ is a subring of $\struct {R^S, +, *}$
{{iff}}
:$(1) \quad \map C {S, R} \ne \O$
:$(2) \quad \forall f, g \in \map C {S, R} : f + \paren{-g} \in  \map C {S, R}$
:$(3) \quad \forall f, g \in \map C {S, R} : f * g \in  \map C {S, R}$
Theorem: Zero of Ring of Continuous Mappings

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\struct {R, +, *, \tau_{_R} }$ be a topological ring with zero $0_R$.
Let $\struct{\map C {S, R}, +, *}$ be the ring of continuous mappings from $S$ to $R$.
Then:
:the zero of $\struct{\map C {S, R}, +, *}$ is the constant mapping $0_{R^S} : S \to R$ defined by:
::$\forall s \in S : \map {0_{R^S}} s = 0_R$

Proof:
Let $\struct {R^S, +, *}$ be the ring of mappings from $S$ to $R$.
From Ring of Continuous Mappings is Subring of All Mappings:
:$\struct{\map C {S, R}, +, *}$ is a subring of $\struct {R^S, +, *}$
From Induced Structure Identity:
:the zero of $\struct {R^S, +, *}$ is the constant mapping $0_{R^S} : S \to R$ defined by:
::$\forall s \in S : \map {0_{R^S}} s = 0_R$
From Zero of Subring is Zero of Ring:
:$0_{R^S} \in \map C {S, R}$
{{qed}}
Theorem: Church's Theorem

There exists no effective procedure for determining whether or not a given well-formed formula of the predicate calculus is a theorem.
That is, the decision problem for the predicate calculus is undecidable.

Proof:
{{ProofWanted}}
{{Namedfor|Alonzo Church|cat = Church}}
Theorem: Unity of Ring of Continuous Mappings

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\struct {R, +, *, \tau_{_R} }$ be a topological ring with unity $1_R$.
Let $\struct{\map C {S, R}, +, *}$ be the ring of continuous mappings from $S$ to $R$.
Then:
:the unity of $\struct{\map C {S, R}, +, *}$ is the constant mapping $1_{R^S} : S \to R$ defined by:
::$\forall s \in S : \map {1_{R^S}} s = 1_R$.

Proof:
Let $\struct {R^S, +, *}$ be the ring of mappings from $S$ to $R$.
From Ring of Continuous Mappings is Subring of All Mappings:
:$\struct{\map C {S, R}, +, *}$ is a subring of $\struct {R^S, +, *}$
From Induced Structure Identity:
:the unity of $\struct {R^S, +, *}$ is the constant mapping $1_{R^S} : S \to R$ defined by:
::$\forall s \in S : \map {1_{R^S}} s = 1_R$
From Constant Mapping is Continuous:
:$1_{R^S} \in \map C {S, R}$
From Subring Containing Ring Unity has Unity:
:$1_{R^S}$ is the unity of $\map C {S, R}$
{{qed}}
Theorem: Commutativity of Ring of Continuous Mappings

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\struct {R, +, *, \tau_{_R} }$ be a commutative topological ring.
Let $\struct{\map C {S, R}, +, *}$ be the ring of continuous mappings from $S$ to $R$.
Then:
:$\struct{\map C {S, R}, +, *}$ is a commutative ring

Proof:
From Structure Induced by Commutative Operation is Commutative:
:the ring of mappings $\struct{R^S, +, *}$ is commutative
From Ring of Continuous Mappings is Subring of All Mappings:
:$\struct{\map C {S, R}, +, *}$ is a subring of $\struct{R^S, +, *}$
From Subring of Commutative Ring is Commutative:
:$\struct{\map C {S, R}, +, *}$ is commutative
{{qed}}
Theorem: Tangents to Circle from Point are of Equal Length

Let $\CC$ be a circle.
Let $P$ be a point in the exterior of $\CC$.
Let $PA$ and $PB$ be tangents to $\CC$ from $P$ touching $\CC$ at $A$ and $B$ respectively.
:400px
Then:
:$PA = PB$

Proof:
Let $O$ be the center of $\CC$.
Construct $OA$ and $OB$.
From Radius at Right Angle to Tangent:
:$PA \perp OA$ and $PB \perp OB$
and so $\angle OAP = \angle OBP$ which equals a right angle.
:400px
Consider the right triangles $\triangle OAP$ and $\triangle OBP$.
We have:
:$OA = OB$ by definition of radius of circle
:$\angle OAP = \angle OBP$
:$OP$ is their common hypotenuse.
Hence by Triangle Right-Angle-Hypotenuse-Side Congruence:
:$\triangle OAP \cong \triangle OBP$
and so $PA = PB$.
{{qed}}
Theorem: Tangents to Circle from Point subtend Equal Angles at Center

Let $\CC$ be a circle.
Let $P$ be a point in the exterior of $\CC$.
Let $PA$ and $PB$ be tangents to $\CC$ from $P$ touching $\CC$ at $A$ and $B$ respectively.
:400px
Then:
:$\angle OPA = \angle OPB$

Proof:
Let $O$ be the center of $\CC$.
Construct $OA$ and $OB$.
From Radius at Right Angle to Tangent:
:$PA \perp OA$ and $PB \perp OB$
and so $\angle OAP = \angle OBP$ which equals a right angle.
:400px
Consider the right triangles $\triangle OAP$ and $\triangle OBP$.
We have:
:$OA = OB$ by definition of radius of circle
:$\angle OAP = \angle OBP$
:$OP$ is their common hypotenuse.
Hence by Triangle Right-Angle-Hypotenuse-Side Congruence:
:$\triangle OAP \cong \triangle OBP$
and so $OPA = \angle OPB$.
{{qed}}
Theorem: Tangents to Circle from Point subtend Equal Angles at Center/Corollary

Let $\CC$ be a circle.
Let $P$ be a point in the exterior of $\CC$.
Let $PA$ and $PB$ be tangents to $\CC$ from $P$ touching $\CC$ at $A$ and $B$ respectively.
:400px
Then $OP$ is a bisector of $\angle APB$.

Proof:
From Tangents to Circle from Point subtend Equal Angles at Center:
:$\angle OPA = \angle OPB$
from which follows the result.
{{qed}}
Theorem: Order of Convergence Implies Convergence

Let $\sequence {x_n}$ be an real sequence that converges to $\alpha$ with order $p$, where $p \ge 1$.
Then, $\sequence {x_n}$ converges to $\alpha$.

Proof:
By definition of order of convergence, there exist a sequence $\sequence {\epsilon_n}$ and $c > 0$ such that:
:$\size {x_n - \alpha} \le \epsilon_n$
:$\ds \lim_{n \to \infty} \frac {\epsilon_{n + 1}} {\epsilon_n^p} = c$
:$p = 1 \implies c < 1$
Theorem: Equation of Circular Helix/Parametric Form

Let $\HH$ be a '''circular helix''' embedded in Cartesian $3$-space whose axis coincides with the $z$-axis.
$\HH$ can be described by the parametric equation:
:<nowiki>$\begin {cases}
x & = a \cos t \\
y & = a \sin t \\
z & = b t \\
\end {cases}$</nowiki>
where $t$ is the parameter.

Proof:
{{ProofWanted|It needs to be proved that the tangent to $\HH$ is at a constant angle to the $z$-axis}}