avewright/proofwiki-math huggingface dataset:
Theorem: Absolute Value Function is Continuous

Let $f$ be the real function defined as:
:$\forall x \in \R: \map f x = \size x$
where $\size x$ denotes the absolute value of $x$.
Then $f$ is a continuous real function.

Proof:
Let $a \in \R$.
Let $\epsilon \in \R_{\mathop > 0}$.
Let $\delta \le \epsilon$.
We have:
{{begin-eqn}}
{{eqn | q = \forall x \in \R : \size{x - a} < \delta
      | l = \size{\map f x - \map f a}
      | r = \bigsize {\size x - \size a}
      | c = Definition of $f$
}}
{{eqn | o = \le
      | r = \size {x - a}
      | c = Reverse Triangle Inequality on Real Numbers
}}
{{eqn | o = <
      | r = \delta
      | c = {{hypothesis}}
}}
{{eqn | o = \le
      | r = \epsilon
      | c = {{hypothesis}}
}}
{{end-eqn}}
Since $\epsilon$ was arbitrary, it follows that $f$ is continuous at $a$ by definition.
Since $a$ was arbitrary, it follows that $f$ is continuous everywhere by definition.
{{qed}}
Category:Absolute Value Function
Category:Continuous Real Functions
9pdn55iz6q221r3uyh37iymbikzfyui
Theorem: Pointwise Difference is Pointwise Addition with Negation

Let $S$ be a set.
Let $\R$ denote the real number line.
Let $f, g :S \to \R$ be real-valued functions.
Let $f - g$ denote the pointwise difference of $f$ and $g$, that is, $f - g$ is the mapping defined by:
:$\forall s \in S : \map {\paren{f - g} } s = \map f s - \map g s$
Then:
:$f - g = f + \paren{-g}$
where:
:$-g$ denotes the pointwise negation of $g$
:$f + \paren{-g}$ denotes the pointwise addition of $f$ and $-g$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \map {\paren{f - g} } s
      | r = \map f s - \map g s
      | c = {{Defof|Pointwise Difference of Real-Valued Functions}}
}}
{{eqn | r = \map f s + \paren{- \map g s}
}}
{{eqn | r = \map f s + \map {\paren{-g} } s
      | c = {{Defof|Pointwise Negation of Real-Valued Function}}
}}
{{eqn | r = \map {\paren{f + \paren{-g} } } s
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{end-eqn}}
By definition of equality of mappings:
:$f - g = f + \paren{-g}$
{{qed}}
Category:Real-Valued Functions
8nv8cgwr75pz0r2q2ejnr9hyjevusag
Theorem: Absolute Value of Function is Composite with Absolute Value Function

Let $S$ be a set.
Let $\R$ denote the real number line.
Let $f: S \to \R$ be real-valued function.
Let $\size f$ denote the absolute value of $f$, that is, $\size f$ is the mapping defined by:
:$\forall s \in S : \map {\size f} s = \size{\map f s}$
Then:
:$\size f = \size{\,\cdot\,} \circ f$
where:
:$\size{\,\cdot\,} : \R \to \R$ denotes the absoute value function
:$\size{\,\cdot\,} \circ f$ denotes the composite mapping of $\size{\,\cdot\,}$ and $f$

Proof:
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \map {\size f } s
      | r = \size{\map f s}
      | c = {{Defof|Absolute Value of Real-Valued Function}}
}}
{{eqn | r = \map {\paren{\size{\,\cdot\,} \circ f} } s
      | c = {{Defof|Composite Mapping}}
}}
{{end-eqn}}
By definition of equality of mappings:
:$\size f = \size{\,\cdot\,} \circ f$
{{qed}}
Category:Real-Valued Functions
bh1u45vhlcrngwfllw5cggjnvnhfqxx
Theorem: Combination Theorem for Bounded Real-Valued Functions/Difference Rule

:$f - g$ is a bounded real-valued function

