avewright/proofwiki-math huggingface dataset:
Theorem: All Bases of Matroid have same Cardinality

Let $M = \struct {S, \mathscr I}$ be a matroid.
Let $\rho: \powerset S \to \Z$ be the rank function of $M$.
Let $B$ be a base of $M$.
Then:
:$\card B = \map \rho S$
That is, all bases of $M$ have the same cardinality, which is the rank of $M$.

Proof:
By definition of the rank function:
:$\map \rho S = \max \set {\card X: X \subseteq S, X \in \mathscr I}$
Let $B_1$ be an independent subset such that:
:$\card {B_1} = \map \rho S$
It is shown that $B_1$ is a base.
Let $X$ be an independent superset of $B_1$.
From Cardinality of Subset of Finite Set:
:$\card {B_1} \le \card X$
By choice of $B_1$:
:$\card X \le \card {B_1}$
It follows that:
:$\card X = \card {B_1}$
From Cardinality of Proper Subset of Finite Set:
:$X = B_1$
It follows that $B_1$ is a maximal independent subset.
That is, $B_1$ is a base.
It is now shown that any other base has the same cardinality as $B_1$.
Let $B_2$ be any other base.
By choice of $B_1$:
:$\card {B_2} \le \card {B_1}$
{{AimForCont}} $\card {B_2} < \card {B_1}$.
From Independent Set can be Augmented by Larger Independent Set there exists $Z \subseteq B_1 \setminus B_2$ such that:
:$B_2 \cup Z \in \mathscr I$
:$\card {B_2 \cup Z} = \card {B_1}$
This contradicts the maximality of $B_2$ in $\mathscr I$.
Then:
:$\card {B_2} = \card {B_1} = \map \rho S$
{{qed}}
Theorem: Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom

Let $S$ be a finite set.
Let $\mathscr B$ be a non-empty set of subsets of $S$.
Then $\mathscr B$ is the set of bases of a matroid on $S$ {{iff}} $\mathscr B$ satisfies formulation $1$ of base axiom:
{{:Axiom:Base Axiom (Matroid)/Formulation 1}}

Proof:
=== Necessary Condition ===
Let $\mathscr B$ be the set of bases of the matroid on $M = \struct{S, \mathscr I}$
{{:Matroid Bases Iff Satisfies Formulation 1 of Matroid Base Axiom/Necessary Condition}}{{qed|lemma}}
Theorem: Number of Integer Partitions into Sum of Consecutive Primes

Let $n$ be a natural number.
Let $\map f n$ denote the number of integer partitions of $n$ where the parts are consecutive prime numbers.
For example:
:$\map f {41} = 3$
because:
:$41 = 11 + 13 + 17 = 2 + 3 + 5 + 7 + 11 + 13$
Then:
:$\ds \lim_{x \mathop \to \infty} \dfrac 1 x \sum_{n \mathop = 1}^x \map f n = \ln 2$

