avewright/proofwiki-math huggingface dataset:
Theorem: P-adic Numbers is Locally Compact Topological Space

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\tau_p$ be the topology induced by the non-Archimedean norm $\norm {\,\cdot\,}_p$.
Then the topological space $\struct {\Q_p, \tau_p}$ is locally compact.

Proof:
From Local Basis of P-adic Number:
:$\forall a \in \Q_p$: the set $\set {\map {B_{p^{-n} } } a: n \in Z}$ is a local basis of $a$.
From Open and Closed Balls in P-adic Numbers are Compact Subspaces;
:$\forall a \in \Q_p$: the set $\set {\map {B_{p^{-n} } } a: n \in Z}$ is a local basis of compact sets of $a$.
Hence $\struct {\Q_p, \norm {\,\cdot\,}_p}$ is locally compact by definition.
{{qed}}
Theorem: Open and Closed Balls in P-adic Numbers are Compact Subspaces

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $a \in \Q_p$.
Let $n \in \Z$.
Then the open ball $\map {B_{p^{-n} } } a$ and closed ball $\map {B^-_{p^{-n}}} a$ are compact.

Proof:
We begin by proving the theorem for the closed ball $\map {B^-_{p^{-n} } } a$.
From Open Ball in P-adic Numbers is Closed Ball then the theorem will be proved.
Let $d$ denote the subspace metric induced on $\map {B^-_{p^{-n}}} a$ by the $p$-adic Metric.
From Open and Closed Balls in P-adic Numbers are Totally Bounded:
:the closed ball $\map {B^-_{p^{-n}}} a$ is totally bounded in $d$.
From P-adic Numbers form Completion of Rational Numbers with P-adic Norm:
:$\struct {\Q_p, \norm {\,\cdot\,}_p}$ is complete.
From Open and Closed Balls in P-adic Numbers are Clopen in P-adic Metric:
:the closed ball $\map {B^-_{p^{-n}}} a$ is closed in the $p$-adic metric.
From Subspace of Complete Metric Space is Closed iff Complete:
:the closed ball $\map {B^-_{p^{-n}}} a$ is complete in $d$.
From Complete and Totally Bounded Metric Space is Sequentially Compact:
:the closed ball $\map {B^-_{p^{-n}}} a$ is sequentially compact in $d$.
From Sequentially Compact Metric Space is Compact:
:the closed ball $\map {B^-_{p^{-n} } } a$ is compact in $d$.
Hence the closed ball $\map {B^-_{p^{-n} } } a$ is a compact subspace in the $p$-adic metric by definition.
The result follows.
{{qed}}
Category:Topology of P-adic Numbers
68dvzuqpxbl73clpkn79ncvt0f6sb2n
Theorem: Ambiguous Case for Triangle Side-Side-Angle Congruence

Let $\triangle ABC$ be a triangle.
Let the sides $a, b, c$ of $\triangle ABC$ be opposite $A, B, C$ respectively.
Let the sides $a$ and $b$ be known.
Let the angle $\angle B$ also be known.
Then it may not be possible to know the value of $\angle A$.
This is known as the '''ambiguous case'''.

