Theorem: Power of a Point Theorem

Let $C$ be a circle in the Euclidean plane whose center is $O$ and whose radius is $r$.
Let $P$ be an arbitrary point in the plane.
Let $p$ be the power of point $P$ {{WRT}} $C$.
Let a directed line segment from $P$ be drawn either:
:intersecting $C$ at two points $A$ and $A'$
or:
:tangent to $C$ at $A = A'$.
Then:
:$PA \cdot PA' = p$

Proof:
Let $d$ be the distance from $P$ to $O$.
Let $t$ be the length of the tangent from $P$ to $C$.
We use the following several times.
{{begin-eqn}}
{{eqn | l = PA 
      | r = -AP
      | c = {{Defof|Directed Line Segment}}
}}
{{eqn | n = 1
      | l = PA \cdot PA' 
      | r = -AP \cdot PA'
      | c = substitution
}}
{{eqn | n = 2
      | l = p 
      | r = d^2 - r^2
      | c = {{Defof|Power of Point}}
}}
{{eqn | n = 3
      | l = d^2 
      | r = t^2 + r^2
      | c = Pythagoras's Theorem
}}
{{eqn | n = 4
      | l = p 
      | r = t^2
      | c = from $(2)$ and $(3)$
}}
{{end-eqn}}
;$P$ is Circle Center
By definition of center of circle:
:a straight line through $O$ is a diameter of $C$.
{{begin-eqn}}
{{eqn | l = P
      | r = O
      | c = by construction
}}
{{eqn | ll= \leadsto
      | l = d
      | r = 0
      | c = 
}}
{{eqn | l = AP
      | r = r
      | c = {{Defof|Circle}}
}}
{{eqn | l = PA'
      | r = r
      | c = {{Defof|Circle}}
}}
{{eqn | ll= \leadsto
      | l = AP \cdot PA'
      | r = r^2
      | c =
}}
{{eqn | l = PA \cdot PA'
      | r = -r^2
      | c = $(1)$
}}
{{eqn | l = p
      | r = d^2 - r^2
      | c = $(2)$
}}
{{eqn | ll= \leadsto
      | l = p
      | r = -r^2
      | c =
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA'
      | r = p
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
;$P$ is Interior Point of $C$
:200px
Let $P$ be in the interior of $C$ but not at $O$.
Let $BB'$ be the diameter of $C$ through $P$.
{{begin-eqn}}
{{eqn | l = BP
      | r = r - d
      | c = by construction
}}
{{eqn | l = PB'
      | r = r + d
      | c = by construction
}}
{{eqn | ll= \leadsto
      | l = BP \cdot PB'
      | r = \paren {r + d} \paren {r - d}
      | c =
}}
{{eqn | ll= \leadsto
      | l = BP \cdot PB'
      | r = r^2 - d^2
      | c =
}}
{{eqn | l = AP \cdot PA'
      | r = BP \cdot PB'
      | c = Intersecting Chords Theorem
}}
{{eqn | l = AP \cdot PA'
      | r = r^2 - d^2
      | c = {{EuclidCommonNotionLink|1}}
}}
{{eqn | l = PA \cdot PA'
      | r = d^2 - r^2
      | c = $(1)$
}}
{{eqn | l = p 
      | r = d^2 - r^2
      | c = $(2)$
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA' 
      | r = p
      | c =
}}
{{end-eqn}}
{{qed|lemma}}
;$P$ is on circle $C$
{{begin-eqn}}
{{eqn | l = PA
      | r = 0
      | c = by construction
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA'
      | r = 0
      | c = 
}}
{{eqn | l = d
      | r = r
      | c = by construction
}}
{{eqn | l = p 
      | r = d^2 - r^2
      | c = $(2)$
}}
{{eqn | ll= \leadsto
      | l = p
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA'
      | r = p
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
;$P$ is Exterior Point and $PA$ tangent to $C$
Let $A$ be such that $PA$ is tangent to $C$ at $A$.
We have {{hypothesis}} that the point $A'$ is the same point as $A$.
{{begin-eqn}}
{{eqn | l = PA
      | r = t
      | c = by construction
}}
{{eqn | l = PA'
      | r = PA
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA'
      | r = t^2
      | c = 
}}
{{eqn | l = p
      | r = t^2
      | c = $(4)$
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA'
      | r = p
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
;$P$ is Exterior Point and $PAA'$ a secant of $C$
{{begin-eqn}}
{{eqn | l = PA \cdot PA'
      | r = t^2
      | c = Tangent Secant Theorem
}}
{{eqn | l = p
      | r = t^2
      | c = $(4)$
}}
{{eqn | ll= \leadsto
      | l = PA \cdot PA'
      | r = p
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}