Proof:
Let $\mathbb P$ denote the set of prime numbers.
Every set of consecutive primes whose sum is less than $x$ will contribute $1$ to the sum:
:$\map f 1 + \map f 2 + \dotsb + \map f x$
The number of such sets of $r$ primes is clearly at most:
:$\map \pi {x / r}$
and at least:
:$\map \pi {x / r} - r$
where $\pi$ is the prime-counting function.
Hence:
:$\ds \sum_{r \mathop = 1}^k \paren {\map \pi {x / r} - r} \le \map f 1 + \map f 2 + \dotsb + \map f x \le \sum_{r \mathop = 1}^k \map \pi {x / r}$
where $k$ is determined by:
:$(1): \quad p_1 + p_2 + \dotsb + p_k < x < p_1 + p_2 + . . . + p_{k + 1}$
From $(1)$ and the well known $p_r \asymp r \ln r$ we find:
:$(2): \quad k \asymp \sqrt {\dfrac x {\ln x} }$
Here $f \asymp g$ denotes that $\dfrac f g$ is bounded above and below by positive numbers for large arguments.
This implies:
:$\ds \sum_{r \mathop = 1}^k r = \map o x$
where $\map o x$ denotes little-$\oo$ notation.
Hence, if we can show that:
:$\ds \sum_{r \mathop = 1}^k \map \pi {x / r} \approx \ln 2$
it will follow that:
:$\map f 1 + \map f 2 + \dotsb + \map f x \approx x \ln 2$
Using $(2)$ and the Prime Number Theorem, the following estimates are justified:
{{begin-eqn}}
{{eqn | l = \sum_{r \mathop = 1}^k \map \pi {x / r}
      | o = \approx
      | r = \sum_{r \mathop = 1}^k \dfrac x {r \, \map \ln {x / r} }
      | c = 
}}
{{eqn | o = \approx
      | r = \int_1^k \dfrac {x \rd r} {r \, \map \ln {x / r} }
      | c = 
}}
{{eqn | r = \bigintlimits {-x \map \ln {\map \ln {x / r} } } 1 k
      | c = 
}}
{{eqn | r = x \paren {\ln \ln x - \map {\ln \ln} {x / k} }
      | c = 
}}
{{eqn | o = \approx
      | r = x \paren {\ln \ln x - \ln \ln \sqrt {x \ln x} }
      | c = 
}}
{{eqn | o = \approx
      | r = \ln 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Coherent Sequence Converges to P-adic Integer

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\sequence {\alpha_n}$ be a coherent sequence. 
Let $\Z_p$ be the $p$-adic integers.
Then the sequence $\sequence {\alpha_n}$ converges to some $x \in \Z_p$.
That is, there exists $x \in \Z_p$ such that:
:$\ds \lim_{n \mathop \to \infty} \alpha_n = x$

Proof:
From Coherent Sequence is Partial Sum of P-adic Expansion there exists a unique $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$
such that:
:$\forall n \in \N: \alpha_n = \ds \sum_{i \mathop = 0}^n d_i p^i$
From P-adic Expansion Converges to P-adic Number:
:$\exists x \in \Q_p : \ds \lim_{n \mathop \to \infty} \alpha_n = x$
By definition of a coherent sequence:
:$\forall n \in \N: \alpha_n \in \Z \subseteq \Z_p$
By definition, the $p$-adic integers $\Z_p$ is the closed ball $\map {B^-_1} 0$.
From Closed Ball of Non-Archimedean Division Ring is Clopen, $\Z_p$ is closed in $\norm{\,\cdot\,}_p$.
From Subset of Metric Space contains Limits of Sequences iff Closed:
:$x \in \Z_p$
The result follows.
{{qed}}
Theorem: Dixon's Theorem (Group Theory)

Let $P_1$ and $P_2$ be distinct elements of the symmetric group on $n$ letters.
The probability that $\set {P_1, P_2}$ forms a generator of $S_n$ approaches $\dfrac 3 4$ as $n$ tends to infinity.

Proof:
{{ProofWanted}}
{{Namedfor|John Douglas Dixon|cat = Dixon, J.D.}}
Theorem: P-adic Integer is Limit of Unique P-adic Expansion

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\Z_p$ be the $p$-adic integers.
Let $x \in \Z_p$.
Then $x$ is the limit of a unique $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$

Proof:
From P-adic Integer is Limit of Unique Coherent Sequence of Integers, there exists a unique coherent sequence $\sequence{\alpha_n}$ such that:
:$\ds \lim_{n \mathop \to \infty} \alpha_n = x$
From Coherent Sequence is Partial Sum of P-adic Expansion, there exists a unique $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$
such that:
:$\forall n \in \N: \alpha_n = \ds \sum_{i \mathop = 0}^n d_i p^i$
That is:
:$\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = 0}^n d_i p^i = x$
{{qed}}
Theorem: P-adic Number is Limit of Unique P-adic Expansion

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $x \in \Q_p$.
Then $x$ is the limit of a unique $p$-adic expansion.

Proof:
Let $\Z_p$ be the $p$-adic integers.
From P-adic Number times Integer Power of p is P-adic Integer:
:$\exists m \in \Z_{\ge 0} : x p^m \in \Z_p$
From P-adic Integer is Limit of Unique P-adic Expansion, there exists a unique $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$
such that:
:$\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = 0}^n d_i p^i = x p^m$
From Multiple Rule for Sequences in Normed Division Ring:
:$\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = 0}^n d_i p^{i - m} = x$
Re-indexing from $-m$:
:$\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = -m}^n d_i' p^i = x$
where:
:$\forall i \in \Z_{\ge -m} : d_i' = d_{i + m}$
Then the $p$-adic expansion $\ds \sum_{n \mathop = -m}^\infty d_n' p^n$ converges to $x$.
Let $\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = -m}^n e_i p^i = x$.
From Multiple Rule for Sequences in Normed Division Ring:
:$\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = -m}^n e_i p^{i + m} = x p^m$
Re-indexing from $0$:
:$\ds \lim_{n \mathop \to \infty} \sum_{i \mathop = 0}^n e_i' p^i = x p^m$
where:
:$\forall i \in \Z_{\ge -m} : e_i' = e_{i - m}$
From P-adic Integer is Limit of Unique P-adic Expansion:
:$\forall i \in \Z_{\ge 0} : e_i' = d_i$
Re-indexing from $-m$:
:$\forall i \in \Z_{\ge -m} : e_i = d_i'$
Hence $\ds \sum_{n \mathop = -m}^\infty d_n' p^n$ is the unique $p$-adic expansion that converges to $x$.
{{qed}}
Theorem: Finite Set Contains Subset of Smaller Cardinality