Proof:
From the Law of Sines, we have:
:$\dfrac {\sin a} {\sin A} = \dfrac {\sin b} {\sin B} = \dfrac {\sin c} {\sin C}$
from which:
:$\sin A = \dfrac {\sin a \sin B} {\sin b}$
We find that $0 < \sin A \le 1$.
We have that:
:$\sin A = \map \sin {\pi - A}$
and so unless $\sin A = 1$ and so $A = \dfrac \pi 2$, it is not possible to tell which of $A$ or $\pi - A$ provides the correct solution.
:400px
{{qed}}
Theorem: Analogue Formula for Spherical Law of Cosines

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Then:
{{begin-eqn}}
{{eqn | l = \sin a \cos B
      | r = \cos b \sin c - \sin b \cos c \cos A
}}
{{eqn | l = \sin a \cos C
      | r = \cos c \sin b - \sin c \cos b \cos A
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \sin c \sin a \cos B
      | r = \cos b - \cos c \cos a
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos b - \cos c \paren {\cos b \cos c + \sin b \sin c \cos A}
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos b \paren {1 - \cos^2 c} - \sin b \sin c \cos c \cos A
      | c = rearranging
}}
{{eqn | r = \sin^2 c \cos b - \sin b \sin c \cos c \cos A
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin a \cos B
      | r = \sin c \cos b - \sin b \cos c \cos A
      | c = simplifying
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sin a \sin b \cos C
      | r = \cos c - \cos a \cos b
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos c - \cos b \paren {\cos b \cos c + \sin b \sin c \cos A}
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos c \paren {1 - \cos^2 b} - \sin b \sin c \cos b \cos A
      | c = rearranging
}}
{{eqn | r = \sin^2 b \cos c - \sin b \sin c \cos b \cos A
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin a \cos C
      | r = \cos b \sin c - \sin c \cos b \cos A
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Analogue Formula for Spherical Law of Cosines

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Then:
{{begin-eqn}}
{{eqn | l = \sin a \cos B
      | r = \cos b \sin c - \sin b \cos c \cos A
}}
{{eqn | l = \sin a \cos C
      | r = \cos c \sin b - \sin c \cos b \cos A
}}
{{end-eqn}}

Proof:
:500px
Suppose $c$ is less than $\dfrac \pi 2$.
Let $BA$ be produced to $D$ so that $BD = \dfrac \pi 2$.
Then:
:$AD = \dfrac \pi 2 - c$
and:
:$\angle CAD = pi - A$
Let $C$ and $D$ be joined by an arc of a great circle, denoted $x$.
From the triangle $\sphericalangle DAC$, using the Spherical Law of Cosines:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \map \cos {\dfrac \pi 2 - c} \cos b + \map \sin {\dfrac \pi 2 - c} \sin b \, \map \cos {\pi - A}
      | c = 
}}
{{eqn | r = \sin c \cos b - \cos c \sin b \cos A
      | c = 
}}
{{end-eqn}}
From the triangle $\sphericalangle DBC$, using the Spherical Law of Cosines:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \cos \dfrac \pi 2 \cos a + \sin \pi 2 \sin a \cos B
      | c = 
}}
{{eqn | r = \sin a \cos B
      | c = 
}}
{{end-eqn}}
Hence:
:$\sin a \cos B = \sin c \cos b - \cos c \sin b \cos A$
The case where $c > \dfrac \pi 2$ is worked similarly, but by making $D$ the point between $A$ and $B$ such that $BD$ is $\dfrac \pi 2$.
{{qed}}
Theorem: Four-Parts Formula

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
We have:
:$\cos a \cos C = \sin a \cot b - \sin C \cot B$
That is:
:$\map \cos {\text {inner side} } \cdot \map \cos {\text {inner angle} } = \map \sin {\text {inner side} } \cdot \map \cot {\text {other side} } - \map \sin {\text {inner angle} } \cdot \map \cot {\text {other angle} }$
This is known as the '''four-parts formula''', as it defines the relationship between each of four consecutive parts of $\triangle ABC$.

