Working on the book: Lang, Serge & Murrow, Gene. "Geometry - Second Edition" (p. 170)
- In Figure 5.67, line $L$ is tangent to the circle at $P$. Prove that no other point on $L$ can possibly intersect the circle. [Hint: If $Q$ is a point on $L$ and $P\neq Q$, show that $d(O, Q) > d(O, P)$. Cf. Theorem 3-5.]
Proof:
Let:
- $C$ be a circle with radius $r$ and center $O$.
- $L$ a line tangent to $C$ at point $P$.
Show:
$$ \lnot \exists Q(Q \in L \land Q \neq P \land Q \in C) $$
or, equivalently:
$$ \forall Q(Q \in L \to (Q \neq P \to Q \notin C)) $$
I will use Fitch-style natural deduction system (indented bars denote sub-proofs). Added instantiated theorems and axioms to the premises.
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $
$ \fitch{1.\,P \in C\\ 2.\,P \in L\\ 3.\,P \in C \leftrightarrow d(O, P) = r\\ 4.\,Q \in C \leftrightarrow d(O, Q) = r\\ 5.\,d(O, Q)^2 = d(P, Q)^2 + d(O,P)^2 \qquad \text{Pythagoras}\\ 6.\,0 = d(P, Q) \leftrightarrow Q = P \qquad \text{DIST 1} }{ \fitch{7.\,Q \in L}{ \fitch{8.\,Q \neq P}{ \fitch{9.\,Q \in C}{ 10.\,d(O, Q) = r \be{4,9} 11.\,d(O, P) = r \be{3,1} 12.\,d(O, Q) = d(O, P) \qe{11,10} 13.\,d(O, Q)^2 = d(O, P)^2 \qquad \text{arithmetic}\\ 14.\,d(O, Q)^2 = d(P, Q)^2 + d(O,P)^2 \R{5} 15.\,d(O, Q)^2 = d(P, Q)^2 + d(O,Q)^2 \qe{12,14} 16.\,0 = d(P, Q)^2 \qquad \text{arithmetic}\\ 17.\,0 = d(P, Q) \qquad \text{arithmetic}\\ 18.\,Q = P \be{6,17} 19.\,\bot \ii{8,18} }\\ 20.\,Q \notin C \ni{10-19} }\\ 21.\,Q \neq P \to Q \notin C \ii{8-20} }\\ 22.\,Q \in L \to (Q \neq P \to Q \notin C)\ii{7-21} 23.\,\forall Z(Z \in L \to (Z \neq P \to Z \notin C)) \Ai{22} } $
Is this symbolization and proof correct ?