avewright/proofwiki-math huggingface dataset:
Theorem: Angle Bisectors are Harmonic Conjugates

Let $\LL_1$ and $\LL_2$ be straight lines which intersect at $O$.
Let $\LL_3$ and $\LL_4$ be the angle bisectors of the angles formed at the point of intersection of $\LL_1$ and $\LL_2$.
Then $\LL_3$ and $\LL_4$ are harmonic conjugates with respect to $\LL_1$ and $\LL_2$.

Proof:
Consider a straight line parallel to $\LL_4$ which intersects $\LL_1$, $\LL_2$ and $\LL_3$ at $L$, $M$ and $N$ respectively.
From Bisectors of Adjacent Angles between Straight Lines Meeting at Point are Perpendicular, $\LL_3$ is perpendicular to $\LL_4$.
Hence as $LM$ is parallel to $\LL_4$, $LM$ is perpendicular to $ON$, which is $\LL3$.
:440px
The triangle $\triangle OLM$ has:
:$\angle NOL = \angle NOM$
:$\angle ONL = \angle ONM$ as both are right angles
:$ON$ common
So $\triangle ONL$ and $\triangle ONM$ are congruent.
So $N$ is the midpoint of $LM$.
From Harmonic Range with Unity Ratio, the points $L$, $N$, $M$ and the point at infinity form a harmonic range.
Hence from Straight Line which cuts Harmonic Pencil forms Harmonic Range, the straight lines $\LL_1$, $\LL_2$, $\LL_3$ and $\LL_4$ form a harmonic pencil.
That is: $\LL_3$ and $\LL_4$ are harmonic conjugates with respect to $\LL_1$ and $\LL_2$.
{{qed}}
Theorem: Bisectors of Angles between Two Straight Lines/Homogeneous Quadratic Equation Form

Consider the homogeneous quadratic equation:
:$(1): \quad a x^2 + 2 h x y + b y^2 = 0$
representing two straight lines through the origin.
Then the homogeneous quadratic equation which represents the angle bisectors of the angles formed at their point of intersection is given by:
:$h x^2 - \paren {a - b} x y - h y^2 = 0$

Proof:
From Angle Bisectors are Harmonic Conjugates, the two angle bisectors are harmonic conjugates of the straight lines represented by $(1)$.
From Condition for Homogeneous Quadratic Equation to describe Perpendicular Straight Lines, these angle bisectors can be described by the homogeneous quadratic equation:
:$x^2 + 2 \lambda x y - y^2 = 0$
From Condition for Pairs of Lines through Origin to be Harmonic Conjugates: Homogeneous Quadratic Equation Form:
:$-a + b - 2 \lambda h = 0$
Hence:
:$\lambda = -\dfrac {a + b} {2 h}$
The result follows.
{{qed}}
Theorem: Equation of Tangent to Circle Centered at Origin

Let $\CC$ be a circle whose radius is $r$ and whose center is at the origin of a Cartesian plane.
Let $P = \tuple {x_1, y_1}$ be a point on $\CC$.
Let $\TT$ be a tangent to $\CC$ passing through $P$.
Then $\TT$ can be defined by the equation:
:$x x_1 + y y_1 = r^2$