Let $S$ be a finite sets.
Let
:$\size S = n$
where $\size {\, \cdot \,}$ denotes cardinality.
Let $0 \le m \le n$.
Then there exists a subset $X \subseteq S$ such that:
:$\size X = m$

Proof:
=== Case 1 ===
Let $m = n$. 
Then $X = S$ is a subset $X \subseteq S$ such that:
:$\size X = m$
{{qed|lemma}}
Theorem: Integral from 0 to 1 of Complete Elliptic Integral of First Kind

Let $G$ denote Catalan's constant.
Then:
:$2 G = \ds \int_0^1 \map K k \rd k$
where $\map K k$ denotes the complete elliptic integral of the first kind:
:$\map K k = \ds \int \limits_0^{\pi / 2} \dfrac {\d \phi} {\sqrt {1 - k^2 \sin^2 \phi} }$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^1 \map K k \rd k
      | r = \int_0^1 \int_0^{\pi / 2} \dfrac 1 {\sqrt {1 - k^2 \sin^2 \phi} } \rd \phi \rd k
      | c = {{Defof|Complete Elliptic Integral of the First Kind}}
}}
{{eqn | r = \int_0^{\pi / 2} \int_0^1 \dfrac 1 {\sqrt {1 - k^2 \sin^2 \phi} } \rd k \rd \phi
      | c = Tonelli's Theorem
}}
{{eqn | r = \int_0^{\pi / 2} \dfrac 1 {\sin \phi} \int_0^{\sin \phi} \dfrac 1 {\sqrt {1 - u^2} } \rd u \rd \phi
      | c = Substitution of $u = k \sin \phi$ and $\rd u = \rd k \sin \phi$
}}
{{eqn | r = \int_0^{\pi / 2} \dfrac {\map \arcsin {\sin \phi} } {\sin \phi} \rd \phi
      | c = Arcsine as Integral
}}
{{eqn | r = \int_0^{\pi / 2} \dfrac \phi {\sin \phi} \rd \phi
      | c = {{Defof|Inverse Sine}}
}}
{{eqn | r = 2 \int_0^{\pi / 4} \dfrac {2 \theta} {\sin 2 \theta} \rd \theta
      | c = Substitution of $2 \theta = \phi$ and $2 \rd \theta = \rd \phi$
}}
{{eqn | r = 2 \int_0^{\pi / 4} \dfrac {\theta} {\sin \theta \cos \theta} \rd \theta
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 2 \int_0^{\pi / 4} \dfrac {\theta} {\sin \theta \times \dfrac {\cos \theta} {\cos \theta} \times \cos \theta} \rd \theta
      | c = multiplying by $1$
}}
{{eqn | r = 2 \int_0^{\pi / 4} \dfrac \theta {\tan \theta} \sec^2 \theta \rd \theta
      | c = 
}}
{{eqn | r = 2 \int_0^1 \dfrac {\arctan t} t \rd t
      | c = Substitution of $t = \tan \theta$ and $\rd t = \sec^2 \theta \rd \theta$
}}
{{eqn | r = 2 \int_0^1 \dfrac 1 t \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {t^{2 n + 1} } {2 n + 1} \rd t
      | c = Power Series Expansion for Real Arctangent Function
}}
{{eqn | r = 2 \sum_{n \mathop = 0}^\infty \dfrac {\paren {-1}^n} {2 n + 1} \int_0^1 t^{2 n} \rd t
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = 2 \sum_{n \mathop = 0}^\infty \dfrac {\paren {-1}^n} {\paren {2 n + 1}^2}
      | c = Integral of Power
}}
{{eqn | r = 2 G 
      | c = {{Defof|Catalan's Constant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Trivial Group is Smallest Group

Let $G = \struct {\set e, \circ}$ be a trivial group.
Then $G$ is the smallest group possible, in that there exists no set with lower cardinality which is the underlying set of a group.

Proof:
From Trivial Group is Group, we have that there does exist a group of cardinality $1$.
From Group is not Empty, there can be no group of smaller order.
{{qed}}
Theorem: Sum to Infinity of Reciprocal of n^4 by 2n Choose n

It is conjectured that:
:$\map \zeta 4 = \ds \dfrac {36} {17} \sum_{n \mathop = 1}^\infty \dfrac 1 {n^4 \dbinom {2 n} n}$

Proof:
{{ProofWanted|The significance of this result is not clear.}}
Theorem: Partial Sums of P-adic Expansion forms Coherent Sequence

Let $p$ be a prime number.
Let $\ds \sum_{n \mathop = 0}^\infty d_n p^n$ be a $p$-adic expansion.
Let $\sequence {\alpha_n}$ be the sequence of partial sums; that is:
:$\forall n \in \N :\alpha_n = \ds \sum_{i \mathop = 0}^n d_i p^i$.
Then $\sequence {\alpha_n}$ is a coherent sequence.

Proof:
From the definition of a coherent sequence, it needs to be shown that $\sequence {\alpha_n}$ is a sequence of integers such that:
:$(1): \quad \forall n \in \N: 0 \le \alpha_n < p^{n + 1}$
:$(2): \quad \forall n \in \N: \alpha_{n + 1} \equiv \alpha_n \pmod {p^{n + 1}}$
That the sequence $\sequence {\alpha_n}$ is a sequence of integers follows immediately from the assumption that the series begins at $n = 0$ and so the terms of each summation are integers. 
First note:
{{begin-eqn}}
{{eqn | q = \forall n \in \N
      | l = \alpha_{n + 1}
      | r = \ds \sum_{i \mathop = 0}^{n + 1} d_i p^i
}}
{{eqn | r = \ds \sum_{i \mathop = 0}^n d_i p^i + d_{n + 1} p^{n + 1}
}}
{{eqn | r = \alpha_n + d_{n + 1} p^{n + 1}
}}
{{end-eqn}}
Theorem: P-adic Expansion is a Cauchy Sequence in P-adic Norm/Represents a P-adic Number

Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic Numbers.
Then the sequence of partial sums of the series:
:$\ds \sum_{n \mathop = m}^\infty d_n p^n$
represents a $p$-adic number of $\struct {\Q_p,\norm {\,\cdot\,}_p}$.

Proof:
From P-adic Expansion is a Cauchy Sequence in P-adic Norm, the sequence of partial sums of the series:
:$\ds \sum_{n \mathop = m}^\infty d_n p^n$
is a Cauchy Sequence.
Then the sequence of partial sums of the series:
:$\ds \sum_{n \mathop = m}^\infty d_n p^n$
is a representative of a $p$-adic number by definition.
{{qed}}
Theorem: Gibbs Phenomenon

The Fourier series overshoots at a jump discontinuity, and adding more terms to the sum does not cause this overshoot to die out.
:500px
:500px
{{finish|Anyone care to flesh this out? I've got bored with it.}}

Proof:
{{ProofWanted|Working on it}}
{{Namedfor|Josiah Willard Gibbs|cat = Gibbs}}
Theorem: Root of Equation e^x (x - 1) = e^-x (x + 1)

The equation:
:$e^x \paren {x - 1} = e^{-x} \paren {x + 1}$
has a root:
:$x = 1 \cdotp 19966 \, 78640 \, 25773 \, 4 \ldots$

Proof:
Let $\map f x = e^x \paren {x - 1} - e^{-x} \paren {x + 1}$.
Then if $\map f c = 0$, $c$ is a root of $e^x \paren {x - 1} = e^{-x} \paren {x + 1}$.
Notice that:
:$\map f 1 = e^1 \paren {1 - 1} - e^{-1} \paren {1 + 1} = -\dfrac 2 e < 0$
:$\map f 2 = e^2 \paren {2 - 1} - e^{-2} \paren {2 + 1} = e^2 - \dfrac 3 {e^2} > 0$
By Intermediate Value Theorem:
:$\exists c \in \openint 1 2: \map f c = 0$.
This shows that our equation has a root between $1$ and $2$.
The exact value of this root can be found using any numerical method, e.g. Newton's Method.
{{ProofWanted|Analysis needed of the Kepler Equation}}
Theorem: Mergelyan-Wesler Theorem

Let $P = \sequence {D_1, D_2, \dotsc}$ be an infinite sequence of disjoint open disks whose union is the unit disk $D$ except for a set of measure zero.
Let $r_n$ be the radius of $D_n$.
Then:
:$\ds \sum_{k \mathop = 1}^\infty r_k = +\infty$

Proof:
{{ProofWanted}}
{{Namedfor|Sergey Nikitovich Mergelyan|name2 = Oscar Wesler|cat = Mergelyan|cat2 = Wesler}}
Theorem: Integer Arbitrarily Close to Rational in Valuation Ring of P-adic Norm

Let $\norm {\,\cdot\,}_p$ be the $p$-adic norm on the rationals $\Q$ for some prime number $p$.
Let $x \in \Q$ such that $\norm x_p \le 1$.
Then for all $i \in \N$ there exists $\alpha \in \Z$ such that:
:$\norm {x - \alpha}_p \le p^{-i}$

Proof:
Let $i \in \N$.
Let $x = \dfrac a b: a, b \in \Z \text{ and } b \ne 0$.
{{WLOG}} we can assume that $\dfrac a b$ is in canonical form.
By Valuation Ring of P-adic Norm on Rationals:
:$\dfrac a b \in \Z_{\paren p} = \set {\dfrac c d \in \Q : p \nmid d}$
So $p \nmid b$.
Since $p \nmid b$, by Prime not Divisor implies Coprime then $p^i \perp b$.
By Integer Combination of Coprime Integers, there exists $m, l \in \Z: m b + l p^i = 1$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {\dfrac a b - am}_p
      | r = \norm {\dfrac a b}_p \norm {1 - a m b}_p
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | o = \le
      | r = \norm {1 - m b}_p
      | c = As $\norm {\dfrac a b}_p \le 1$
}}
{{eqn | r = \norm {l p^i}_p
      | c = As $1 - m b = l p^i$
}}
{{eqn | o = \le
      | r = p^{-i}
      | c = {{Defof|P-adic Norm|$p$-adic norm on integers}}
}}
{{end-eqn}}
As $am \in \Z$, the result follows with $\alpha = am$.
{{qed}}
Theorem: P-adic Integer has Unique Coherent Sequence Representative

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a$ be a $p$-adic number, that is left coset, in $\Q_p$ such that $\norm a _p \le 1$.
Then $a$ has exactly one representative that is a coherent sequence.

Proof:
Let $\sequence{\beta_n}$ be a sequence representing $a$.
That is, $\sequence{\beta_n}$ is a Cauchy sequence in the $p$-adic norm $\norm{\,\cdot\,}_p$ on the rational numbers $\Q$.
By definition of a Cauchy sequence:
:$\forall j \in \N : \exists \mathop {\map M j} \in \N: \forall m, n \in \N: m, n \ge \map M j : \norm {x_n - x_m} < p^{-j}$
For all $j \in \N$, let:
:$\map N j = \max \set{j, \map M j}$
From P-adic Norm of p-adic Number is Power of p,
:$\forall j \in \N : \exists \mathop {\map N j} \ge j : \forall m, n \in \N: m, n \ge \map N j : \norm {\beta_n - \beta_m} \le p^{-\paren{j + 1}}$
Theorem: P-adic Integer has Unique Coherent Sequence Representative/P-adic Expansion

Then $a$ has exactly one representative that is a $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$

Proof:
From P-adic Integer has Unique Coherent Sequence Representative, $a$ has exactly one representative coherent sequence.
Let $\sequence{\alpha_n}$ be the coherent sequence such that:
:$\sequence{\alpha_n}$ is a representative of $a$.
From Coherent Sequence is Partial Sum of P-adic Expansion, there exists a $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$
such that:
:$\forall n \in \N: \alpha_n = \ds \sum_{i \mathop = 0}^n d_i p^i$
Then $\ds \sum_{n \mathop = 0}^\infty d_n p^n$ is a representative of $a$.
Let $\ds \sum_{n \mathop = 0}^\infty d'_n p^n$ be a $p$-adic expansion that is a representative of $a$.
From Partial Sums of P-adic Expansion forms Coherent Sequence, the partial sums:
:$\forall n \in \N: \alpha'_n = \ds \sum_{i \mathop = 0}^n d'_i p^i$
are a coherent sequence that is a representative of $a$.
Since $\sequence{\alpha_n}$ is the only coherent sequence that is a  representative of $a$, then:
:$\sequence{\alpha'_n} = \sequence{\alpha_n}$
It follows that:
:$\forall n \in \N : d'_n = d_n$
Then $\ds \sum_{n \mathop = 0}^\infty d_n p^n$ is the only $p$-adic expansion that is a representative of $a$.
{{qed}}
Theorem: P-adic Number has Unique P-adic Expansion Representative

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a$ be a $p$-adic number, that is left coset, in $\Q_p$.
Then $a$ has exactly one representative that is a $p$-adic expansion.

Proof:
=== Case 1 ===
Let $\norm a_p \le 1$.
From P-adic Integer has Unique P-adic Expansion Representative, $a$ has exactly one representative that is a $p$-adic expansion of the form:
:$\ds \sum_{n \mathop = 0}^\infty d_n p^n$
{{qed|lemma}}
Theorem: Value of Plastic Constant

The plastic constant $P$ is evaluated as:
{{begin-eqn}}
{{eqn | l = P
      | r = \sqrt [3] {\frac {9 + \sqrt {69} } {18} } + \sqrt [3] {\frac {9 - \sqrt {69} } {18} }
      | c = 
}}
{{eqn | r = 1 \cdotp 32471 \, 79572 \, 44746 \, 02596 \, 09088 \, 54 \ldots
      | c = 
}}
{{end-eqn}}

Proof:
By definition, the plastic constant $P$ is the real root of the cubic:
:$x^3 - x - 1 = 0$
Recall Cardano's Formula:
{{:Cardano's Formula}}
Here we have:
{{begin-eqn}}
{{eqn | l = a
      | r = 1
}}
{{eqn | l = b
      | r = 0
}}
{{eqn | l = c
      | r = -1
}}
{{eqn | l = d
      | r = -1
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = Q
      | r = \dfrac {3 \times 1 \times \paren {-1} - 0^2} {9 \times 1^2}
      | c = 
}}
{{eqn | r = \dfrac {-3} 9
      | c = 
}}
{{eqn | r = -\dfrac 1 3
      | c = 
}}
{{eqn | l = R
      | r = \dfrac {9 \times 1 \times 0 \times \paren {-1} - 27 \times 1^2 \times \paren {-1} - 2 \times 0^3} {54 \times 1^3}
      | c = 
}}
{{eqn | r = \dfrac {27} {54}
      | c = 
}}
{{eqn | r = \dfrac 1 2
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \sqrt {Q^3 + R^2}
      | r = \sqrt {\paren {-\dfrac 1 3}^3 + \paren {\dfrac 1 2}^2}
      | c = 
}}
{{eqn | r = \sqrt {\dfrac 1 4 - \dfrac 1 {27} }
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {27 - 4} {108} }
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {3 \times 23} {3 \times 2^2 \times 3^3} }
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {69} {18^2} }
      | c = 
}}
{{eqn | r = \dfrac {\sqrt {69} } {18}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = S = \sqrt [3] {R + \sqrt {Q^3 + R^2} }
      | r = \sqrt [3] {\dfrac 1 2 + \dfrac {\sqrt {69} } {18} }
      | c = 
}}
{{eqn | r = \sqrt [3] {\dfrac {9 + \sqrt {69} } {18} }
      | c = 
}}
{{eqn | l = T = \sqrt [3] {R - \sqrt {Q^3 + R^2} }
      | r = \sqrt [3] {\dfrac 1 2 - \dfrac {\sqrt {69} } {18} }
      | c = 
}}
{{eqn | r = \sqrt [3] {\dfrac {9 - \sqrt {69} } {18} }
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = S + T - \dfrac b {3 a}
      | r = \sqrt [3] {\dfrac {9 + \sqrt {69} } {18} } + \sqrt [3] {\dfrac {9 - \sqrt {69} } {18} } - \dfrac 0 {3 \times 1}
      | c = 
}}
{{eqn | r = \sqrt [3] {\dfrac {9 + \sqrt {69} } {18} } + \sqrt [3] {\dfrac {9 - \sqrt {69} } {18} }
      | c = 
}}
{{end-eqn}}
The number can then be calculated.
Since $S \ne T$, the other two roots $x_2, x_3$ has non-zero imaginary parts $\pm \dfrac {i \sqrt 3} 2 \paren {S - T}$.
Hence the root above is the only real root.
{{qed}}
Theorem: Unique Integer Close to Rational in Valuation Ring of P-adic Norm

Let $\norm {\,\cdot\,}_p$ be the $p$-adic norm on the rationals $\Q$ for some prime number $p$.
Let $x \in \Q$ such that $\norm{x}_p \le 1$.
Then for all $i \in \N$ there exists a unique $\alpha \in \Z$ such that:
:$(1): \quad \norm {x - \alpha}_p \le p^{-i}$
:$(2): \quad  0 \le \alpha \le p^i - 1$

Proof:
Let $i \in \N$.
From Integer Arbitrarily Close to Rational in Valuation Ring of P-adic Norm:
:$\exists \mathop {\alpha'} \in \Z: \norm{x - \alpha'}_p \le p^{-i}$
By Integer is Congruent to Integer less than Modulus, then there exists $\alpha \in \Z$:
:$\alpha \equiv \alpha' \pmod {p^i}$.
:$0 \le \alpha \le p^i - 1$
Then $\norm {\alpha' - \alpha}_p \le p^{-i}$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {x - \alpha}_p
      | r = \norm {\paren {x - \alpha'} + \paren {\alpha' - \alpha} }_p
}}
{{eqn | o = \le
      | r = \max \set {\norm {x - \alpha'}_p, \norm {\alpha' - \alpha}_p }
      | c = {{NormAxiomNonArch|4}}
}}
{{eqn | o = \le
      | r = p^{-i}
}}
{{end-eqn}}
Now suppose $\beta \in \Z$ satisfies:
:$(\text a): \quad 0 \le \beta \le p^i - 1$
:$(\text b): \quad \norm {x -\beta}_p \le p^{-i}$
Then:
{{begin-eqn}}
{{eqn | l = \norm {\alpha - \beta}_p
      | r = \norm {\paren{\alpha - x} + \paren {x - \beta} }_p
}}
{{eqn | o = \le
      | r = \max \set {\norm{\alpha - x}_p, \: \norm {x - \beta}_p}
      | c = {{NormAxiomNonArch|4}}
}}
{{eqn | o = \le
      | r = \max \set {\norm {x - \alpha}_p, \: \norm {x - \beta}_p}
      | c = Norm of Negative
}}
{{eqn | o = \le
      | r = p^{-i}
}}
{{end-eqn}}
Hence $p^i \divides \alpha - \beta$, or equivalently, $\alpha \equiv \beta \pmod {p^i}$
By Initial Segment of Natural Numbers forms Complete Residue System then $\alpha = \beta$.
The result follows.
{{qed}}
Theorem: Hermite Constant for Dimension 2

The Hermite constant for dimension $2$ is:
:$\gamma_2 = \dfrac 2 {\sqrt 3}$
or, as it is often presented:
:$\paren {\gamma_2}^2 = \dfrac 4 3$

Proof:
The statement of the result to be proved can be expressed as:
:There exist non-zero $x$ and $y$ such that:
::$\paren {a x^2 + 2 b x y + c y^2}^2 \le \size {a c - b^2} \times \dfrac 4 3$
{{ProofWanted|over my head}}
Theorem: Angle between Straight Lines in Plane

Let $L_1$ and $L_2$ be straight lines embedded in a cartesian plane, given by the equations:
{{begin-eqn}}
{{eqn | q = L_1
      | l = y
      | r = m_1 x + c_1
}}
{{eqn | q = L_2
      | l = y
      | r = m_2 x + c_2
}}
{{end-eqn}}
Then the angle $\psi$ between $L_1$ and $L_2$ is given by:
:$\psi = \arctan \dfrac {m_1 - m_2} {1 + m_1 m_2}$

Proof:
:500px
Let $\psi_1$ and $\psi_2$ be the angles that $L_1$ and $L_2$ make with the $x$-axis respectively.
Then by the definition of slope:
{{begin-eqn}}
{{eqn | l = \tan \psi_1
      | r = m_1
}}
{{eqn | l = \tan \psi_2
      | r = m_2
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \tan \psi
      | r = \map \tan {\psi_2 - \psi_1}
      | c = 
}}
{{eqn | r = \dfrac {\tan \psi_2 - \tan \psi_1} {1 + \tan \psi_1 \tan \psi_2}
      | c = Tangent of Difference
}}
{{eqn | r = \dfrac {m_2 - m_1} {1 + m_1 m_2}
      | c = Definition of $m_1$ and $m_2$
}}
{{end-eqn}}
{{qed}}