Proof:
From Pointwise Difference is Pointwise Addition with Negation:
:$f - g = f + \paren{-g}$
where:
:$-g$ denotes the pointwise negation of $g$
:$f + \paren{-g}$ denotes the pointwise addition of $f$ and $-g$
From Negation Rule for Bounded Real-Valued Function:
:$-g$ is a bounded real-valued function
From Sum Rule for Bounded Real-Valued Functions
:$f + \paren{-g}$ is a bounded real-valued function
The result follows.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
2s2ga929nl7vyowjr1lkvh4gt5ezo84
Theorem: Combination Theorem for Bounded Real-Valued Functions/Multiple Rule

:$\lambda f$ is a bounded real-valued function

Proof:
By definition of bounded real-valued function
:$\exists M_f \in \R_{\ge 0} : \forall s \in S : \size{\map f s} \le M_f$
Let $M = \size{\lambda} M_f$.
We have:
{{begin-eqn}}
{{eqn | q = \forall s \in S
      | l = \size{\map {\paren{\lambda f} } s}
      | r = \size{\lambda \map f s}
      | c = {{Defof|Pointwise Scalar Multiplication of Real-Valued Function}}
}}
{{eqn | r = \size{\lambda} \size{\map f s}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le
      | r = \size{\lambda} M_f
      | c = {{Defof|Bounded Real-Valued Function}}
}}
{{eqn | r = M
      | c = definition of $M$
}}
{{end-eqn}}
It follows that $\lambda f$ is a bounded real-valued function by definition.
{{qed}}
Category:Combination Theorem for Bounded Real-Valued Functions
0xrwg36h3cgue0myaq71gzcfvxmu8za
Theorem: Inverse of a Line Through Circle Center is a Line

Let $C$ be a circle in the plane on center $O$.
Let the radius of $C$ be $r$.
Let $L$ be an arbitrary ray through $O$.
Let $P$ be an otherwise arbitrary point, but lying on $L$.
Let $T : X \to Y$ be an inversive transformation with $C$ as the inversion circle. 
Then $O$ is the inversion center.
Then the image of $P$ under $T$ also lies on $L$.