Proof:
From Equation of Straight Line Tangent to Circle we have that for a general circle of radius $r$ and center $\tuple {a, b}$:
:$y - y_1 = \dfrac {a - x_1} {y_1 - b} \paren {x - x_1}$
is the equation of a tangent $\TT$ to $\CC$ passing through $\tuple {x_1, y_1}$.
Setting the center to $\tuple {0, 0}$:
{{begin-eqn}}
{{eqn | l = y - y_1
      | r = -\dfrac {x_1} {y_1} \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_1 \paren {y - y_1}
      | r = -x_1 \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x x_1 + y y_1
      | r = x_1^2 + y_1^2
      | c = 
}}
{{eqn | r = r^2
      | c = as $\tuple {x_1, y_1}$ is on $\CC$
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Tangent to Circle Centered at Origin

Let $\CC$ be a circle whose radius is $r$ and whose center is at the origin of a Cartesian plane.
Let $P = \tuple {x_1, y_1}$ be a point on $\CC$.
Let $\TT$ be a tangent to $\CC$ passing through $P$.
Then $\TT$ can be defined by the equation:
:$x x_1 + y y_1 = r^2$

Proof:
From the slope-intercept form of a line, the equation of a line passing through $P$ is:
:$y - y_1 = \mu \paren {x - x_1}$
If this line passes through another point $\tuple {x_2, y_2}$ on $\CC$, the slope of the line is given by:
:$\mu = \dfrac {y_2 - y_1} {x_2 - x_1}$
Because $P$ and $Q$ both lie on $\CC$, we have:
{{begin-eqn}}
{{eqn | l = x_1^2 + y_1^2
      | r = r^2 = x_2^2 + y_2^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_2^2 - y_1^2
      | r = x_2^2 - x_1^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {y_2 - y_1} {x_2 - x_1}
      | r = -\dfrac {x_1 + x_2} {y_1 + y_2}
      | c = 
}}
{{end-eqn}}
As $Q$ approaches $P$, we have that $y_2 \to y_1$ and $x_2 \to x_1$.
The limit of the slope is therefore:
:$-\dfrac {2 x_1} {2 y_1} = -\dfrac {x_1} {y_1}$
The equation of the tangent $\TT$ to $\CC$ passing through $\tuple {x_1, y_1}$ is therefore:
{{begin-eqn}}
{{eqn | l = y - y_1
      | r = -\dfrac {x_1} {y_1} \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_1 \paren {y - y_1}
      | r = -x_1 \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x x_1 + y y_1
      | r = x_1^2 + y_1^2
      | c = 
}}
{{eqn | r = r^2
      | c = as $\tuple {x_1, y_1}$ is on $\CC$
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Normal to Circle Centered at Origin

Let $\CC$ be a circle whose radius is $r$ and whose center is at the origin of a Cartesian plane.
Let $P = \tuple {x_1, y_1}$ be a point on $\CC$.
Let $\NN$ be a normal to $\CC$ passing through $P$.
Then $\NN$ can be defined by the equation:
:$y_1 x - x_1 y = 0$

Proof:
Let $\TT$ be the tangent to $\CC$ passing through $P$.
From Equation of Tangent to Circle Centered at Origin, $\TT$ can be described using the equation:
:$x x_1 + y y_1 = r^2$
expressible as:
:$y - y_1 = -\dfrac {x_1} {y_1} \paren {x - x_1}$
where the slope of $\TT$ is $-\dfrac {x_1} {y_1}$.
By definition, the normal is perpendicular to the tangent.
From Condition for Straight Lines in Plane to be Perpendicular, the slope of $\NN$ is $\dfrac {y_1} {x_1}$
Hence the equation for $\NN$ is:
{{begin-eqn}}
{{eqn | l = y - y_1
      | r = \dfrac {y_1} {x_1} \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1 \paren {y - y_1}
      | r = y_1 \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1 y 
      | r = y_1 x
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Normal to Circle passes through Center

A normal $\NN$ to a circle $\CC$ passes through the center of $\CC$.

Proof:
Let $\CC$ be positioned in a Cartesian plane with its center at the origin.
Let $\NN$ pass through the point $\tuple {x_1, y_1}$.
From Equation of Normal to Circle Centered at Origin, $\NN$ has the equation:
:$y_1 x - x_1 y = 0$
or:
:$y = \dfrac {y_1} {x_1} x$
From the Equation of Straight Line in Plane: Slope-Intercept Form, this is the equation of a straight line passing through the origin.
As the geometry of a circle is unchanged by a change of coordinate axes, the result follows for a general circle in whatever frame.
{{qed}}
Theorem: Equation of Chord of Contact on Circle Centered at Origin

Let $\CC$ be a circle whose radius is $r$ and whose center is at the origin of a Cartesian plane.
Let $P = \tuple {x_0, y_0}$ be a point which is outside the boundary of $\CC$.
Let $UV$ be the chord of contact on $\CC$ with respect to $P$.
Then $UV$ can be defined by the equation:
:$x x_0 + y y_0 = r^2$

Proof:
Let $\TT_1$ and $\TT_2$ be a tangents to $\CC$ passing through $P$.
Let:
:$\TT_1$ touch $\CC$ at $U = \tuple {x_1, y_1}$
:$\TT_2$ touch $\CC$ at $V = \tuple {x_2, y_2}$
Then the chord of contact on $\CC$ with respect to $P$ is defined as $UV$.
:480px
From Equation of Tangent to Circle Centered at Origin, $\TT_1$ is expressed by the equation:
:$x x_1 + y y_1 = r^2$
but as $\TT_1$ also passes through $\tuple {x_0, y_0}$ we also have:
:$x_0 x_1 + y_0 y_1 = r^2$
This also expresses the condition that $U$ should lie on $\TT_1$:
:$x x_0 + y y_0 = r^2$
Similarly, From Equation of Tangent to Circle Centered at Origin, $\TT_2$ is expressed by the equation:
:$x x_2 + y y_2 = r^2$
but as $\TT_2$ also passes through $\tuple {x_0, y_0}$ we also have:
:$x_0 x_2 + y_0 y_2 = r^2$
This also expresses the condition that $V$ should lie on $\TT_2$:
:$x x_0 + y y_0 = r^2$
So both $U$ and $V$ lie on the straight line whose equation is:
:$x x_0 + y y_0 = r^2$
and the result follows.
{{qed}}
Theorem: Harmonic Property of Pole and Polar/Circle

Let $\CC$ be a circle whose radius is $r$ and whose center is at the origin of a Cartesian plane.
Let $P$ be an arbitrary point in the Cartesian plane.
Let $\LL$ be a straight line through $P$ which intersects $\CC$ at points $U$ and $V$.
Let $Q$ be the point where $\LL$ intersects the polar of $P$.
Then $\tuple {PQ, UV}$ is a harmonic range.

Proof:
From Equation of Circle center Origin, we have that the equation of $\CC$ is:
:$x^2 + y^2 = r^2$
Let $P = \tuple {x_1, y_1}$.
Let $Q = \tuple {x, y}$ be a point on $\LL$.
Let $V$ divide $PQ$ in the ratio $k : 1$.
Then the coordinates of $V$ are:
:$V = \tuple {\dfrac {k x + x_1} {k + 1}, \dfrac {k y + y_1} {k + 1} }$
Substituting into the equation for $\CC$:
{{begin-eqn}}
{{eqn | l = \paren {k x + x_1}^2 + \paren {k x + y_1}^2
      | r = r^2 \paren {k + 1}^2
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = k^2 \paren {x^2 + y^2 - r^2} + 2 k \paren {x x_1 + y y_1 - r^2} + \paren { {x_1}^2 + {y_1}^2 - r^2}
      | r = 0
      | c = 
}}
{{end-eqn}}
The roots of this quadratic equation in $k$ correspond to the points $U$ and $V$.
Now let $Q$ lie on the polar of $P$.
:400px
Then by definition of polar:
:$x x_1 + y y_1 - r^2 = 0$
and the roots of $(1)$ are equal but of opposite sign.
That is, $U$ and $V$ divide $PQ$ internally and externally in the same ratio.
Hence $\tuple {PQ, UV}$ is a harmonic range.
{{qed}}
Theorem: Polar of Point is Perpendicular to Line through Center

Let $\CC$ be a circle.
Let $P$ be a point.
Let $\LL$ be the polar of $P$ with respect to $\CC$.
Then $\LL$ is perpendicular to the straight line through $P$ and the center of $\CC$.

Proof:
Let $\CC$ be positioned so as for its center to be at the origin of a Cartesian plane.
Let $P$ be located at $\tuple {x_0, y_0}$.
From Equation of Straight Line in Plane, $P$ can be described as:
:$y = \dfrac {y_0} {x_0} x$
and so has slope $\dfrac {y_0} {x_0}$.
By definition of polar, $\LL$ has the equation:
:$x x_0 + y y_0 = r^2$
which has slope $-\dfrac {x_0} {y_0}$.
Hence the result from Condition for Straight Lines in Plane to be Perpendicular.
{{qed}}
Theorem: Product of Distances of Polar and Pole from Center of Circle

Let $\CC$ be a circle of radius $r$ whose center is at $O$.
Let $P$ be a point.
Let $\LL_1$ be the polar of $P$ with respect to $\CC$.
Let $\LL_2$ be the line $OP$.
Let $N$ be the point of intersection of $\LL_1$ and $\LL_2$.
Then:
:$ON \cdot OP = r^2$

Proof:
Let $U$ and $V$ be the points where $OP$ intersects $\CC$.
:400px
From Harmonic Property of Pole and Polar wrt Circle, $\tuple {UV, NP}$ form a harmonic range.
That is:
{{begin-eqn}}
{{eqn | l = \dfrac {VN} {NU}
      | r = -\dfrac {VP} {PN}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {ON} {OV}
      | r = \dfrac {OV} {OP}
      | c = as $O$ is the midpoint of $UV$
}}
{{eqn | ll= \leadsto
      | l = ON \cdot OP
      | r = OV^2
      | c = 
}}
{{eqn | r = r^2
      | c = $UV$ is the diameter of $\CC$
}}
{{end-eqn}}
{{qed}}
Theorem: Coordinates of Pole of Given Polar

Let $\CC$ be a circle of radius $r$ whose center is at the origin of a Cartesian plane.
Let $\LL$ be a straight line whose equation is given as:
:$l x + m y + n = 0$
Then the pole $P$ of $\LL$ with respect to $\CC$ is:
:$P = \tuple {-\dfrac l n r^2, -\dfrac m n r^2}$

Proof:
From Equation of Circle center Origin, we have that the equation of $\CC$ is:
:$x^2 + y^2 = r^2$
Let $P = \tuple {x_0, y_0}$.
By definition of polar:
:$x x_0 + y y_0 = r^2$
Comparing this with the equation for $\LL$:
:$\dfrac {x_0} l = \dfrac {y_0} m = \dfrac {r^2} {-n}$
The result follows.
{{qed}}
Theorem: Coordinates of Pole of Given Polar/Homogeneous Coordinates

The pole $P$ of $\LL$ with respect to $\CC$, given in homogeneous Cartesian coordinates is:
:$P = \tuple {l, m, -\dfrac n {r^2} }$

Proof:
From Coordinates of Pole of Given Polar, $P$ can be expressed in conventional Cartesian coordinates as:
:$P = \tuple {-\dfrac l n r^2, -\dfrac m n r^2}$
Hence in homogeneous Cartesian coordinates:
:$P = \tuple {-\dfrac l n r^2, -\dfrac m n r^2, 1}$
From Multiples of Homogeneous Cartesian Coordinates represent Same Point, we multiply each coordinate by $-\dfrac n {r^2}$:
:$P = \tuple {l, m, -\dfrac n {r^2} }$
{{qed}}
Theorem: Reciprocal Property of Pole and Polar

Let $\CC$ be a circle.
Let $P$ and $Q$ be points in the plane of $\CC$.
Let $\PP$ and $\QQ$ be the polars of $P$ and $Q$ with respect to $\CC$ respectively.
Let $Q$ lie on $\PP$ with respect to $\CC$.
Then $P$ lies on $\QQ$.
That is:
:if $P$ lies on the polar of $Q$, then $Q$ lies on the polar of $P$
:if the pole of $\PP$ lies on $\QQ$, then the pole of $\QQ$ lies on $\PP$

Proof:
Let $\CC$ be a circle of radius $r$ whose center is at the origin of a Cartesian plane.
Let $P = \tuple {x_0, y_0}$.
Let $Q = \tuple {x_1, y_1}$.
The polar of $P$ is given by:
:$x x_0 + y y_0 = r^2$
The polar of $Q$ is given by:
:$x x_1 + y y_1 = r^2$
Let $Q$ lie on the polar of $P$.
Then $Q$ satisfies the equation:
:$x_0 x_1 + y_0 y_1 = r^2$
which is exactly the same as the condition for $P$ to lie on $Q$.
{{qed}}
Theorem: Derivative of Differentiable Function on Open Interval is Baire Function

Let $I = \openint a b$ be a open interval.
Let $f : I \to \R$ be a differentiable function.
Let $f' : I \to \R$ be the derivative of $f$.
Then $f'$ is a Baire function.

Proof:
For each $n \in \N$, let $f_n : I \to \R$ be a function with: 
:$\ds \map {f_n} x = n \paren {\map f {\min \set {x + \frac 1 n, \frac {b + x} 2} } - \map f x}$
for each $x$.
Note that from:
:Minimum of Finitely Many Continuous Real Functions is Continuous
:Composite of Continuous Mappings is Continuous
:Combined Sum Rule for Continuous Real Functions
we have:
:$f_n$ is continuous for each $n$. 
We aim to show that $f_n$ converges pointwise to $f'$.
Fix $x \in I$. 
Let $\epsilon$ be a positive real number.
Since $f$ is differentiable with derivative $f'$, there exists $\delta > 0$ such that: 
:$\ds \size {\frac {\map f {x + h} - \map f x} h - \map {f'} x} < \epsilon$
for all real $h$ with $0 < \size h < \delta$.
Let $N$ be the least natural number such that:
:$\ds x + \frac 1 N < \frac {b + x} 2$
That is:
:$\ds N > \frac 2 {b - x} > 0$
Then, for $n > N$ we have: 
:$\ds \min \set {x + \frac 1 n, \frac {b + x} 2} = x + \frac 1 n$
Then, for $n > \max \set {1/\delta, N}$ we also have $0 < 1/n < \delta$, and so: 
{{begin-eqn}}
{{eqn	| l = \size {\map {f_n} x - \map {f'} x}
	| r = \size {n \paren {\map f {x + \frac 1 n} - \map f x} - \map {f'} x}
}}
{{eqn	| r = \size {\frac {\map f {x + \frac 1 n} - \map f x} {\frac 1 n} - \map {f'} x}
}}
{{eqn	| o = <
	| r = \epsilon
}}
{{end-eqn}}
By the definition of pointwise convergence:
:$f_n$ converges pointwise to $f'$.
Since $\sequence {f_n}$ is a sequence of continuous real functions converging pointwise to $f'$, we have: 
:$f'$ is a Baire function.
{{qed}}
Category:Baire Functions
ian3b2bue2j1nw2jipxesinz3xs3hbb
Theorem: Riemann Integrable Dirac Function does not Exist

Let $\delta : \R \to \R$ be a real function.
Let $\phi : \R \to \R$ be a smooth function vanishing outside $\closedint a b$.
Let $a \in \R_{> 0}$ be a real number.
Suppose $\delta$ is Riemann integrable on $\closedint {-a} a$.
Suppose for every $\phi$ we have that:
:$\ds \int_{-a}^a \map \delta x \map \phi x = \map \phi 0$
Then $\delta$ does not exist.

Proof:
{{AimForCont}} $\delta$ exists.
Let $\phi$ be a test function of the following form:
:$\map \phi x = \begin {cases} \map \exp {\dfrac 1 {x^2 - 1} } & : \size x < 1 \\ 0 & : \size x \ge 1 \end {cases}$
Let $n \in \N$ be a natural number.
Let $\phi_n : \R \to \R$ be a real function such that:
:$\forall n \in N : \forall x \in \R : \map {\phi_n} x := \map \phi {n x}$
Then $\map \phi {nx}$ is smooth, vanishes outside $\ds \closedint {- \frac 1 n} {\frac 1 n}$ and:
:$\forall x \in \R : 0 \le \map \phi {nx} \le 1$
Hence:
{{begin-eqn}}
{{eqn | l = \frac 1 e
      | r = \map {\phi_n} 0
}}
{{eqn | r = \int_{-\frac 1 n}^{\frac 1 n} \map \delta x \map \phi {nx} \rd x
}}
{{eqn | o = \le
      | r = \int_{-\frac 1 n}^{\frac 1 n} \paren {\sup_{x \mathop \in \closedint {-\frac 1 n} {\frac 1 n} } \map \delta x} \cdot 1 \rd x
      | c = Riemann Integrable Function is Bounded
}}
{{eqn | r = \paren {\sup_{x \mathop \in \closedint {-\frac 1 n} {\frac 1 n} } \map \delta x} \frac 2 n
}}
{{eqn | ll= \leadsto
      | l = \frac 1 e
      | o = \le
      | r = \paren {\sup_{x \mathop \in \closedint {-1} 1} \map \delta x} \lim_{n \mathop \to \infty} \frac 2 n
      | c = taking the limit $n \to \infty$ of both sides
}}
{{eqn | r = 0
}}
{{end-eqn}}
This is a contradiction.
{{qed}}
Theorem: Baire Function may not be Continuous

Let $X \subseteq \R$.
Let $f : X \to \R$ be a Baire function.
Then $f$ is not necessarily continuous.

Proof:
Let:
:$X = \closedint 0 1$
For each $n$, define the function $f_n : \closedint 0 1 \to \R$ to have: 
:$\map {f_n} x = x^n$
for each $x \in \closedint 0 1$.
Note that for $0 \le x < 1$, we have: 
:$x^n \to 0$
Note also that: 
:$\map {f_n} 1 = 1$
so:
:$\map {f_n} 1 \to 1$
Define $f : \closedint 0 1 \to \R$ by: 
:$\ds \map f x = \begin{cases}0 & 0 \le x < 1 \\ 1 & x = 1\end{cases}$
for each $x \in \closedint 0 1$.
We have: 
:$\sequence {f_n}$ converges to $f$ pointwise.
Clearly $f$ is not continuous at $1$, since:
:$\size {\map f x - \map f 1} = 1$
for any $x \in \hointr 0 1$.
So $f$ is a Baire function that is not continuous. 
{{qed}}
Theorem: Principal Value of One over x is Distribution

Let $\phi \in \map \DD \R$ be a test function.
Let $T : \map \DD \R \to \C$ be a mapping such that:
:$\forall \phi \in \map \DD \R : \map T \phi = \PV \frac {\map \phi x} x \rd x : = \lim_{\epsilon \mathop \to 0} \int_{\size x \mathop > \epsilon} \frac {\map \phi x} x \rd x$
where $\PV$ denotes the Cauchy principal value.
Then $T$ is a Schwartz distribution.

Proof:
Let $\phi \in \map \DD \R$ be a test function with a support on $\closedint {-a} a$.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi x
      | r = \map \phi 0 + \int_0^x \dfrac {\d \map \phi x} {\d x} \rd x
}}
{{eqn | r = \map \phi 0 + x \int_0^1 \dfrac {\d \map \phi {t x} } {\map \d {t x} } \rd t
}}
{{end-eqn}}
Furthermore:
{{begin-eqn}}
{{eqn | l = \int_{a \mathop \ge \size x \mathop > \epsilon} \frac 1 x \rd x
      | r = \int_\epsilon^a \frac 1 x \rd x + \int_{-a}^{-\epsilon} \frac 1 x \rd x
}}
{{eqn | r = \int_\epsilon^a \frac 1 x \rd x + \int_a^\epsilon \frac 1 x \rd x
}}
{{eqn | r = 0
}}
{{end-eqn}}
Theorem: Minimum of Finitely Many Continuous Real Functions is Continuous

Let $n \ge 2$ be a natural number.
Let $X \subseteq \R$. 
Let $f_1, f_2, \ldots, f_n$ be functions $X \to \R$.
Define the function $m : X \to \R$ by:
:$\ds \map m x = \min_i \map {f_i} x$
for all $x \in X$.
Then $m$ is continuous.

Proof:
We proceed by induction.
For all natural numbers $n \ge 2$, let $\map P n$ be the proposition:
:for every collection of $n$ functions $f_1, f_2, \ldots, f_n : X \to \R$, $m$ is continuous.
Theorem: Condition for Lines to be Conjugate

Let $\CC$ be a circle of radius $r$ whose center is at the origin of a Cartesian plane.
Let $\PP$ and $\QQ$ be conjugate lines with respect to $\CC$:
{{begin-eqn}}
{{eqn | ll= \PP:
      | l = l_1 x + m_1 y + n_1
      | r = 0
}}
{{eqn | ll= \QQ:
      | l = l_2 x + m_2 y + n_2
      | r = 0
}}
{{end-eqn}}
Then:
:$l_1 l_2 + m_1 m_2 = \dfrac {n_1 n_2} {r^2}$

Proof:
By definition of conjugate lines, $\PP$ and $\QQ$ are the polars of points $P$ and $Q$ respectively, such that $P$ lies on $\QQ$ and $Q$ lies on $\PP$.
From Coordinates of Pole of Given Polar, $P$ is given by:
:$P = \tuple {-\dfrac {l_1} {n_1} r^2, -\dfrac {m_1} {n_1} r^2}$
We have that $P$ lies on $\QQ$.
Substituting $x = -\dfrac {l_1} {n_1} r^2$ and $y = -\dfrac {m_1} {n_1} r^2$ in the equation of $\QQ$, we obtain:
{{begin-eqn}}
{{eqn | l = l_2 \paren {-\dfrac {l_1} {n_1} r^2} + m_2 \paren {-\dfrac {m_1} {n_1} r^2} + n_2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = l_1 l_2 r^2 + m_1 m_2 r^2
      | r = n_1 n_2
      | c = multiplying by $n_1$ and rearranging
}}
{{end-eqn}}
from which the result follows.
{{qed}}
Theorem: Distributional Derivative of Heaviside Step Function

Let $H : \R \to \closedint 0 1$ be the Heaviside step function.
Let $T \in \map {\DD'} \R$ be a Schwartz distribution corresponding to $H$.
Let $\delta \in \map {\DD'} \R$ be the Dirac delta distribution.
Then the distributional derivative of $T$ is $\delta$.

Proof:
Let $\phi \in \map \DD \R$ be a test function.
Then:
{{begin-eqn}}
{{eqn | l = \map {T'} \phi
      | r = -\map T {\phi'}
      | c = {{Defof|Distributional Derivative}}
}}
{{eqn | r = -\int_{-\infty}^\infty \map H x \map {\phi'} x \rd x
}}
{{eqn | r = -\int_0^\infty \map {\phi'} x \rd x
}}
{{eqn | r = \map \phi 0 - \map \phi \infty
}}
{{eqn | r = \map \phi 0
      | c = {{Defof|Test Function}}, Value of Compactly Supported Function outside its Support, $\infty$ is not in a bounded subset of real numbers
}}
{{eqn | r = \map \delta \phi
      | c = {{Defof|Dirac Delta Distribution}}
}}
{{end-eqn}}
{{qed}}
Theorem: Differentiable Function as Distribution

Let $T \in \map {\DD'} \R$ be a Schwartz distribution.
Let $f : \R \to \R$ be a continuously differentiable real function.
Suppose $T_f$ is a Schwartz distribution identified with $f$.
Then $T_f' = T_{f'}$.

Proof:
Let $\phi \in \map \DD \R$ be a test function with a support on $\closedint a b$.
Then:
{{begin-eqn}}
{{eqn | l = \map {T'_f} \phi
      | r = -\map {T_f} {\phi'}
      | c = {{Defof|Distributional Derivative}}
}}
{{eqn | r = -\int_{-\infty}^\infty \map f x \map {\phi'} x \rd x
}}
{{eqn | r = -\int_a^b \map f x \map {\phi'} x \rd x
      | c = {{Defof|Test Function}}, Integral of Compactly Supported Function
}}
{{eqn | r = -\paren {\map f b \map \phi b - \map f a \map \phi a} + \int_a^b \map \phi x \map {f'} x \rd x
      | c = Integration by Parts
}}
{{eqn | r = \int_a^b \map \phi x \map {f'} x \rd x
      | c = {{Defof|Test Function}}
}}
{{eqn | r = \map {T_{f'} } \phi
}}
{{end-eqn}}
{{qed}}
Theorem: Intersections of Line joining Conjugate Points with Circle form Harmonic Range

Let $\CC$ be a circle.
Let $P$ and $Q$ be conjugate points {{WRT}} $\CC$.
Let $A$ and $B$ be the points of intersection of $PQ$ with $\CC$.
Then $A$ and $B$ are harmonic conjugates {{WRT}} $P$ and $Q$.

Proof:
By definition of conjugate points, the polar of $P$ passes through $Q$.
Hence by Harmonic Property of Pole and Polar wrt Circle, $A$ and $B$ are harmonic conjugates {{WRT}} $P$ and $Q$.
{{Qed}}
Theorem: Conjugate Lines are Harmonic Conjugates with respect to Tangents from Point of Intersection

Let $\CC$ be a circle.
Let $\PP$ and $\QQ$ be conjugate lines {{WRT}} $\CC$.
Let $\PP$ and $\QQ$ intersect at $O$.
Let $OS$ and $OT$ be the tangents to $\CC$ from $O$.
Then $\PP$ and $\QQ$ are harmonic conjugates {{WRT}} $OS$ and $OT$.

Proof:
Let $P$ and $Q$ be the poles of $\PP$ and $\QQ$ {{WRT}} $\CC$.
Because $O$ lies on both $\PP$ and $\QQ$, its polar passes through both $P$ and $Q$.
That is, the polar of $O$ is $PQ$ itself.
:420px
The polar of $O$, by definition, is the chord of contact of $OS$ and $OT$ with $\CC$.
From Intersections of Line joining Conjugate Points with Circle form Harmonic Range, $\tuple {PQ, ST}$ forms a harmonic range.
Hence $\map O {PQ, ST}$ forms a harmonic pencil.
That is, $\PP$ and $\QQ$ are harmonic conjugates {{WRT}} $OS$ and $OT$.
{{Qed}}
Theorem: Triangle Conjugacy is Mutual

Let $\CC$ be a circle.
Let $\triangle PQR$ be a triangle.
Let $\triangle P'Q'R'$ be such that:
:$P'$ is the pole of $QR$
:$Q'$ is the pole of $PR$
:$R'$ is the pole of $PQ$
{{WRT}} $\CC$.
Then:
:$P$ is the pole of $Q'R'$
:$Q$ is the pole of $P'R'$
:$R$ is the pole of $P'Q'$
{{WRT}} $\CC$.
That is, $\triangle PQR$ and $\triangle P'Q'R'$ are '''conjugate triangles {{WRT}} $\CC$'''.
</onlyinclude>

Proof:
We have that:
:the polar of $P'$ is $QR$
:the polar of $Q'$ is $PR$ 
and so both polars pass through $R$.
Therefore:
:the polar of $R$ is $P'Q'$.
Similarly:
:the polar of $P$ is $Q'R'$
and:
:the polar of $Q$ is $P'R'$.
{{qed}}