avewright/proofwiki-math huggingface dataset:
Theorem: Mass of Mole of Isotope of Element

Let $S$ be a substance made up entirely of a particular isotope $Q$ of a particular element.
Let one atom of $Q$ contain $n$ neutrons and $p$ protons.
Then one mole of $S$ has a mass of approximately $n + p$ grams.

Proof:
Let $m_Q$ grams be the mass of one atom of $Q$.
Let $m_C$ grams be the mass of one atom of carbon-12.
Let $M_Q$ grams be the mass of one mole of $Q$.
Let $M_C$ grams be the mass of one mole of carbon-12.
The mass of a proton and the mass of a neutron are approximately equal.
Together, the protons and neutrons make up the vast majority of the mass of the atom they compose.
Hence the mass of one atom is proportional to the total number of its protons and neutrons.
There are $6$ protons and $6$ neutrons in one atom of carbon-12.
Thus we have:
{{begin-eqn}}
{{eqn | l = m_Q : m_C
      | r = \paren {n + p} : {6 + 6}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {m_Q} {m_C}
      | r = \dfrac {n + p} {12}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {M_Q} {M_C}
      | r = \dfrac {n + p} {12}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = M_Q
      | r = \paren {n + p} \dfrac {M_C} {12}
      | c = 
}}
{{end-eqn}}
Before $2018$, the '''mole''' was defined as the number of atoms in $12$ grams of carbon-12.
While the '''mole''' is no longer so defined, the mass of $1$ mole of carbon-12 is still $12$ grams, for all practical purposes.
Thus we have:
{{begin-eqn}}
{{eqn | l = M_C
      | r = 12 \ \mathrm g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = M_Q
      | r = \paren {n + p} \dfrac {12 \ \mathrm g} {12}
      | c = substituting for $M_C$ in $(1)$
}}
{{eqn | ll= \leadsto
      | l = M_Q
      | r = \paren {n + p} \ \mathrm g
      | c = 
}}
{{end-eqn}}
{{Qed}}
Category:Substance
jkn10vsar0mwnsposvr5qu8eqcvqmd3
Theorem: Mass of Mole of Substance

Let $S$ be a substance with molecular weight $W_S$.
Then one mole of $S$ has a mass of $W_S$ grams.

Proof:
Let $m_S$ grams be the mean mass of one molecule of $S$.
Let $m_C$ grams be the mass of one atom of carbon-12.
Let $M_S$ grams be the mass of one mole of $S$.
Let $M_C$ grams be the mass of one mole of carbon-12.
Then:
{{begin-eqn}}
{{eqn | l = W_S
      | r = m_S \times \dfrac {12} {m_C}
      | c = {{Defof|Molecular Weight}}
}}
{{eqn | r = M_S \times \dfrac {12} {M_C}
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = M_S
      | r = W_S \times \dfrac {M_C} {12}
      | c = 
}}
{{end-eqn}}
Before $2018$, the '''mole''' was defined as the number of atoms in $12$ grams of carbon-12.
While the '''mole''' is no longer so defined, the mass of $1$ mole of carbon-12 is still $12$ grams, for all practical purposes.
Thus we have:
{{begin-eqn}}
{{eqn | l = M_C
      | r = 12 \ \mathrm g
      | c = 
}}
{{eqn | ll= \leadsto
      | l = M_S
      | r = W_S \dfrac {12 \ \mathrm g} {12}
      | c = substituting for $M_C$ in $(1)$
}}
{{eqn | ll= \leadsto
      | l = M_S
      | r = W_S \ \mathrm g
      | c = 
}}
{{end-eqn}}
{{Qed}}
Category:Substance
nla3didvr4mnna01sqhxbidf7w4wg85
Theorem: Linear Second Order ODE/y'' = y'

The second order ODE:
:$(1): \quad y'' = y'$
has the general solution:
:$y = A_1 e^x + A_2$

