avewright/proofwiki-math huggingface dataset:
Theorem: Spherical Law of Sines

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:
:$\dfrac {\sin a} {\sin A} = \dfrac {\sin b} {\sin B} = \dfrac {\sin c} {\sin C}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin b \sin c \cos A
      | r = \cos a - \cos b \cos c
      | c = Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = \sin^2 b \sin^2 c \cos^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin^2 b \sin^2 c \paren {1 - \sin^2 A}
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin^2 b \sin^2 c - \sin^2 b \sin^2 c \sin^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = multiplying out
}}
{{eqn | ll= \leadsto
      | l = \paren {1 - \cos^2 b} \paren {1 - \cos^2 c} - \sin^2 b \sin^2 c \sin^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = 1 - \cos^2 b - \cos^2 c + \cos^2 b \cos^2 c - \sin^2 b \sin^2 c \sin^2 A
      | r = \cos^2 a - 2 \cos a \cos b \cos c + \cos^2 b \cos^2 c
      | c = multiplying out
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin^2 b \sin^2 c \sin^2 A
      | r = 1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c
      | c = rearranging and simplifying
}}
{{end-eqn}}
Let $X \in \R_{>0}$ such that:
:$X^2 \sin^2 a \sin^2 b \sin^2 c = 1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c$
Then from $(1)$:
{{begin-eqn}}
{{eqn | l = \dfrac {X^2 \sin^2 a \sin^2 b \sin^2 c} {\sin^2 b \sin^2 c \sin^2 A}
      | o = =
      | r = \dfrac {1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c} {1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = X^2
      | r = \dfrac {\sin^2 A} {\sin^2 a}
      | c = 
}}
{{end-eqn}}
In a spherical triangle, all of the sides are less than $\pi$ radians.
The same applies to the angles.
From Shape of Sine Function:
:$\sin \theta > 0$ for all $0 < \theta < \pi$
Hence the negative root of $\dfrac {\sin^2 A} {\sin^2 a}$ does not apply, and so:
:$X = \dfrac {\sin A} {\sin a}$
Similarly, from applying the Spherical Law of Cosines to $\cos B$ and $\cos C$:
{{begin-eqn}}
{{eqn | l = \sin a \sin c \cos B
      | r = \cos b - \cos a \cos c
}}
{{eqn | l = \sin a \sin b \cos C
      | r = \cos c - \cos a \cos b
}}
{{end-eqn}}
we arrive at the same point:
{{begin-eqn}}
{{eqn | l = X
      | r = \dfrac {\sin B} {\sin b}
}}
{{eqn | r = \dfrac {\sin A} {\sin a}
}}
{{end-eqn}}
where:
:$X^2 \sin^2 a \sin^2 b \sin^2 c = 1 - \cos^2 a - \cos^2 b - \cos^2 c + 2 \cos a \cos b \cos c$
as before.
Hence we have:
:$\dfrac {\sin a} {\sin A} = \dfrac {\sin b} {\sin B} = \dfrac {\sin c} {\sin C}$
{{qed}}
Theorem: Spherical Law of Sines

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:
:$\dfrac {\sin a} {\sin A} = \dfrac {\sin b} {\sin B} = \dfrac {\sin c} {\sin C}$

Proof:
:500px
Let $A$, $B$ and $C$ be the vertices of a spherical triangle on the surface of a sphere $S$.
By definition of a spherical triangle, $AB$, $BC$ and $AC$ are arcs of great circles on $S$.
By definition of a great circle, the center of each of these great circles is $O$.
Let $O$ be joined to each of $A$, $B$ and $C$.
Let $P$ be an arbitrary point on $OC$.
Construct $PQ$ perpendicular to $OA$ meeting $OA$ at $Q$.
Construct $PR$ perpendicular to $OB$ meeting $OB$ at $R$.
In the plane $OAB$:
:construct $QS$ perpendicular to $OA$
:construct $RS$ perpendicular to $OB$
where $S$ is the point where $QS$ and $RS$ intersect.
Let $OS$ and $PS$ be joined.
Let tangents be constructed at $A$ to the arcs of the great circles $AC$ and $AB$.
These tangents contain the spherical angle $A$.
But by construction, $QS$ and $QP$ are parallel to these tangents.
Hence $\angle PQS = \sphericalangle A$.
Similarly, $\angle PRS = \sphericalangle B$.
Also we have:
{{begin-eqn}}
{{eqn | l = \angle COB
      | r = a
}}
{{eqn | l = \angle COA
      | r = b
}}
{{eqn | l = \angle AOB
      | r = c
}}
{{end-eqn}}
It is to be proved that $PS$ is perpendicular to the plane $AOB$.
By construction, $OQ$ is perpendicular to both $PQ$ and $QS$.
Thus $OQ$ is perpendicular to the plane $PQS$.
Similarly, $OR$ is perpendicular to the plane $PRS$.
Thus $PS$ is perpendicular to both $OQ$ and $OR$.
Thus $PS$ is perpendicular to every line in the plane of $OQ$ and $OR$.
That is, $PS$ is perpendicular to the plane $OAB$.
In particular, $PS$ is perpendicular to $OS$, $SQ$ and $SR$
It follows that $\triangle PQS$ and $\triangle PRS$ are right triangles.
From the right triangles $\triangle OQP$ and $\triangle ORP$, we have:
{{begin-eqn}}
{{eqn | n = 1
      | l = PQ
      | r = OP \sin b
}}
{{eqn | n = 2
      | l = PR
      | r = OP \sin a
}}
{{eqn | n = 3
      | l = OQ
      | r = OP \cos b
}}
{{eqn | n = 4
      | l = OR
      | r = OP \cos a
}}
{{end-eqn}}
From the right triangles $\triangle PQS$ and $\triangle PRS$, we have:
{{begin-eqn}}
{{eqn | l = PS
      | r = PS \sin \angle PRS
}}
{{eqn | r = PQ \sin A
}}
{{eqn | l = PS
      | r = PR \sin \angle PRS
}}
{{eqn | r = PR \sin B
}}
{{eqn | ll= \leadsto
      | l = OP \sin b \sin A
      | r = OP \sin a \sin B
      | c = from $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\sin a} {\sin A}
      | r = \dfrac {\sin b} {\sin B}
      | c = 
}}
{{end-eqn}}
The result follows by applying this technique {{mutatis}} to the other angles of $ABC$.
{{qed}}
Theorem: 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:
:$\cos a = \cos b \cos c + \sin b \sin c \cos A$

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: 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:
:$\cos a = \cos b \cos c + \sin b \sin c \cos A$

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: 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:
:$\cos a = \cos b \cos c + \sin b \sin c \cos A$