Proof:
:400px
{{begin-eqn}}
{{eqn | l = \cos b
      | r = \cos a \cos c + \sin a \sin c \cos B
      | c = Spherical Law of Cosines
}}
{{eqn | l = \cos c
      | r = \cos b \cos a + \sin b \sin a \cos C
      | c = Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = \cos b
      | r = \cos a \paren {\cos b \cos a + \sin b \sin a \cos C} + \sin a \sin c \cos B
      | c = substituting for $\cos c$
}}
{{eqn | ll= \leadsto
      | l = \cos b
      | r = \cos^2 a \cos b + \cos a \sin b \sin a \cos C + \sin a \sin c \cos B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos b \paren {1 - \cos^2 a}
      | r = \cos a \sin b \sin a \cos C + \sin a \sin c \cos B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos b \sin^2 a
      | r = \cos a \sin b \sin a \cos C + \sin a \sin c \cos B
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \cot b \sin a
      | r = \cos a \cos C + \dfrac {\sin c} {\sin b} \cos B
      | c = dividing both sides by $\sin a \sin b$
}}
{{eqn | ll= \leadsto
      | l = \cot b \sin a
      | r = \cos a \cos C + \dfrac {\sin C} {\sin B} \cos B
      | c = Spherical Law of Sines
}}
{{eqn | ll= \leadsto
      | l = \cos a \cos C
      | r = \sin a \cot b - \sin C \cot B
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Countable Basis for P-adic Numbers/Closed Balls

For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map {B_\epsilon^-} a$ denote the closed $\epsilon$-ball of $a$.
Then:
:$\BB_p = \set {\map {B^-_{p^{-n} } } q : q \in \Q, n \in \Z}$
is a countable basis for $\struct{\Q_p, \tau_p}$.

Proof:
For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map {B_\epsilon} a$ denote the open $\epsilon$-ball of $a$.
From Open Ball in P-adic Numbers is Closed Ball:
:$\BB_p = \set {\map {B^-_{p^{-n} } } q : q \in \Q, n \in \Z} = \set {\map {B_{p^{-n + 1} } } q : q \in \Q, n \in \Z} = \set {\map {B_{p^{-n} } } q : q \in \Q, n \in \Z}$
From Countable Basis for P-adic Numbers:
:$\BB_p$ is a countable basis for $\struct{\Q_p, \tau_p}$.
{{qed}}
Theorem: Countable Basis for P-adic Numbers/Cosets

Let $\Z_p$ be the $p$-adic integers.
Then:
:$\BB_p = \set {q + p^n \Z_p : q \in \Q, n \in \Z}$
is a countable basis for $\struct{\Q_p, \tau_p}$.

Proof:
For any $\epsilon \in \R_{>0}$ and $a \in \Q_p$ let $\map {B_\epsilon^-} a$ denote the closed $\epsilon$-ball of $a$.
From Closed Balls of P-adic Number:
:$\BB_p = \set {q + p^n \Z_p : q \in \Q, n \in \Z} = \set {\map {B^-_{p^{-n} } } q : q \in \Q, n \in \Z}$
From Countable Closed Ball Basis for P-adic Numbers:
:$\BB_p$ is a countable basis for $\struct{\Q_p, \tau_p}$.
{{qed}}
Theorem: Summary of Topology on P-adic Numbers

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\tau_p$ be the topology induced by the non-Archimedean norm $\norm {\,\cdot\,}_p$.
Then $\struct{\Q_p, \tau_p}$ is:
:$(1): \quad$ Hausdorff
:$(2): \quad$ second-countable
:$(3): \quad$ totally disconnected
:$(4): \quad$ locally compact

Proof:
Follows from:
:P-adic Numbers is Hausdorff Topological Space
:P-adic Numbers is Second Countable Topological Space
:P-adic Numbers is Totally Disconnected Topological Space
:P-adic Numbers is Locally Compact Topological Space
{{qed}}
Theorem: Reciprocal of 7

:$\dfrac 1 7 = 0 \cdotp \dot 14285 \, \dot 7$

Proof:
Performing the calculation using long division:
<pre>
   0.142857...
  ------------
 7)1.000000000
     7
     --
     30
     28
     --
      20
      14
      --
       60
       56
       --
        40
        35
        --
         50
         49
         --
          10
           7
          --
          ..
</pre>
{{qed}}
Category:7
Category:Examples of Reciprocals
n548wo6qzv7svj5rzi05a3pcz8b0yru
Theorem: Spherical Triangle is Polar Triangle of its Polar Triangle

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Let $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$.
Then $\triangle ABC$ is the polar triangle of $\triangle A'B'C'$.

Proof:
:400px
Let $BC$ be produced to meet $A'B'$ and $A'C'$ at $L$ and $M$ respectively.
Because $A'$ is the pole of the great circle $LBCM$, the spherical angle $A'$ equals the side of the spherical triangle $ALM$.
By construction we have that $B'$ is the pole of $AC$.
Thus the length of the arc of the great circle from $B$ to any point on $AC$ is a right angle.
Similarly, the length of the arc of the great circle from $A'$ to any point on $BC$ is also a right angle.
Hence:
:the length of the great circle arc $CA'$ is a right angle
:the length of the great circle arc $CB'$ is a right angle
and it follows by definition that $C$ is a pole of $A'B'$.
In the same way:
:$A$ is a pole of $B'C'$
:$B$ is a pole of $A'C'$.
Hence, by definition, $\triangle ABC$ is the polar triangle of $\triangle A'B'C'$.
{{qed}}
Theorem: Side of Spherical Triangle is Supplement of Angle of Polar Triangle

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Let $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$.
Then $A'$ is the supplement of $a$.
That is:
:$A' = \pi - a$
and it follows by symmetry that:
:$B' = \pi - b$
:$C' = \pi - c$

Proof:
:400px
Let $BC$ be produced to meet $A'B'$ and $A'C'$ at $L$ and $M$ respectively.
Because $A'$ is the pole of the great circle $LBCM$, the spherical angle $A'$ equals the side of the spherical triangle $A'LM$.
That is:
:$(1): \quad \sphericalangle A' = LM$
From Spherical Triangle is Polar Triangle of its Polar Triangle, $\triangle ABC'$ is also the polar triangle of $\triangle A'B'C'$.
That is, $C$ is a pole of the great circle $A'LB'$.
Hence $CL$ is a right angle.
Similarly, $BM$ is also a right angle.
Thus we have:
{{begin-eqn}}
{{eqn | l = LM
      | r = LB + BM
      | c = 
}}
{{eqn | n = 2
      | r = LB + \Box
      | c = where $\Box$ denotes a right angle
}}
{{end-eqn}}
By definition, we have that:
:$BC = a$
{{begin-eqn}}
{{eqn | l = BC
      | r = a
      | c = by definition of $\triangle ABC$
}}
{{eqn | ll= \leadsto
      | l = LB + a
      | r = LC
      | c = 
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = LB
      | r = \Box - a
      | c = as $LC = \Box$
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \sphericalangle A'
      | r = LM
      | c = from $(1)$
}}
{{eqn | r = LB + \Box
      | c = from $(2)$
}}
{{eqn | r = \paren {\Box - a} + \Box
      | c = from $(3)$
}}
{{eqn | r = \paren {2 \Box} - a
      | c = 
}}
{{end-eqn}}
where $2 \Box$ is $2$ right angles, that is, $\pi$ radians.
That is, $A'$ is the supplement of $a$:
:$A' = \pi - a$
By applying the same analysis to $B'$ and $C'$, it follows similarly that:
:$B' = \pi - b$
:$C' = \pi - c$
{{qed}}
Theorem: Integers are Dense in P-adic Integers/Unit Ball

The integers $\Z$ are dense in the closed ball $\map {B^-_1} 0$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map {B^-_1} 0
      | r = \map {B^-_{p^0} } 0
      | c = Zeroth Power of Real Number equals One
}}
{{eqn | r = 0 + p^0 \Z_p
      | c = Closed Balls of P-adic Number    
}}
{{eqn | r = 0 + 1 \cdot \Z_p
}}
{{eqn | r = 0 + \Z_p
      | c = {{Defof|Multiplicative Identity}}
}}
{{eqn | r = \Z_p
      | c = {{Defof|Additive Identity}}
}}
{{end-eqn}}
From Integers are Dense in P-adic Integers, the integers $\Z$ are dense in the closed ball $\map {B^-_1} 0$.
{{qed}}
Category:Integers are Dense in P-adic Integers
ce0zu18re5q9juf68r0397fvuja4g4o
Theorem: Analogue Formula for Spherical Law of Cosines/Corollary