Proof:
The proof proceeds by using Solution of Second Order Differential Equation with Missing Dependent Variable.
Substitute $p$ for $y'$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \dfrac {\d p} {\d x}
      | r = p
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = \int \rd x
      | r = \int \frac {\d p} p
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \ln p + C
      | c = Primitive of $\dfrac 1 x$
}}
{{eqn | ll= \leadsto
      | l = p = \frac {\d y} {\d x}
      | r = A_1 e^x
      | c = where $A_1 = e^C$
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = \int A_1 e^x \rd x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = y
      | r = A_1 e^x + A_2
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
{{qed}}
Theorem: Linear Second Order ODE/y'' = y'

The second order ODE:
:$(1): \quad y'' = y'$
has the general solution:
:$y = A_1 e^x + A_2$

Proof:
Using Solution of Second Order Differential Equation with Missing Independent Variable, $(1)$ can be expressed as:
{{begin-eqn}}
{{eqn | l = p \frac {\d p} {\d y}
      | r = p
      | c = where $p = \dfrac {\d y} {\d x}$
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = \int \frac {p \rd p} p
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \int \rd y
      | r = \int \rd p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = p + A_2
      | c = Primitive of Constant
}}
{{eqn | ll= \leadsto
      | l = p = \frac {\d y} {\d x}
      | r = y - A_2
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \frac {\d y} {\d x} - y
      | r = -A_2
      | c = 
}}
{{end-eqn}}
$(1)$ is a linear first order ODE in the form:
:$\dfrac {\d y} {\d x} + \map P x y = \map Q x$
where:
:$\map P x = -1$
:$\map Q x = -A_2$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map P x \rd x
      | r = -\int \rd x
      | c = 
}}
{{eqn | r = -x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e^{\int P \rd x}
      | r = e^{-x}
      | c = 
}}
{{end-eqn}}
Thus from Solution by Integrating Factor, $(1)$ can be rewritten as:
{{begin-eqn}}
{{eqn | l = \map {\dfrac {\d} {\d x} } {y e^{-x} }
      | r = -A_2 e^{-x}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y e^{-x}
      | r = -A_2 \int e^ \rd x
      | c = 
}}
{{eqn | r = A_2 e^{-x} + A_1
      | c = Primitive of Exponential Function
}}
{{eqn | r = -e^{-x} \paren {x^2 + 2 x + 2} + C
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = A_1 e^x + A_2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: First Order ODE/x y' = 2 y

The first order ODE:
:$x y' = 2 y$
has the general solution:
:$y = C x^2$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = x y'
      | r = 2 y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \int \dfrac {\d y} y
      | r = 2 \int \dfrac {\d x} x
      | c = Solution to Separable Differential Equation
}}
{{eqn | ll= \leadsto
      | l = \ln y
      | r = 2 \ln x + \ln C
      | c = Primitive of Reciprocal
}}
{{eqn | ll= \leadsto
      | l = \ln y
      | r = \map \ln C x^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = C x^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Singleton in Normed Vector Space is Closed

Let $X$ be a vector space over $\R$ or $\C$.
Let $\struct {X, \norm {\, \cdot \,}}$ be a normed vector space.
Let $\set x \subseteq X$ be a singleton.
Then $\set x$ is closed.

Proof:
Note that either $\set x = X$ or $\set x \subset X$.
Suppose, $X = \set x$.
Then:
:$X \setminus \set x = \O$
We have that Empty Set is Open in Normed Vector Space.
$\set x$ is a complement of $\O$ in $X$.
By definition, $x$ is closed.
Suppose, $X \ne \set x$, i.e. $\set x \subset X$.
Define $U := X \setminus \set x$.
Let $y \in U$.
Let $\epsilon := \norm {x - y}$.
Suppose, $\epsilon > 0$.
By Normed Vector Space is Open in Itself:
:$\forall x \in X : \exists \epsilon \in \R_{>0} : \map {B_\epsilon} x \subseteq X$
Suppose, $z \in \map {B_\epsilon} y$.
Then:
:$\norm {y - z} < \epsilon$.
We have that:
{{begin-eqn}}
{{eqn | l = \norm {z - x}
      | o = \ge
      | r = \norm {x - y} - \norm {y - z}
      | c = {{NormAxiomVector|3}}
}}
{{eqn | o = \ge
      | r = \epsilon - \norm {y - z}
}}
{{eqn | o = >
      | r = \epsilon - \epsilon
}}
{{eqn | r = 0}} 
{{end-eqn}}
Hence, $z \ne x$.
Then $z$ is in the complement of $\set x$ in $X$, i.e. $z \in U$.
In other words:
:$\forall y \in U : \exists \epsilon = \norm {x - y} > 0 : \map {B_\epsilon} x \subseteq U$
So $U$ is open, and $\set x = X \setminus U$ is closed. 
{{qed}}
Theorem: Singleton Set is Nowhere Dense in Rational Space

Let $\struct {\Q, \tau_d}$ be the rational number space under the Euclidean topology $\tau_d$.
Then every singleton subset of $\Q$ is nowhere dense in $\struct {\Q, \tau_d}$.

Proof:
Let $x \in \Q$.
By definition of nowhere dense, we need to show that:
:$\paren {\set x^-}^\circ = \O$
where $S^-$ denotes the closure of a set $S$ and $S^\circ$ denotes its interior.
By Real Number is Closed in Real Number Line, $\set x$ is closed in $\struct {\R, \tau_d}$.
$\struct {\Q, \tau_d}$ is a subspace of $\struct {\R, \tau_d}$.
Thus by Closed Set in Topological Subspace, $\set x$ is closed in $\struct {\Q, \tau_d}$.
From Closed Set Equals its Closure, it follows that:
:$\set x^- = \set x$
From Interior of Singleton in Real Number Line is Empty:
:$\set x^\circ = \O$
Hence:
:$\paren {\set x^-}^\circ = \set x^\circ = \O$
{{qed}}
Category:Rational Number Space
Category:Singletons
Category:Examples of Nowhere Dense
20hlcqfjw7j75jwgzk8ycojt3jj773r
Theorem: Real Function of Two Variables represents Surface in Cartesian 3-Space

Let $S$ and $T$ be subsets of the set of real numbers $\R$.
Let $f: S \times T \to \R$ be a real function of two variables.
Then the locus of $f$ describes a surface embedded in the Cartesian space $\R^3$.

Proof:
{{ProofWanted|The book says "clearly represents", but there is a concern that $f$ may need to be defined as continuous. And while it's intuitively obvious, it may not be so easy to prove rigorously.}}
Theorem: Finite Subset of Normed Vector Space is Closed

Let $M = \struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Let $F \subseteq X$ be finite.
Then $F$ is closed in $M$.

Proof:
Suppose $F$ is empty.
By Empty Set is Closed in Normed Vector Space, $F$ is closed.
Suppose, for some $n \in \N$, that:
:$\ds F = \bigcup_{i \mathop = 1}^n \set {x_i}$
We have that Singleton in Normed Vector Space is Closed.
Hence $F$ is a finite union of closed sets.
By Finite Union of Closed Sets is Closed in Normed Vector Space, $F$ is closed.
{{qed}}
Theorem: Finite Union of Closed Sets is Closed/Normed Vector Space

Let $M = \struct {X, \norm {\, \cdot \,} }$ be a normed vector space.
Then the union of finitely many closed sets of $M$ is itself closed.

Proof:
Let $\ds \bigcup_{i \mathop = 1}^n F_i$ be the union of a finite number of closed sets of $M$.
By definition of closed set, each of the $X \setminus F_i$ is by definition open in $M$.
Then from De Morgan's laws:
:$\ds X \setminus \bigcup_{i \mathop = 1}^n F_i = \bigcap_{i \mathop = 1}^n \paren {X \setminus F_i}$
We have that $\ds \bigcap_{i \mathop = 1}^n \paren {X \setminus F_i}$ is the intersection of a finite number of open sets of $M$.
By Finite Intersection of Open Sets of Normed Vector Space is Open, $\ds \bigcap_{i \mathop = 1}^n \paren {X \setminus F_i} = X \setminus \bigcup_{i \mathop = 1}^n F_i$ is likewise open in $M$.
Then by definition of closed set, $\ds \bigcup_{i \mathop = 1}^n F_i$ is closed in $M$.
{{qed}}
Theorem: Primitive of x fourth by Cosine of a x

:$\ds \int x^4 \cos a x \rd x = \frac {\sin a x} a x^4 + \frac {4 \cos a x} {a^2} x^3 - \frac {12 \sin a x} {a^3} x^2 - \frac {24 \cos a x} {a^4} x + \frac {24 \sin a x} {a^5} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int x^4 \cos a x \rd x
      | r = \frac {\sin a x} a x^4 + \frac {4 \cos a x} {a^2} x^{4 - 1} - \frac {4 \paren {4 - 1} } {a^2} \int x^{4 - 2} \cos a x \rd x + C
      | c = Primitive of $x^n \cos a x$
}}
{{eqn | r = \frac {\sin a x} a x^4 + \frac {4 \cos a x} {a^2} x^3 - \frac {12} {a^2} \int x^2 \cos a x \rd x + C
      | c = Simplifying
}}
{{eqn | r = \frac {\sin a x} a x^4 + \frac {4 \cos a x} {a^2} x^3 - \frac {12} {a^2} \paren {\frac {2 x \cos a x} {a^2} + \paren {\frac {x^2} a - \frac 2 {a^3} } \sin a x} + C
      | c = Primitive of $x^2 \cos a x$
}}
{{eqn | r = \frac {\sin a x} a x^4 + \frac {4 \cos a x} {a^2} x^3 - \frac {12 \sin a x} {a^3} x^2 - \frac {24 \cos a x} {a^4} x + \frac {24 \sin a x} {a^5} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of x sixth by Cosine of a x

:$\ds \int x^6 \cos a x \rd x = \frac {\sin a x} a x^6 + \frac {6 \cos a x} {a^2} x^5 - \frac {30 \sin a x} {a^3} x^4 - \frac {120 \cos a x} {a^4} x^3 + \frac {360 \sin a x} {a^5} x^2 + \frac {720 \cos a x} {a^6} x - \frac {720 \sin a x} {a^7} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int x^6 \cos a x \rd x
      | r = \frac {\sin a x} a x^6 + \frac {6 \cos a x} {a^2} x^{6 - 1} - \frac {6 \paren {6 - 1} } {a^2} \int x^{6 - 2} \cos a x \rd x + C
      | c = Primitive of $x^n \cos a x$
}}
{{eqn | r = \frac {\sin a x} a x^6 + \frac {6 \cos a x} {a^2} x^5 - \frac {30} {a^2} \int x^4 \cos a x \rd x + C
      | c = Simplifying
}}
{{eqn | r = \frac {\sin a x} a x^6 + \frac {6 \cos a x} {a^2} x^5 - \frac {30} {a^2} \paren {\frac {\sin a x} a x^4 + \frac {4 \cos a x} {a^2} x^3 - \frac {12 \sin a x} {a^3} x^2 - \frac {24 \cos a x} {a^4} x + \frac {24 \sin a x} {a^5} } + C
      | c = Primitive of $x^4 \cos a x$
}}
{{eqn | r = \frac {\sin a x} a x^6 + \frac {6 \cos a x} {a^2} x^5 - \frac {30 \sin a x} {a^3} x^4 - \frac {120 \cos a x} {a^4} x^3 + \frac {360 \sin a x} {a^5} x^2 + \frac {720 \cos a x} {a^6} x - \frac {720 \sin a x} {a^7} + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Fourier Series/Sixth Power of x over Minus Pi to Pi

:$\ds x^6 = \frac {\pi^6} 7 + \sum_{n \mathop = 1}^\infty \frac {12 n^4 \pi^4 - 240 n^2 \pi^2 + 1440} {n^6} \cos n \pi \cos n x$

Proof:
Since $x^6 = \paren {-x}^6$, $x^6$ is an even function.
By Fourier Series for Even Function over Symmetric Range, the Fourier series of $\map f x$ can be expressed as:
:$x^6 \sim \dfrac {a_0} 2 + \ds \sum_{n \mathop = 1}^\infty a_n \cos n x$
where for all $n \in \Z_{> 0}$:
{{begin-eqn}}
{{eqn | l = a_n 
      | r = \dfrac 2 \pi \int_0^\pi x^6 \cos n x \  \d x
}}
{{eqn | r = \dfrac 2 \pi \paren {\intlimits {\frac {\sin n x} n x^6 + \frac {6 \cos n x} {n^2} x^5 - \frac {30 \sin n x} {n^3} x^4 - \frac {120 \cos n x} {n^4} x^3 + \frac {360 \sin n x} {n^5} x^2 + \frac {720 \cos n x} {n^6} x - \frac {720 \sin n x} {n^7} } {x \mathop = 0} {x \mathop = \pi} }
      | c = Primitive of $x^6 \cos a x$
}}
{{eqn | r = \dfrac 2 \pi \paren {\frac {6 \pi^5 \cos n \pi} {n^2} - \frac {120 \pi^3 \cos n \pi} {n^4} + \frac {720 \pi \cos n \pi} {n^6}  }
      | c = 
}}
{{eqn | r = \frac {12 n^4 \pi^4 - 240 n^2 \pi^2 + 1440} {n^6} \cos n \pi
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = a_0
      | r = \dfrac 2 \pi \int_0^\pi x^6 \  \d x
}}
{{eqn | r = \dfrac 2 \pi \intlimits {\frac {x^7} 7} {x \mathop = 0} {x \mathop = \pi}
      | c = Primitive of Power
}}
{{eqn | r = \frac {2 \pi^6} 7
}}
{{end-eqn}}
This gives:
:$x^6 \sim \dfrac {\pi^6} 7 + \ds \sum_{n \mathop = 1}^\infty \frac {12 n^4 \pi^4 - 240 n^2 \pi^2 + 1440} {n^6} \cos n \pi \cos n x$
{{qed}}
Theorem: Derivative of x to the a x

:$\dfrac \d {\d x} x^{a x} = a x^{a x} \paren {\ln x + 1}$

Proof:
Let $y := x^{a x}$.
As $x > 0$, we can take the natural logarithm of both sides:
{{begin-eqn}}
{{eqn | l = \ln y
      | r = \ln x^{a x}
}}
{{eqn | r = a x \ln x
      | c = Laws of Logarithms
}}
{{eqn | l = \map {\frac \d {\d x} } {\ln y}
      | r = \map {\frac \d {\d x} } {a x \ln x}
      | c = differentiating both sides {{WRT|Differentiation}} $x$
}}
{{eqn | l = \frac 1 y \frac {\d y} {\d x}
      | r = a \map {\frac \d {\d x} } {x \ln x}
      | c = Chain Rule for Derivatives and Derivative of Natural Logarithm Function
}}
{{eqn | r = a \paren {\map {\frac \d {\d x} } x \cdot \ln x + x \frac {\d} {\d x} \ln x}
      | c = Product Rule for Derivatives
}}
{{eqn | r = a \paren {1 \cdot \ln x + x \cdot \frac 1 x}
      | c = Derivative of Identity Function and Derivative of Natural Logarithm Function
}}
{{eqn | r = a \paren {\ln x + 1}
      | c = simplification
}}
{{eqn | l = \frac {\d y} {\d x}
      | r = a x^{a x} \paren {\ln x + 1}
      | c = multiplying both sides by $y = x^{a x}$
}}
{{end-eqn}}
{{qed}}
Category:Derivative of x to the x
k7bzemqa34muxcyuwp4uuwkipcjckaq
Theorem: Integer as Sum of Polygonal Numbers/Lemma 3

Let $n, m, r \in \R_{>0}$.
Suppose $\dfrac n m > 1$.
Let $b \in \openint {\dfrac 2 3 + \sqrt {8 \paren {\dfrac n m} - 8} } {\dfrac 1 2 + \sqrt {6 \paren {\dfrac n m} - 3} }$.
Define:
:$a = 2 \paren {\dfrac {n - b - r} m} + b = \paren {1 - \dfrac 2 m} b + 2 \paren {\dfrac {n - r} m}$
Then $a, b$ satisfy:
:$b^2 < 4 a$
:$3 a < b^2 + 2 b + 4$

Proof:
=== $b^2 < 4 a$ ===
:$b^2 - 4 a = b^2 - 4 \paren {1 - \dfrac 2 m} b - 8 \paren {\dfrac {n - r} m}$
By the Quadratic Formula, $b^2 - 4 a < 0$ when $b$ is between:
{{begin-eqn}}
{{eqn | o =
      | r = \frac 1 2 \paren {4 \paren {1 - \frac 2 m} \pm \sqrt {16 \paren {1 - \frac 2 m}^2 + 32 \paren {\frac {n - r} m} } }
}}
{{eqn | r = 2 - \frac 4 m \pm \sqrt {\paren {2 - \frac 4 m}^2 + 8 \paren {\frac n m} - 8 \paren {\frac r m} }
}}
{{end-eqn}}
Observing the term in the square root, we have: 
:$2 - \dfrac 4 m - \sqrt {\paren {2 - \dfrac 4 m}^2 + 8 \paren {\dfrac n m} - 8 \paren {\dfrac r m} } < 0$
Since $b > 0$ this is satisfied.
Also we have:
{{begin-eqn}}
{{eqn | l = b
      | o = <
      | r = \frac 2 3 + \sqrt {8 \paren {\frac n m} - 8}
}}
{{eqn | o = <
      | r = 2 - \frac 4 m + \sqrt {8 \paren {\frac n m} - 8 \paren {\dfrac r m} }
      | c = $m \ge 3$, $r < m$
}}
{{eqn | o = \le
      | r = 2 - \frac 4 m + \sqrt {\paren {2 - \frac 4 m}^2 + 8 \paren {\frac n m} - 8 \paren {\dfrac r m} }
      | c = Square is nonnegative
}}
{{end-eqn}}
showing that first inequality is satisfied.
{{qed|lemma}}
Theorem: Integer as Sum of Polygonal Numbers/Lemma 2

Let $n, m \in \R_{>0}$ such that $\dfrac n m \ge 1$.
Define $I$ to be the open real interval:
:$I = \openint {\dfrac 2 3 + \sqrt {8 \paren {\dfrac n m} - 8} } {\dfrac 1 2 + \sqrt {6 \paren {\dfrac n m} - 3} }$
Then:
:For $\dfrac n m \ge 116$, the length of $I$ is greater than $4$.

Proof:
We need to show that $\paren {\dfrac 2 3 + \sqrt {8 \paren {\dfrac n m} - 8} } - \paren {\dfrac 1 2 + \sqrt {6 \paren {\dfrac n m} - 3}} > 4$ when $\dfrac n m \ge 116$.
Let $x = \dfrac n m - 1$. 
Then:
{{begin-eqn}}
{{eqn | l = \paren {\frac 2 3 + \sqrt {8 \paren {\frac n m} - 8} } - \paren {\frac 1 2 + \sqrt {6 \paren {\frac n m} - 3} }
      | o = >
      | r = 4
}}
{{eqn | ll= \leadstoandfrom
      | l = \sqrt {8 x} - \sqrt {6 x + 3}
      | o = >
      | r = \frac {23} 6
}}
{{end-eqn}}
To simplify calculations, we consider:
{{begin-eqn}}
{{eqn | l = \sqrt {8 x} - \sqrt {6 x + 3}
      | o = >
      | r = 4
      | c = which is greater than $\dfrac {23} 6$
}}
{{eqn | ll= \leadstoandfrom
      | l = 8 x + 6 x + 3 - 2 \sqrt {48 x^2 + 24 x}
      | o = >
      | r = 16
      | c = squaring Both Sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \sqrt {48 x^2 + 24 x}
      | o = <
      | r = 7 x - \frac {13} 2
}}
{{eqn | ll= \leadstoandfrom
      | l = 48 x^2 + 24 x
      | o = <
      | r = 49 x^2 - 91 x + \frac {169} 4
      | c = squaring Both Sides
}}
{{eqn | ll= \leadstoandfrom
      | l = x^2 - 115 x + \frac {169} 4
      | o = >
      | r = 0
}}
{{eqn | ll= \leadstoandfrom
      | l = x \paren {x - 115} + \frac {169} 4
      | o = >
      | r = 0
}}
{{end-eqn}}
which is true when $x \ge 115$.
Thus this condition is satisfied when $\dfrac n m \ge 116$.
{{qed}}
Theorem: Integer as Sum of Three Odd Squares

Let $r$ be a positive integer.
Then:
:$r \equiv 3 \pmod 8$
{{iff}}:
:$r$ is the sum of $3$ odd squares.

Proof:
=== Sufficient Condition ===
From Integer as Sum of Three Squares, every positive integer not of the form $4^n \paren {8 m + 7}$ can be expressed as the sum of three squares.
Hence every positive integer $r$ such that $r \equiv 3 \pmod 8$ can likewise be expressed as the sum of three squares.
From Square Modulo 8, the squares modulo $8$ are $0, 1$ and $4$.
Thus for $r$ to be the sum of three squares, each of those squares needs to be congruent modulo $8$ to $1$.
Thus each square is odd, and $r$ can be expressed in the form $8 n + 3$ as the sum of $3$ odd squares.
{{qed|lemma}}
Theorem: Binet Form/Second Form

The recursive sequence:
:$V_n = m V_{n - 1} + V_{n - 2}$
where:
{{begin-eqn}}
{{eqn | l = V_0
      | r = 2
      | c = 
}}
{{eqn | l = V_1
      | r = m
      | c = 
}}
{{end-eqn}}
has the closed-form solution:
:$V_n = \alpha^n + \beta^n$
where $\Delta, \alpha, \beta$ are as for the first form.

Proof:
Proof by induction:
Let $\map P n$ be the proposition:
:$V_n = \alpha^n + \beta^n$
Theorem: Join Semilattice Ordered Subset Not Always Subsemilattice

Let $\struct {S, \circ}$ be a semilattice.
Let $\preceq$ be the ordering on $S$ defined by:
:$a \preceq b \iff \paren {a \circ b} = b$
Let $T$ be a subset of $S$.
Let the ordered subset $\struct {T, \preceq \restriction_T}$ be a join semilattice.
Let $\vee$ be the binary operation on $T$ defined by:
:for all $a, b \in T$: $a \vee b$ is the join of $a$ and $b$ {{WRT}} $\preceq \restriction_T$.
Then:
:$\struct {T, \vee}$ may not be a subsemilattice of $\struct {S, \circ}$.

Proof:
Let $S = \set {p, q, r, s}$.
Let $\circ: S \times S \to S$ be defined by:
:$p \circ q = q \circ p = r$
:$p \circ r = r \circ p = r$
:$q \circ r = r \circ q = r$
:$p \circ s = s \circ p = s$
:$q \circ s = s \circ q = s$
:$r \circ s = s \circ r = s$
:$p \circ p = p$
:$q \circ q = q$
:$r \circ r = r$
:$s \circ s = s$
Then a manual check shows that $\struct {S, \circ}$ satisfies:
:{{Semilattice-axiom|0}}
:{{Semilattice-axiom|1}}
:{{Semilattice-axiom|2}}
:{{Semilattice-axiom|3}}
So $\struct {S, \circ}$ is a semilattice with ordering:
:${\preceq} = \set {\tuple {p, p}, \tuple {q, q}, \tuple {r, r}, \tuple {s, s}, \tuple {p, r}, \tuple {q,r}, \tuple {p, s}, \tuple {q,s}, \tuple {r, s} }$
Let $T = \set {p, q, s}$.
Then:
:${\preceq \restriction_T} = \set {\tuple {p, p}, \tuple {q, q}, \tuple {s, s}, \tuple {p, s}, \tuple {q, s} }$
Then a manual check shows that all joins exist in $\struct {T, \preceq \restriction_T}$:
:$p \vee q = q \vee p = s$
:$p \vee s = s \vee p = s$
:$q \vee s = s \vee q = s$
:$p \vee p = p$
:$q \vee q = q$
:$s \vee s = s$
So $\struct {T, \preceq \restriction_T}$ is a join semilattice {{WRT}} $\preceq \restriction_T$.
Now:
:$p \vee q = s \ne r = p \circ q$
So $\vee$ is not the restriction of $\circ$ to $T$.
That is, $\struct {T, \vee}$ is not a subsemilattice of $\struct {S, \circ}$ by definition.
{{qed}}
Theorem: Closure of Subset of Closed Set of Topological Space is Subset

Let $T$ = $\struct {S, \tau}$ be a topological space.
Let $F$ be a closed set of $T$.
Let $H \subseteq F$ be a subset of $F$.
Let $H^-$ denote the closure of $H$.
Then $H^- \subseteq F$.

Proof:
{{begin-eqn}}
{{eqn | l = H
      | o = \subseteq
      | r = F
}}
{{eqn | ll= \leadsto
      | l = H^-
      | o = \subseteq
      | r = F^-
      | c = Topological Closure of Subset is Subset of Topological Closure
}}
{{eqn | r = F
      | c = Set is Closed iff Equals Topological Closure
}}
{{end-eqn}}
{{qed}}
Theorem: Closure of Subset of Closed Set of Topological Space is Subset

Let $T$ = $\struct {S, \tau}$ be a topological space.
Let $F$ be a closed set of $T$.
Let $H \subseteq F$ be a subset of $F$.
Let $H^-$ denote the closure of $H$.
Then $H^- \subseteq F$.

Proof:
Let $x \notin F$.
Then $x$ is in the open set $S \setminus F$.
From Set Difference with Subset is Superset of Set Difference:
:$S \setminus F \subseteq S \setminus H$
From Subsets of Disjoint Sets are Disjoint:
:$S \setminus F \cap H = \O$
From Set is Open iff Neighborhood of all its Points:
:$S \setminus F$ is an neighborhood of $x$
By definition of the closure of $H$:
:$x \notin H^-$
We have shown that:
:$S \setminus F \subseteq S \setminus H^-$
From Set Difference with Subset is Superset of Set Difference:
:$H^- \subseteq F$
{{qed}}
Theorem: Number of Partial Derivatives of Order n

Let $u = \map f {x_1, x_2, \ldots, x_m}$ be a function of the $m$ independent variables $x_1, x_2, \ldots, x_m$.
There are $m^n$ partial derivatives of $u$ of order $n$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:There are $m^n$ partial derivatives of $u$ of order $n$.
$\map P 0$ is the degenerate case where $f$ is not partially differentiated at all:
:$\map f {x_1, x_2, \ldots, x_m}$
and it is apparent that there is only $1 = m^0$ such.
Thus $\map P 0$ is seen to hold.