Proof:
:500px
Let $A$, $B$ and $C$ be the vertices of a spherical triangle on the surface of a sphere $S$.
By definition of a spherical triangle, $AB$, $BC$ and $AC$ are arcs of great circles on $S$.
By definition of a great circle, the center of each of these great circles is $O$.
Let $AD$ be the tangent to the great circle $AB$.
Let $AE$ be the tangent to the great circle $AC$.
Thus the radius $OA$ of $S$ is perpendicular to $AD$ and $AE$.
By construction, $AD$ lies in the same plane as $AB$.
Thus when $OB$ is produced, it will intersect $AD$ at $D$, say.
Similarly, $OC$ can be produced to intersect $AE$ at $E$, say.
The spherical angle $\sphericalangle BAC$ is defined as the angle between the tangents $AD$ and $AE$.
Thus:
:$\sphericalangle BAC = \angle DAE$
or, denoting that spherical angle $\sphericalangle BAC$ as $A$:
:$A = \angle DAE$
In the (plane) triangle $OAD$, we have that $\angle OAD$ is a right angle.
We also have that $\angle AOD = \angle AOB$ is equal to $c$, by definition of the length of a side of a spherical triangle.
Thus:
{{begin-eqn}}
{{eqn | l = AD
      | r = OA \tan c
      | c = 
}}
{{eqn | l = OD
      | r = OA \sec c
      | c = 
}}
{{end-eqn}}
and by similar analysis of $\triangle OAE$, we have:
{{begin-eqn}}
{{eqn | l = AE
      | r = OA \tan b
      | c = 
}}
{{eqn | l = OE
      | r = OA \sec b
      | c = 
}}
{{end-eqn}}
From consideration of $\triangle DAE$:
{{begin-eqn}}
{{eqn | l = DE^2
      | r = AD^2 + AE^2 - 2 AD \cdot AE \cos \angle DAE
      | c = Law of Cosines
}}
{{eqn | n = 1
      | r = OA^2 \paren {\tan^2 c + \tan^2 b - 2 \tan b \tan c \cos A}
      | c = 
}}
{{end-eqn}}
From consideration of $\triangle DOE$:
{{begin-eqn}}
{{eqn | l = DE^2
      | r = OD^2 + OE^2 - 2 OD \cdot OE \cos \angle DOE
      | c = Law of Cosines
}}
{{eqn | n = 2
      | r = OA^2 \paren {\sec^2 c + \sec^2 b - 2 \sec b \sec c \cos a}
      | c = as $\angle DOE = \angle BOC$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \sec^2 c + \sec^2 b - 2 \sec b \sec c \cos a
      | r = \tan^2 c + \tan^2 b - 2 \tan b \tan c \cos A
      | c = from $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \tan^2 c} + \paren {1 + \tan^2 b} - 2 \sec b \sec c \cos a
      | r = \tan^2 c + \tan^2 b - 2 \tan b \tan c \cos A
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = 1 - \sec b \sec c \cos a
      | r = \tan b \tan c \cos A
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \cos b \cos c - \cos a
      | r = \sin b \sin c \cos A
      | c = multiplying both sides by $\cos b \cos c$
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Spherical Law of Cosines/Angles

:$\cos A = -\cos B \cos C + \sin B \sin C \cos a$

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'
      | r = \cos b' \cos c' + \sin b' \sin c' \cos A'
      | c = Spherical Law of Cosines
}}
{{eqn | ll= \leadsto
      | l = \map \cos {\pi - A}
      | r = \map \cos {\pi - B} \, \map \cos {\pi - C} + \map \sin {\pi - B} \, \map \sin {\pi - C} \, \map \cos {\pi - a}
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle
}}
{{eqn | ll= \leadsto
      | l = -\cos A
      | r = \paren {-\cos B} \paren {-\cos C} + \map \sin {\pi - B} \, \map \sin {\pi - C} \, \paren {-\cos a}
      | c = Cosine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = -\cos A
      | r = \paren {-\cos B} \paren {-\cos C} + \sin B \sin C \paren {-\cos a}
      | c = Sine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \cos A
      | r = -\cos B \cos C + \sin B \sin C \cos a
      | c = simplifying and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Spherical Law of Tangents

:$\dfrac {\tan \frac 1 2 \paren {A + B} } {\tan \frac 1 2 \paren {A - B} } = \dfrac {\tan \frac 1 2 \paren {a + b} } {\tan \frac 1 2 \paren {a - b} }$

Proof:
{{begin-eqn}}
{{eqn | l = \tan \dfrac {A + B} 2
      | r = \dfrac {\cos \frac {a - b} 2} {\cos \frac {a + b} 2} \cot \dfrac C 2
      | c = Napier's Analogies
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \tan \frac {A + B} 2 \cos \frac {a + b} 2
      | r = \cos \frac {a - b} 2 \cot \frac C 2
      | c = more manageable in this form
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \tan \dfrac {A - B} 2
      | r = \dfrac {\sin \frac {a - b} 2} {\sin \frac {a + b} 2} \cot \dfrac C 2
      | c = Napier's Analogies
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \tan \frac {A - B} 2 \sin \frac {a + b} 2
      | r = \sin \frac {a - b} 2 \cot \frac C 2
      | c = more manageable in this form
}}
{{end-eqn}}
Hence we have:
{{begin-eqn}}
{{eqn | l = \dfrac {\tan \frac {A + B} 2 \cos \frac {a + b} 2} {\tan \frac {A - B} 2 \sin \frac {a + b} 2}
      | r = \dfrac {\cos \frac {a - b} 2 \cot \frac C 2} {\sin \frac {a - b} 2 \cot \frac C 2}
      | c = dividing $(1)$ by $(2)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\tan \frac {A + B} 2} {\tan \frac {A - B} 2} \dfrac 1 {\tan \frac {a + b} 2}
      | r = \dfrac 1 {\tan \frac {a - b} 2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\tan \frac {A + B} 2} {\tan \frac {A - B} 2}
      | r = \dfrac {\tan \frac {a + b} 2} {\tan \frac {a - b} 2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Half Angle for Spherical Triangles

:$\cos \dfrac A 2 = \sqrt {\dfrac {\sin s \, \map \sin {s - a} } {\sin b \sin c} }$
where $s = \dfrac {a + b + c} 2$.

Proof:
{{begin-eqn}}
{{eqn | l = \cos a
      | r = \cos b \cos c + \sin b \sin c \cos A
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos b \cos c + \sin b \sin c \paren {2 \cos^2 \dfrac A 2 - 1}
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | r = \map \cos {b + c} + 2 \sin b \sin c \cos^2 \dfrac A 2
      | c = Cosine of Sum
}}
{{eqn | ll= \leadsto
      | l = \cos a - \map \cos {b + c}
      | r = 2 \sin b \sin c \cos^2 \dfrac A 2
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = 2 \sin \dfrac {a + \paren {b + c} } 2 \sin \dfrac {\paren {b + c} - a} 2
      | r = 2 \sin b \sin c \cos^2 \dfrac A 2
      | c = Cosine minus Cosine
}}
{{eqn | ll= \leadsto
      | l = \map \sin {\dfrac {a + b + c} 2} \map \sin {\dfrac {a + b + c} 2 - a}
      | r = \sin b \sin c \cos^2 \dfrac A 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin s \, \map \sin {s - a}
      | r = \sin b \sin c \cos^2 \dfrac A 2
      | c = setting $s = \dfrac {a + b + c} 2$ and simplifying
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Cosine of Half Side for Spherical Triangles

:$\cos \dfrac a 2 = \sqrt {\dfrac {\map \cos {S - B} \, \map \cos {S - C} } {\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 = \sin \dfrac {A'} 2
      | r = \sqrt {\dfrac {\sin \paren {s' - b'} \sin \paren {s' - c'} } {\sin b' \sin c'} }
      | c = Sine of Half Angle for Spherical Triangles
}}
{{eqn | ll= \leadsto
      | l = \sin \dfrac {\pi - a} 2
      | r = \sqrt {\dfrac {\map \sin {s' - b'}  \, \map \sin {s' - c'} } {\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 \sin {\dfrac \pi 2 - \dfrac a 2}
      | r = \sqrt {\dfrac {\map \sin {s' - b'}  \, \map \sin {s' - c'} } {\sin B \sin C} }
      | c = Sine of Supplementary Angle
}}
{{eqn | ll= \leadsto
      | l = \cos \dfrac a 2
      | r = \sqrt {\dfrac {\map \sin {s' - b'}  \, \map \sin {s' - c'} } {\sin B \sin C} }
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = s' - b'
      | r = \dfrac {\paren {\pi - A} + \paren {\pi - B} + \paren {\pi - C} } 2 - \paren {\pi - B}
      | c = Side of Spherical Triangle is Supplement of Angle of Polar Triangle 
}}
{{eqn | r = \dfrac {\pi - \paren {A + B + C} } 2 + B
      | c = simplifying
}}
{{eqn | r = \dfrac \pi 2 - \paren {S - B}
      | c = where $S = \dfrac {A + B + C} 2$
}}
{{eqn | ll= \leadsto
      | l = \map \sin {s' - b'}
      | r = \map \sin {\dfrac \pi 2 - \paren {S - B} }
      | c = 
}}
{{eqn | r = \map \cos {S - B}
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
and similarly:
:$\map \sin {s' - c'} = \map \cos {S - C}$
The result follows.
{{qed}}
Theorem: Equation of Circle/Polar

:$r^2 - 2 r r_0 \map \cos {\theta - \varphi} + \paren {r_0}^2 = R^2$

Proof:
Let the point $\polar {r, \theta}_\text {Polar}$ satisfy the equation:
:$r^2 - 2 r r_0 \map \cos {\theta - \varphi} + \paren {r_0}^2 = R^2$
Let the points $\polar {r, \theta}$ and $\polar {r_0, \varphi}$ be rewritten in Cartesian coordinates:
:$\polar {r, \theta}_\text {Polar} = \tuple {r \cos \theta, r \sin \theta}_\text{Cartesian}$
:$\polar {r_0, \varphi}_\text{Polar} = \tuple {r_0 \cos \varphi, r_0 \sin \varphi}_\text{Cartesian}$
Thus the distance between $\polar {r, \theta}_\text {Polar}$ and $\polar {r_0, \varphi}_\text{Polar}$ is:
{{begin-eqn}}
{{eqn | o = 
      | r = \sqrt {\paren {r \cos \theta - r_0 \cos \varphi}^2 + \paren {r \sin \theta - r_0 \sin \varphi}^2}
}}
{{eqn | r = \sqrt {r^2 \cos^2 \theta + \paren {r_0}^2 \cos^2 \varphi - 2 r r_0 \cos \theta \cos \varphi + r^2 \sin^2 \theta + \paren {r_0}^2 \sin^2 \varphi - 2 r r_0 \sin \theta \sin \varphi}
}}
{{eqn | r = \sqrt {r^2 \paren {\cos^2 \theta + \sin^2 \theta} + \paren {r_0}^2 \paren {\cos^2 \varphi + \sin^2 \varphi} - 2 r r_0 \paren {\cos \theta \cos \varphi + \sin \theta \sin \varphi} }
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | r = \sqrt {r^2 + \paren {r_0}^2 - 2 r r_0 \map \cos {\theta - \varphi} }
      | c = Cosine of Difference and Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
But from the equation, this quantity equals $R$.
Therefore the distance between points satisfying the equation and the center is constant and equal to the radius $R$.
{{qed}}
Category:Equation of Circle
j0cy3bs58hyb5fplxgmhgdktgr7knlj
Theorem: Equation of Circle/Cartesian/Formulation 2

The equation:
:$A \paren {x^2 + y^2} + B x + C y + D = 0$
is the equation of a circle with radius $R$ and center $\tuple {a, b}$, where:
:$R = \dfrac 1 {2 A} \sqrt {B^2 + C^2 - 4 A D}$
:$\tuple {a, b} = \tuple {\dfrac {-B} {2 A}, \dfrac {-C} {2 A} }$
provided:
:$A > 0$
:$B^2 + C^2 \ge 4 A D$

Proof:
{{begin-eqn}}
{{eqn | l = A \paren {x^2 + y^2} + B x + C y + D
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x^2 + y^2 + \frac B A x + \frac C A y 
      | r = - \frac D A
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x^2 + 2 \frac B {2 A} x + \frac {B^2} {4 A^2} + y^2 + 2 \frac C {2 A} y + \frac {C^2} {4 A^2}
      | r = \frac {B^2} {4 A^2} + \frac {C^2} {4 A^2} - \frac D A
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {x + \frac B {2 A} }^2 + \paren {y + \frac C {2 A} }^2
      | r = \frac {B^2} {4 A^2} + \frac {C^2} {4 A^2} - \frac D A
      | c = 
}}
{{eqn | r = \frac {B^2} {4 A^2} + \frac {C^2} {4 A^2} - \frac {4 A D} {4 A^2}
      | c = 
}}
{{eqn | r = \frac 1 {4 A^2} \paren {B^2 + C^2 - 4 A D}
      | c = 
}}
{{end-eqn}}
This last expression is non-negative {{iff}} $B^2 + C^2 \ge 4 A D$.
In such a case $\dfrac 1 {4 A^2} \paren {B^2 + C^2 - 4 A D}$ is in the form $R^2$ and so:
:$\paren {x + \dfrac B {2 A} }^2 + \paren {y + \dfrac C {2 A} }^2 = \dfrac 1 {4 A^2} \paren {B^2 + C^2 - 4 A D}$
is in the form:
:$\paren {x - a}^2 + \paren {y - b}^2 = R^2$
Hence the result from Equation of Circle in Cartesian Plane: Formulation 1.
{{qed}}
Category:Equation of Circle
kkgm4b7qm44vpk0ukd31g50gqjfu6iv
Theorem: Equation of Circle center Origin

The circle with radius $R$ whose center is at the origin expressed in Cartesian coordinates is given by the equation:
:$x^2 + y^2 = R^2$

Proof:
From Equation of Circle in Cartesian Plane, the equation of a circle with radius $R$ and center $\tuple {a, b}$ expressed in Cartesian coordinates is:
:$\paren {x - a}^2 + \paren {y - b}^2 = R^2$
Setting $a = b = 0$ yields the result.
{{qed}}
Theorem: Distance Formula/3 Dimensions

The distance $d$ between two points $A = \tuple {x_1, y_1, z_1}$ and $B = \tuple {x_2, y_2, z_2}$ in a Cartesian space of 3 dimensions is:
:$d = \sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2 + \paren {z_1 - z_2}^2}$

Proof:
:600px
Let $d$ be the distance to be found between $A = \tuple {x_1, y_1, z_1}$ and $B = \tuple {x_2, y_2, z_2}$.
Let the points $C$ and $D$ be defined as:
:$C = \tuple {x_2, y_1, z_1}$
:$D = \tuple {x_2, y_2, z_1}$
Let $d'$ be the distance between $A$ and $D$.
From Distance Formula, it can be seen that:
:$d' = \sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2}$
We note that $\triangle ADB$ is a right triangle.
Thus by Pythagoras's Theorem:
:$AB^2 = AD^2 + DB^2$
Thus:
{{begin-eqn}}
{{eqn | l = d^2
      | r = d'^2 + DB^2
      | c = 
}}
{{eqn | r = \paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2 + \paren {z_1 - z_2}^2
      | c = 
}}
{{end-eqn}}
and so:
:$d = \sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2 + \paren {z_1 - z_2}^2}$
as it was to be proved.
{{qed}}
Theorem: Equation of Sphere/Rectangular Coordinates

:$\paren {x - a}^2 + \paren {y - b}^2 + \paren {z - c}^2 = R^2$

Proof:
Let the point $\tuple {x, y, z}$ satisfy the equation:
:$(1): \quad \paren {x - a}^2 + \paren {y - b}^2 + \paren {z - c}^2 = R^2$
By the Distance Formula in 3 Dimensions, the distance between this $\tuple {x, y, z}$ and $\tuple {a, b, c}$ is:
:$\sqrt {\paren {x - a}^2 + \paren {y - b}^2 + \paren {z - c}^2}$
But from equation $(1)$, this quantity equals $R$.
Therefore the distance between points satisfying the equation and the center is constant and equal to the radius.
Thus $\tuple {x, y, z}$ lies on the surface of a sphere with radius $R$ and center $\tuple {a, b, c}$.
Now suppose that $\tuple {x, y, z}$ does not satisfy the equation:
:$\paren {x - a}^2 + \paren {y - b}^2 + \paren {z - c}^2 = R^2$
Then by the same reasoning as above, the distance between $\tuple {x, y, z}$ and $\tuple {a, b, c}$ does not equal $R$.
Therefore $\tuple {x, y, z}$ does not lie on the surface of a sphere with radius $R$ and center $\tuple {a, b, c}$.
Hence it follows that the points satisfying $(1)$ are exactly those points which are the sphere in question.
{{qed}}
Theorem: Equation of Sphere/Rectangular Coordinates/Corollary

The equation of a sphere with radius $R$ whose center is at the origin expressed in Cartesian coordinates is:
:$x^2 + y^2 + z^2 = R^2$

Proof:
From Equation of Sphere in Rectangular Coordinates, the equation of a sphere with radius $R$ and center $\tuple {a, b, c}$ expressed in Cartesian coordinates is:
:$\paren {x - a}^2 + \paren {y - b}^2 + \paren {z - c}^2 = R^2$
Setting $a = b = c = 0$ yields the result.
{{qed}}