{{begin-eqn}}
{{eqn | l = \sin A \cos b
      | r = \cos B \sin C + \sin B \cos C \cos a
}}
{{eqn | l = \sin A \cos c
      | r = \cos C \sin B + \sin C \cos B \cos a
}}
{{end-eqn}}

Proof:
Let $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$.
Let the sides $a', b', c'$ of $\triangle A'B'C'$ be opposite $A', B', C'$ respectively.
From Spherical Triangle is Polar Triangle of its Polar Triangle we have that:
:not only is $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$
:but also $\triangle ABC$ is the polar triangle of $\triangle A'B'C'$.
We have:
{{begin-eqn}}
{{eqn | l = \sin a' \cos B'
      | r = \cos b' \sin c' - \sin b' \cos c' \cos A'
      | c = Analogue Formula for Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = \map \sin {\pi - A} \, \map \cos {\pi - b}
      | r = \map \cos {\pi - B} \, \map \sin {\pi - C} - \map \sin {\pi - B} \, \map \cos {\pi - C} \, \map \cos {\pi - a}
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle
}}
{{eqn | ll= \leadsto
      | l = \map \sin {\pi - A} \paren {-\cos b}
      | r = \paren {-\cos B} \, \map \sin {\pi - C} - \map \sin {\pi - B} \, \paren {-\cos C} \, \paren {-\cos a}
      | c = Cosine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \sin A \, \paren {-\cos b}
      | r = \paren {-\cos B} \sin C - \sin B \, \paren {-\cos C} \, \paren {-\cos a}
      | c = Sine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \sin A \cos b
      | r = \cos B \sin C + \sin B \cos C \cos a
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
and:
{{begin-eqn}}
{{eqn | l = \sin a' \cos C'
      | r = \cos c' \sin b' - \sin c' \cos b' \cos A'
      | c = Analogue Formula for Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = \map \sin {\pi - A} \, \map \cos {\pi - c}
      | r = \map \cos {\pi - C} \, \map \sin {\pi - B} - \map \sin {\pi - C} \, \map \cos {\pi - B} \, \map \cos {\pi - a}
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle
}}
{{eqn | ll= \leadsto
      | l = \map \sin {\pi - A} \paren {-\cos c}
      | r = \paren {-\cos C} \, \map \sin {\pi - B} - \map \sin {\pi - C} \, \paren {-\cos B} \, \paren {-\cos a}
      | c = Cosine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \sin A \, \paren {-\cos c}
      | r = \paren {-\cos C} \sin B - \sin C \, \paren {-\cos B} \, \paren {-\cos a}
      | c = Sine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \sin A \cos c
      | r = \cos C \sin B + \sin C \cos B \cos a
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Four-Parts Formula/Corollary

:$\cos A \cos c = \sin A \cot B - \sin c \cot b$

Proof:
Let $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$.
Let the sides $a', b', c'$ of $\triangle A'B'C'$ be opposite $A', B', C'$ respectively.
From Spherical Triangle is Polar Triangle of its Polar Triangle we have that:
:not only is $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$
:but also $\triangle ABC$ is the polar triangle of $\triangle A'B'C'$.
We have:
{{begin-eqn}}
{{eqn | l = \cos a' \cos C'
      | r = \sin a' \cot b' - \sin C' \cot B'
      | c = Four-Parts Formula
}}
{{eqn | ll= \leadsto
      | l = \map \cos {\pi - A} \, \map \cos {\pi - c}
      | r = \map \sin {\pi - A} \, \map \cot {\pi - B} - \map \sin {\pi - c} \, \map \cot {\pi - b}
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle
}}
{{eqn | ll= \leadsto
      | l = \paren {-\cos A} \, \paren {-\cos c}
      | r = \map \sin {\pi - A} \, \map \cot {\pi - B} - \map \sin {\pi - c} \, \map \cot {\pi - b}
      | c = Cosine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \paren {-\cos A} \, \paren {-\cos c}
      | r = \sin A \, \map \cot {\pi - B} - \sin c \, \map \cot {\pi - b}
      | c = Sine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \paren {-\cos A} \, \paren {-\cos c}
      | r = \sin A \, \paren {-\cot B} - \sin c \, \paren {-\cot b}
      | c = Cotangent of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \cos A \cos c
      | r = \sin c \cot b - \sin A \cot B 
      | c = simplifying and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Witch of Agnesi/Cartesian

The equation of the Witch of Agnesi is given in cartesian coordinates as:
:$y = \dfrac {8 a^3} {x^2 + 4 a^2}$

Proof:
Let $P = \tuple {x, y}$ and $A = \tuple {d, y}$.
We have that:
:$\dfrac {OM} {MN} = \dfrac {2 a} x = \dfrac y d$.
Also, by Pythagoras's Theorem:
:$\paren {a - y}^2 + d^2 = a^2 \implies y \paren {2 a - y} = d^2$
Eliminating $d$ gives us:
:$\dfrac {y^2} {y \paren {2 a - y} } = \dfrac {\paren {2 a}^2} {x^2}$
Hence:
:$\dfrac y {2 a - y} = \dfrac {4 a^2} {x^2}$
from which:
:$y = \dfrac {8 a^3} {x^2 + 4 a^2}$
{{qed}}
Theorem: Cosine in Terms of Haversine

:$\cos \theta = 1 - 2 \hav \theta$
where $\cos$ denotes cosine and $\hav$ denotes haversine.

Proof:
{{begin-eqn}}
{{eqn | l = \hav \theta
      | r = \dfrac 1 2 \paren {1 - \cos \theta}
      | c = {{Defof|Haversine}}
}}
{{eqn | ll= \leadsto
      | l = 2 \hav \theta
      | r = 1 - \cos \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos \theta
      | r = 1 - 2 \hav \theta
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Spherical Law of Haversines

Let $\triangle ABC$ be a spherical triangle on the surface of a sphere whose center is $O$.
Let the sides $a, b, c$ of $\triangle ABC$ be measured by the angles subtended at $O$, where $a, b, c$ are opposite $A, B, C$ respectively.
Then:
:$\hav a = \map \hav {b - c} + \sin b \sin c \hav A$
where $\hav$ denotes haversine.

Proof:
{{begin-eqn}}
{{eqn | l = \cos a
      | r = \cos b \cos c + \sin b \sin c \cos A
      | c = Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = 1 - 2 \hav a
      | r = \cos b \cos c + \sin b \sin c \paren {1 - 2 \hav A}
      | c = Cosine in Terms of Haversine
}}
{{eqn | r = \map \cos {b - c} - 2 \sin b \sin c \hav A
      | c = Cosine of Difference
}}
{{eqn | r = 1 - 2 \map \hav {b - c} - 2 \sin b \sin c \hav A
      | c = Cosine in Terms of Haversine
}}
{{eqn | ll= \leadsto
      | l = \hav a
      | r = \map \hav {b - c} + \sin b \sin c \hav A
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sign of Haversine

The haversine is non-negative for all $\theta \in \R$.

Proof:
The haversine is conventionally defined on the real numbers only.
We have that:
:$\forall \theta \in \R: -1 < \cos \theta < 1$
and so:
:$\forall \theta \in \R: 0 < 1 - \cos \theta < 2$
from which the result follows by definition of haversine.
{{qed}}
Theorem: Haversine Function is Even

The haversine is an even function:
:$\forall \theta \in \R: \map \hav {-\theta} = \hav \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \map \hav {-\theta}
      | r = \dfrac 1 2 \paren {1 - \map \cos {-\theta} }
      | c = {{Defof|Haversine}}
}}
{{eqn | r = \dfrac 1 2 \paren {1 - \cos \theta}
      | c = Cosine Function is Even
}}
{{eqn | r = \hav \theta
      | c = {{Defof|Haversine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Half Side for Spherical Triangles

:$\sin \dfrac a 2 = \sqrt {\dfrac {-\cos S \, \map \cos {S - A} } {\sin B \sin C} }$
where $S = \dfrac {A + B + C} 2$.

Proof:
Let $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$.
Let the sides $a', b', c'$ of $\triangle A'B'C'$ be opposite $A', B', C'$ respectively.
From Spherical Triangle is Polar Triangle of its Polar Triangle we have that:
:not only is $\triangle A'B'C'$ be the polar triangle of $\triangle ABC$
:but also $\triangle ABC$ is the polar triangle of $\triangle A'B'C'$.
Let $s' = \dfrac {a' + b' + c'} 2$.
We have:
{{begin-eqn}}
{{eqn | l = \cos \dfrac {A'} 2
      | r = \sqrt {\dfrac {\sin s' \, \map \sin {s' - a'} } {\sin b' \sin c'} }
      | c = Cosine of Half Angle for Spherical Triangles
}}
{{eqn | ll= \leadsto
      | l = \cos \dfrac {\pi - a} 2
      | r = \sqrt {\dfrac {\sin s' \, \map \sin {s' - a'} } {\map \sin {\pi - B} \, \map \sin {\pi - C} } }
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle
}}
{{eqn | ll= \leadsto
      | l = \map \cos {\dfrac \pi 2 - \dfrac a 2}
      | r = \sqrt {\dfrac {\sin s' \, \map \sin {s' - a'} } {\sin B \sin C} }
      | c = Sine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \sin \dfrac a 2
      | r = \sqrt {\dfrac {\sin s'  \, \map \sin {s' - a'} } {\sin B \sin C} }
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = s' - a'
      | r = \dfrac {\paren {\pi - A} + \paren {\pi - B} + \paren {\pi - C} } 2 - \paren {\pi - A}
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle 
}}
{{eqn | r = \dfrac \pi 2 - \dfrac {A + B + C} 2 + A
      | c = simplifying
}}
{{eqn | r = \dfrac \pi 2 - \paren {S - A}
      | c = where $S = \dfrac {A + B + C} 2$
}}
{{eqn | ll= \leadsto
      | l = \map \sin {s' - a'}
      | r = \map \sin {\dfrac \pi 2 - \paren {S - A} }
      | c = 
}}
{{eqn | r = \map \cos {S - A}
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = s'
      | r = \dfrac {\paren {\pi - A} + \paren {\pi - B} + \paren {\pi - C} } 2
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle 
}}
{{eqn | r = \dfrac {3 \pi} 2 - \dfrac {A + B + C} 2
      | c = simplifying
}}
{{eqn | r = \dfrac {3 \pi} 2 - S
      | c = where $S = \dfrac {A + B + C} 2$
}}
{{eqn | ll= \leadsto
      | l = \sin s'
      | r = \map \sin {\dfrac {3 \pi} 2 - S}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin s'
      | r = -\map \sin {\dfrac \pi 2 - S}
      | c = Sine of Angle plus Straight Angle
}}
{{eqn | r = -\cos S
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
The result follows.
{{qed}}