Proof:
Let $P'$ be the image of $P$ under $T$, with $P \ne O$.
By the definition of inversion:
:$P'$ lies on $L$
We deal with $O$ separately.  By the definition of ray:
:$O$ lies on $L$
{{EuclidSaid}}
:''{{:Definition:Euclid's Definitions - Book I/1 - Point}}''
A point has no length, it has no magnitude.
So we cannot compute $\dfrac {r^2} {OO}$ to find $O'$, the image of $O$.
But by the definition of inversion, the image of $O$ is the point at infinity.
By the definition the point at infinity lies on ''every'' infinite half-line through $O$.
Hence $O$ lies on $L$.
Therefore the image under $T$ of every point on $L$ lies on $L$.
{{qed}}
Category:Inversive Geometry
mmze77pkp7jm1n6y1lpysdw07r4adqk
Theorem: Compound Distribution of Poisson Distributed Bernoulli Trials has Poisson Distribution

Let $N$ be a discrete random variable with a Poisson distribution with expectation $\lambda$.
Let $X_1, X_2, \ldots, X_N$ be pairwise independent discrete random variables each with a Bernoulli distribution with parameter $P$.
Let $S_N : X_1 + X_2 + \cdots + X_N$ be the resulting compound distribution.
Then $S_N$ has a Poisson distribution with expectation $\lambda p$.

Proof:
From the definition of Poisson distribution, we will show that:
:$\map \Pr {S_N = k} = \dfrac {\paren {\lambda p}^k e^{-\lambda p} } {k!}$
{{begin-eqn}}
{{eqn | l = \map \Pr {S_N = k}
      | r = \sum_{n \mathop = 0}^\infty \condprob {S_N = k} {N = n} \map \Pr {N = n}
      | c = Total Probability Theorem
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map \Pr {S_n = k} \map \Pr {N = n}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map \Pr {S_n = k} \frac {\lambda^n e^{-\lambda} } {n!}
      | c = {{Defof|Poisson Distribution}}
}}
{{eqn | r = \sum_{n \mathop = 0}^{k - 1} \map \Pr {S_n = k} \frac {\lambda^n e^{-\lambda} } {n!} + \sum_{n \mathop = k}^\infty \map \Pr {S_n = k} \frac {\lambda^n e^{-\lambda} } {n!}
}}
{{eqn | r = \sum_{n \mathop = k}^\infty \map \Pr {S_n = k} \frac {\lambda^n e^{-\lambda} } {n!}
      | c = support of random variable with binomial distribution is $\set {1, \dots, n}$
}}
{{eqn | r = \sum_{n \mathop = k}^\infty \binom n k p^k \paren {1 - p}^{n - k} \frac{\lambda^n e^{-\lambda} } {n!}
      | c = Binomial Experiment has Binomial Distribution
}}
{{eqn | r = \sum_{n \mathop = k}^\infty \frac {n!} {k! \paren {n - k} !} p^k \paren {1 - p}^{n-k} \frac {\lambda^n e^{-\lambda} } {n!}
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \frac {p^k e^{-\lambda} } {k!} \sum_{n \mathop = k}^\infty \frac {\lambda^n \paren {1 - p}^{n - k} } {\paren {n - k}!}
}}
{{eqn | r = \frac {p^k e^{-\lambda} } {k!} \sum_{n \mathop = 0}^\infty \frac {\lambda^{n + k} \paren {1 - p}^n} {n!}
      | c = Translation of Index Variable of Summation on Infinite Series
}}
{{eqn | r = \frac {\lambda^k p^k e^{-\lambda} } {k!} \sum_{n \mathop = 0}^\infty \frac {\lambda^n \paren {1 - p}^n} {n!}
}}
{{eqn | r = \frac {\lambda^k p^k e^{-\lambda} } {k!}  \sum_{n \mathop = 0}^\infty \frac {\paren {\lambda - \lambda p}^n} {n!}
}}
{{eqn | r = \frac {\lambda^k p^k e^{-\lambda} } {k!} e^{\lambda - \lambda p}
      | c = Power Series Expansion for Exponential Function
}}
{{eqn | r = \frac {\paren {\lambda p}^k e^{-\lambda p} } k
      | c = Sum of Indices of Real Number
}}
{{end-eqn}}
{{qed}}
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Difference Rule

:$f - g$ is a bounded coninuous real-valued function

Proof:
Follows from:
* Difference Rule for Bounded Real-Valued Functions
* Difference Rule for Continuous Real-Valued Functions
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
pjw75utujkv5upyi413ly1vowj1zogq
Theorem: Combination Theorem for Bounded Continuous Real-Valued Functions/Multiple Rule

:$\lambda f$ is a bounded continuous real-valued function

Proof:
Follows from:
* Multiple Rule for Bounded Real-Valued Function
* Multiple Rule for Continuous Real-Valued Function
{{qed}}
Category:Combination Theorem for Bounded Continuous Real-Valued Functions
gq7dnvedl3zmj7rwtz6s7efdhhtdqny
Theorem: Slope of Parabola at Point

Let $a$ be a constant.
Let $T$ be the parabola which is the locus of points $\tuple {x, y}$ satisfying $y = a x^2$.
The slope of the tangent to $y = a x^2$ at $x = c$ is $2 a c$.

Proof:
By Derivative of Power of Function the derivative of $y = ax^2$ is:
:$\dfrac {\d y} {\d x} = 2 a x$
So the derivative of $y = a x^2$ at $x = c$ is $2 a c$.
The result follows from Slope of Tangent to Curve at Point equals Value of Derivative.
{{qed}}
Category:Parabolas
Category:Slope
n07nttxq0l26gdhy3rudjio4vj8g5a0
Theorem: Additive Inverse in Ring of Continuous Mappings

Let $\struct {S, \tau_{_S} }$ be a topological space.
Let $\struct {R, +, *, \tau_{_R} }$ be a topological ring with zero $0_R$.
Let $\struct{\map C {S, R}, +, *}$ be the ring of continuous mappings from $S$ to $R$.
Let $f \in \map C {S, R}$.
Then:
:the additive inverse of $f$ is the pointwise negation $-f$ defined by:
::$\forall s \in S : \map {\paren{-f}} s = - \map f s$

Proof:
Let $\struct {R^S, +, *}$ be the ring of mappings from $S$ to $R$.
From Ring of Continuous Mappings is Subring of All Mappings:
:$\struct{\map C {S, R}, +, *}$ is a subring of $\struct {R^S, +, *}$
From Structure Induced by Ring Operations is Ring:
:$\forall f \in R^S :$ the additive inverse of $f$ is the pointwise negation $-f$, defined by:
::$\forall s \in S: \map {\paren {-f} } s := - \map f s$
The result follows.
{{qed}}
Theorem: Additive Inverse in Ring of Continuous Real-Valued Functions

Let $\struct {S, \tau}$ be a topological space.
Let $\R$ denote the real number line.
Let $\struct {\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
Let $f \in \map C {S, \R}$.
Then:
:the additive inverse of $f$ is the pointwise negation $-f$ defined by:
::$\forall s \in S : \map {-f} s = - \map f s$

Proof:
By definition of ring of continuous real-valued functions:
:$\struct {\map C {S, \R}, +, *}$ is the ring of continuous mappings from $S$ to $\R$.
From Additive Inverse in Ring of Continuous Mappings:
:$\forall f \in \map C {S, \R} :$ the additive inverse of $f$ is the pointwise negation $-f$, defined by:
::$\forall s \in S: \map {\paren {-f} } s := - \map f s$
The result follows.
{{qed}}
Theorem: Additive Inverse in Ring of Bounded Continuous Real-Valued Functions

Let $\struct {S, \tau}$ be a topological space.
Let $\R$ denote the real number line.
Let $\struct {\map {C^*} {S, \R}, +, *}$ be the ring of bounded continuous real-valued functions from $S$.
Let $f \in \map {C^*} {S, \R}$.
Then:
:the additive inverse of $f$ is the pointwise negation $-f$ defined by:
::$\forall s \in S : \map {\paren{-f}} s = - \map f s$

Proof:
Let $\struct{\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
From Ring of Bounded Continuous Functions is Subring of Continuous Real-Valued Functions:
:$\struct{\map {C^*} {S, \R}, +, *}$ is a subring of $\struct{\map C {S, \R}, +, *}$
From Additive Inverse in Ring of Continuous Real-Valued Functions:
:the additive inverse of $f$ in $\struct{\map C {S, \R}, +, *}$ is the pointwise negation $-f$ defined by:
::$\forall s \in S : \map {\paren{-f}} s = - \map f s$
From Inverses in Subgroup:
:$-f$ is the additive inverse of $f$
{{qed}}
Theorem: Broken Chord Theorem

:300px
Let $A$ and $C$ be arbitrary points on a circle in the plane.
Let $M$ be a point on the circle with arc $AM = $ arc $MC$.
Let $B$ lie on the minor arc of $AM$.
Draw chords $AB$ and $BC$.
Find $D$ such that $MD \perp BC$.
Then:
:$AB + BD = DC$

Proof:
:300px
Let $E$ be a point such that $BD = DE$.
Given:
:arc $AM = $ arc $MC$
By Equal Arcs of Circles Subtended by Equal Straight Lines:
:$AM = MC$
By Angles on Equal Arcs are Equal:
:$\angle BAM = \angle MCB$
:$BM$ is shared
We have Ambiguous Case for Triangle Side-Side-Angle Congruence for these three triangles:
* $\triangle BAM$
* $\triangle MBC$
* $\triangle MEC$
Given:
:$\angle MDC$ is a right angle
By External Angle of Triangle is Greater than Internal Opposite:
:$\angle MEC$ is obtuse.
Since $AM = MC$ and $AC$ is the rest of the circumference:
:the major arc of $AM$ is more than half the circle.
It follows that $\angle ABM$ is obtuse.
{{begin-eqn}}
{{eqn | ll = \leadsto
      | l = \triangle ABM
      | o = \cong
      | r = \triangle MEC
      | c =
}}
{{eqn | ll = \leadsto
      | l = AB
      | r = EC
      | c =
}}
{{eqn | l = AB + BD
      | r = DE + EC = DC
      | c = addition
}}
{{end-eqn}}
{{qed}}
Theorem: Broken Chord Theorem

:300px
Let $A$ and $C$ be arbitrary points on a circle in the plane.
Let $M$ be a point on the circle with arc $AM = $ arc $MC$.
Let $B$ lie on the minor arc of $AM$.
Draw chords $AB$ and $BC$.
Find $D$ such that $MD \perp BC$.
Then:
:$AB + BD = DC$

Proof:
Find $E$ on $BC$ such that $BD = BE$.
400px
{{begin-eqn}} 
{{eqn | l = BD
      | r = ED
      | c = {{hypothesis}}
}}
{{eqn | l = MD 
      | o = \perp
      | r = BE
      | c = {{hypothesis}}
}}
{{eqn | l = \triangle MBD
      | o = \cong
      | r = \triangle MED
      | c = Triangle Side-Angle-Side Congruence
}}
{{eqn | ll= \leadsto
      | l = MB
      | r = ME
      | c = congruence
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \angle MBE
      | r = \angle MEB
      | c = Isosceles Triangle has Two Equal Angles
}}
{{eqn | l = \text {arc $AM$}
      | r = \text {arc $MC$}
      | c = {{hypothesis}}
}}
{{eqn | l = \angle MFC
      | r = \angle MBC
      | c = Angles on Equal Arcs are Equal
}}
{{eqn | l = \angle AFM
      | r = \angle MBC
      | c = Angles on Equal Arcs are Equal
}}
{{eqn | l = \angle MEB
      | r = \angle CEF
      | c = Vertical Angle Theorem
}}
{{end-eqn}}
Thus we have five equal angles:
:$\angle MBE$
:$\angle MEB$
:$\angle AFM$
:$\angle MFC$
:$\angle CEF$
By Triangle with Two Equal Angles is Isosceles:
:$\triangle CEF$ is isosceles
By definition of isosceles:
:$CE = CF$
Since $\angle AFM = \angle CEF$:
:$\angle AFC + \angle ECF =$ two right angles.
{{begin-eqn}}
{{eqn | l = BC
      | o = \parallel
      | r = AF
      | c = Supplementary Interior Angles implies Parallel Lines
}}
{{eqn | l = AB
      | r = CF
      | c = Parallel Chords Cut Equal Chords in a Circle
}}
{{eqn | l = AB
      | r = CE
      | c = {{EuclidCommonNotionLink|1}}
}}
{{eqn | l = AB + BD
      | r = DE + EC
      | c = {{EuclidCommonNotionLink|2}}
}}
{{eqn | l = AB + BD
      | r = DC
      | c = Addition
}}
{{end-eqn}}
{{qed}}
Theorem: Broken Chord Theorem

:300px
Let $A$ and $C$ be arbitrary points on a circle in the plane.
Let $M$ be a point on the circle with arc $AM = $ arc $MC$.
Let $B$ lie on the minor arc of $AM$.
Draw chords $AB$ and $BC$.
Find $D$ such that $MD \perp BC$.
Then:
:$AB + BD = DC$

Proof:
300px
Given $MD \perp BC$
Draw $MN \parallel BC$ to meet the circle at $N$.
Draw $NE \parallel MD$.
By Quadrilateral is Parallelogram iff Both Pairs of Opposite Sides are Equal or Parallel:
:$MNED$ is a parallelogram
By Parallelogram with One Right Angle is Rectangle:
:$MNED$ is a rectangle.
{{begin-eqn}}
{{eqn | l = DE
      | r = MN
      | c = {{Defof|Rectangle}}
}}
{{eqn | l = MD
      | r = NE
      | c = {{Defof|Rectangle}}
}}
{{end-eqn}}
By Parallelism implies Equal Corresponding Angles:
:$\angle MDB = \angle NEC$
and both are right angles.
{{begin-eqn}}
{{eqn | l = BM
      | r = NC
      | c = Parallel Chords Cut Equal Chords in a Circle
}}
{{eqn | l = \triangle MDB
      | o = \cong
      | r = \triangle NEC
      | c = Triangle Side-Side-Side Congruence
}}
{{eqn | ll= \leadsto
      | l = BD
      | r = EC
      | c =
}}
{{eqn | l = \text {arc $BM$}
      | r = \text {arc $NC$}
      | c = Equal Arcs of Circles Subtended by Equal Straight Lines
}}
{{eqn | l = \text {arc $AM$}
      | r = \text {arc $MC$}
      | c = {{hypothesis}}
}}
{{eqn | l = \text {arc $AB$}
      | r = \text {arc $MN$}
      | c = {{EuclidCommonNotionLink|3}}
}}
{{eqn | l = AB
      | r = MN
      | c = Equal Arcs of Circles Subtended by Equal Straight Lines
}}
{{eqn | l = AB
      | r = DE
      | c = {{EuclidCommonNotionLink|1}}
}}
{{eqn | l = AB + BC
      | r = DE + EC
      | c = {{EuclidCommonNotionLink|2}}
}}
{{eqn | l = AB + BC
      | r = DE
      | c = addition
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Inverse of Circle Through Inversion Center is Straight Line Not Through Inversion Center

Let an arbitrary circle $K$ be drawn in the plane.
Let $A'$ and $P'$ be arbitrary points on $K$.
Let $T$ be an inversive transformation such that:
:the inversion center of $T$ is $O$
:the inversion circle $O$ for $T$ is chosen such that $OA'$ is a diameter of $K$
:the radius of $O$ is $r$.
Let $A$ and $P$ be the images of $A'$ and $P'$ under $T$ respectively.
Let $L$ be a straight line drawn perpendicular to the extension of $OA'$ at point $A$.
Then $P$ lies on $L$.

Proof:
The diagrams show the two cases:
:$K$ completely inside the circle on $O$
300px
:or with some points outside
300px
The proof is the same for both cases.
{{begin-eqn}}
{{eqn | l = OP \cdot OP'
      | r = OA \cdot OA'
      | c = definition of $T$
}}
{{eqn | ll= \leadsto
      | l = \dfrac {OP} {OA}
      | r = \dfrac {OA'} {OP'}
      | c = rearranging
}}
{{end-eqn}}
$\angle AOP$ is shared.
{{begin-eqn}}
{{eqn | l = \triangle OAP
      | o = \sim
      | r = \triangle OP'A'
      | c = Triangles with One Equal Angle and Two Sides Proportional are Similar
}}
{{eqn | ll= \leadsto
      | l = \angle OAP
      | r = 90 \degrees
      | c = {{Defof|Perpendicular}}
}}
{{end-eqn}}
By Perpendicular from Point to Straight Line in Plane is Unique:
:there is only one straight line perpendicular to a straight line at a given point.
So:
:$AP$ is the same straight line as $L$
That is, $P$ lies on $L$.
$P$ is the image under $T$ of an arbitrary point $P'$ on $K$, and $P$ lies on $L$.
{{qed}}
Theorem: Inverse of Straight Line Not Through Inversion Center is Circle Through Inversion Center

Let $C$ be a circle on center $O$ in the plane.
Let $T : X \to Y$ be an inversive transformation with $C$ as the inversion circle. 
Then $O$ is the inversion center.
Let $L$ be an arbitrary straight line not containing $O$.
Let $P$ be an arbitrary point on $L$.
Let $P'$ be the image of $P$ under $T$.
Then $P'$ lies on a circle through $O$.

Proof:
By Inverse of Circle Through Inversion Center is Straight Line Not Through Inversion Center:
:the image under $T$ of a circle through $C$ is a straight line not through $C$.
By definition of inversive transformation, $T$ is an involution.
Thus, the image under $T$ of a straight line not through $C$ is a circle through $C$.
{{qed}}
Theorem: Ring of Bounded Continuous Functions is Ring of Continuous Functions for Compact Space

Let $\struct {K, \tau}$ be a compact space.
Let $\R$ denote the real number line.
Let $\struct {\map C {S, \R}, +, *}$ be the ring of continuous real-valued functions from $S$.
Let $\struct {\map {C^*} {S, \R}, +, *}$ be the ring of bounded continuous real-valued functions from $S$.
Then:
:$\struct {\map {C^*} {S, \R}, +, *} = \struct {\map C {S, \R}, +, *}$

Proof:
Follows immediately from:
* Compact Space is Pseudocompact Space
* Ring of Bounded Continuous Functions is Ring of Continuous Functions for Pseudocompact Space
{{qed}}
Theorem: Inverse of Circle Not Through Inversion Center

Let $\CC$ be a circle in the plane on center $O$.
Let $T : X \to Y$ be an inversive transformation with $\CC$ as the inversion circle. 
Then $O$ is the inversion center.
Let $K$ be an arbitrary circle distinct from $\CC$ and not through $O$.
Then the image under $T$ of all the points on $K$ lie on the same circle, distinct from both $K$ and $\CC$.

Proof:
Let $AB$ be the diameter of $K$, drawn so that $OAB$ are collinear points.
Let $A'$ and $B'$ be the image of $A$ and $B$ under $T$.
Let $K'$ be the circle with diameter $A'B'$
Let $C$ be an otherwise arbitrary point, lying on $K$.
:400px
{{begin-eqn}}
{{eqn | l = OA \cdot OA'
      | r = OB \cdot OB' = OC \cdot OC'
      | c = Definition of $T$
}}
{{eqn | l = OA : OC
      | r = OC' : OA'
      | c = rearranging
}}
{{eqn | l = \angle BOC
      | r = \angle BOC
      | c = shared
}}
{{eqn | l = \triangle OA'C'
      | o = \sim
      | r = \triangle OCA
      | c = Triangles with One Equal Angle and Two Sides Proportional are Similar
}}
{{eqn | ll = \leadsto
      | l = \angle OA'C'
      | r = \angle OCA = \alpha
      | c =
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = OB : OC
      | r = OC' : OB'
      | c = rearranging
}}
{{eqn | l = \triangle OC'B'
      | o = \sim
      | r = \triangle OBC
      | c = Triangles with One Equal Angle and Two Sides Proportional are Similar
}}
{{eqn | ll = \leadsto
      | l = \angle OC'B'
      | r = \angle OBC = \beta
      | c =
}}
{{eqn | ll = \leadsto
      | l = \gamma
      | r = \angle OCB
      | c =
}}
{{eqn | l = \gamma
      | r = \alpha + \angle ACB
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \angle ACB
      | r = 90^{\circ}
      | c = Thales' Theorem
}}
{{eqn | l = \gamma
      | r = \alpha + \angle A'C'B'
      | c = External Angle of Triangle equals Sum of other Internal Angles
}}
{{eqn | l = \alpha + \angle A'C'B'
      | r = \alpha + \angle ACB
      | c = {{EuclidCommonNotionLink|1}}
}}
{{eqn | l = \angle A'C'B'
      | r = \angle ACB
      | c = {{EuclidCommonNotionLink|3}}
}}
{{eqn | ll = \leadsto
      | l = \angle A'C'B'
      | r = 90^{\circ}
      | c = {{EuclidCommonNotionLink|1}}
}}
{{end-eqn}}
By converse to Thales' Theorem:
:$C'$ is on circle with diameter $A'B'$
We note two other arrangements both covered by this proof.
* $K$ outside and tangent to $\CC$
* $K$ cuts $\CC$ but not through $O$
The third possibility is simply the inverse of an inversive transformation.
* $K$ inside $\CC$ and not through $O$
But this follows, since $T$ is an involution
{{qed}}