avewright/proofwiki-math huggingface dataset:
Theorem: Equation of Straight Line in Plane/General Equation

A straight line $\LL$ is the set of all $\tuple {x, y} \in \R^2$, where:
:$\alpha_1 x + \alpha_2 y = \beta$
where $\alpha_1, \alpha_2, \beta \in \R$ are given, and not both $\alpha_1, \alpha_2$ are zero.

Proof:
Let $y = \map f x$ be the equation of a straight line $\LL$.
From Line in Plane is Straight iff Slope is Constant, $\LL$ has constant slope.
Thus the derivative of $y$ {{WRT|Differentiation}} $x$ will be of the form:
:$y' = c$
Thus:
{{begin-eqn}}
{{eqn | l = y
      | r = \int c \rd x
      | c = Fundamental Theorem of Calculus
}}
{{eqn | r = c x + K
      | c = Primitive of Constant
}}
{{end-eqn}}
where $K$ is arbitrary.
Taking the equation:
:$\alpha_1 x + \alpha_2 y = \beta$
it can be seen that this can be expressed as:
:$y = -\dfrac {\alpha_1} {\alpha_2} x + \dfrac {\beta} {\alpha_2}$
thus demonstrating that $\alpha_1 x + \alpha_2 y = \beta$ is of the form $y = c x + K$ for some $c, K \in \R$.
{{qed}}
Theorem: Slope of Straight Line joining Points in Cartesian Plane

Let $p_1 := \tuple {x_1, y_1}$ and $p_2 := \tuple {x_2, y_2}$ be points in a cartesian plane.
Let $\LL$ be the straight line passing through $p_1$ and $p_2$.
Then the slope of $\LL$ is given by:
:$\tan \theta = \dfrac {y_2 - y_1} {x_2 - x_1}$
where $\theta$ is the angle made by $\LL$ with the $x$-axis.

Proof:
:500px
The slope of a straight line is defined as the change in $y$ divided by the change in $x$.
The change in $y$ from $p_1$ to $p_2$ is $y_2 - y_1$.
The change in $x$ from $p_1$ to $p_2$ is $x_2 - x_1$.
By definition of tangent of $\theta$:
:$\tan \theta = \dfrac {y_2 - y_1} {x_2 - x_1}$
Hence the result.
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Point Form

Let $P_1 := \tuple {x_1, y_1}$ and $P_2 := \tuple {x_2, y_2}$ be points in a cartesian plane.
Let $\LL$ be the straight line passing through $P_1$ and $P_2$.
Then $\LL$ can be described by the equation:
:$\dfrac {y - y_1} {x - x_1} = \dfrac {y_2 - y_1} {x_2 - x_1}$
or:
:$\dfrac {x - x_1} {x_2 - x_1} = \dfrac {y - y_1} {y_2 - y_1}$
This is known as the '''two-point form'''.

Proof:
From the slope-intercept form of the equation of the straight line:
:$(1): \quad y = m x + c$
which is to be satisfied by both $\tuple {x_1, y_1}$ and $\tuple {x_2, y_2}$.
We express $m$ and $c$ in terms of $\paren {x_1, y_1}$ and $\paren {x_2, y_2}$:
{{begin-eqn}}
{{eqn | l = y_1
      | r = m x_1 + c
      | c = 
}}
{{eqn | l = y_2
      | r = m x_2 + c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c
      | r = y_1 - m x_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_2
      | r = m x_2 + y_1 - m x_1
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = m
      | r = \dfrac {y_2 - y_1} {x_2 - x_1}
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = y_1
      | r = m x_1 + c
      | c = 
}}
{{eqn | l = y_2
      | r = m x_2 + c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = m
      | r = \dfrac {y_2 - c} {x_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_1
      | r = \dfrac {y_2 - c} {x_2} x_1 + c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y_1 x_2
      | r = x_1 y_2  + c \paren {x_2 - x_1}
      | c = 
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = c
      | r = \dfrac {y_1 x_2 - x_1 y_2} {x_2 - x_1}
      | c = 
}}
{{end-eqn}}
Substituting for $m$ and $c$ in $(1)$:
{{begin-eqn}}
{{eqn | l = y
      | r = m x + c
      | c = which is $(1)$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \dfrac {y_2 - y_1} {x_2 - x_1} x + \dfrac {y_1 x_2 - x_1 y_2} {x_2 - x_1}
      | c = from $(2)$ and $(3)$
}}
{{eqn | ll= \leadsto
      | l = y \paren {x_2 - x_1} + x_1 y_2
      | r = x \paren {y_2 - y_1} + y_1 x_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y \paren {x_2 - x_1} + x_1 y_2 - y_1 x_1
      | r = x \paren {y_2 - y_1} + y_1 x_2 - x_1 y_1
      | c = adding $y_1 x_1 = x_1 y_1$ to both sides
}}
{{eqn | ll= \leadsto
      | l = y \paren {x_2 - x_1} - y_1 \paren {x_2 - x_1}
      | r = x \paren {y_2 - y_1} - x_1 \paren {y_2 - y_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {y - y_1} \paren {x_2 - x_1} 
      | r = \paren {x - x_1} \paren {y_2 - y_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {y - y_1} {x - x_1}
      | r = \dfrac {y_2 - y_1} {x_2 - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - x_1} {x_2 - x_1}
      | r = \dfrac {y - y_1} {y_2 - y_1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Point Form

Let $P_1 := \tuple {x_1, y_1}$ and $P_2 := \tuple {x_2, y_2}$ be points in a cartesian plane.
Let $\LL$ be the straight line passing through $P_1$ and $P_2$.
Then $\LL$ can be described by the equation:
:$\dfrac {y - y_1} {x - x_1} = \dfrac {y_2 - y_1} {x_2 - x_1}$
or:
:$\dfrac {x - x_1} {x_2 - x_1} = \dfrac {y - y_1} {y_2 - y_1}$
This is known as the '''two-point form'''.

Proof:
Let $\tuple {x, y}$ be an arbitrary point on the straight line through $\tuple {x_1, y_1}$ and $\tuple {x_2, y_2}$.
The area of the triangle formed by $\tuple {x, y}$, $\tuple {x_1, y_1}$ and $\tuple {x_2, y_2}$ is equal to $0$.
Hence from Area of Triangle in Determinant Form:
:$\AA = \dfrac 1 2 \size {\paren {\begin {vmatrix} x & y & 1 \\ x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ \end {vmatrix} } }$
Hence:
{{begin-eqn}}
{{eqn | l = 0
      | r = \dfrac 1 2 \size {\paren {\begin {vmatrix} x & y & 1 \\ x_1 & y_1 & 1 \\ x_2 & y_2 & 1 \\ \end {vmatrix} } }
      | c = Area of Triangle in Determinant Form
}}
{{eqn | r = x_1 y_2 - x_2 y_1 + x_2 y - x y_2 + x y_1 - x_1 y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_2 \paren {y - y_1} - y_2 \paren {x - x_1}
      | r = y x_1 - x y_1
      | c = 
}}
{{eqn | r = x_1 \paren {y - y_1} - y_1 \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x_2 - x_1} \paren {y - y_1}
      | r = \paren {y_2 - y_1} \paren {x - x_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x_2 - x_1} {x - x_1}
      | r = \dfrac {y_2 - y_1} {y - y_1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Point Form

Let $P_1 := \tuple {x_1, y_1}$ and $P_2 := \tuple {x_2, y_2}$ be points in a cartesian plane.
Let $\LL$ be the straight line passing through $P_1$ and $P_2$.
Then $\LL$ can be described by the equation:
:$\dfrac {y - y_1} {x - x_1} = \dfrac {y_2 - y_1} {x_2 - x_1}$
or:
:$\dfrac {x - x_1} {x_2 - x_1} = \dfrac {y - y_1} {y_2 - y_1}$
This is known as the '''two-point form'''.

Proof:
:400px
Let $P = \tuple {x, y}$ be an arbitrary point on the straight line through $P_1 = \tuple {x_1, y_1}$ and $P_2 = \tuple {x_2, y_2}$.
Construct the straight line $P_1 H K$ perpendicular to the $x$-axis.
We have that $\triangle P_1 H P_2$ and $\triangle P_1 K P$ are similar.
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac {P_1 K} {P_1 H}
      | r = \dfrac {K P} {H P_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - x_1} {x_2 - x_1}
      | r = \dfrac {y - y_1} {y_2 - y_1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Point Form

Let $P_1 := \tuple {x_1, y_1}$ and $P_2 := \tuple {x_2, y_2}$ be points in a cartesian plane.
Let $\LL$ be the straight line passing through $P_1$ and $P_2$.
Then $\LL$ can be described by the equation:
:$\dfrac {y - y_1} {x - x_1} = \dfrac {y_2 - y_1} {x_2 - x_1}$
or:
:$\dfrac {x - x_1} {x_2 - x_1} = \dfrac {y - y_1} {y_2 - y_1}$
This is known as the '''two-point form'''.

Proof:
:500px
Let $z_1 = x_1 + i y_1$ and $z_2 = x_2 + i y_2$ be the position vectors of the points $A$ and $B$ embedded in the complex plane.
Let $z = x + i y$ be the position vector of an arbitrary point $P$ on the straight line $AB$.
From the diagram:
{{begin-eqn}}
{{eqn | l = OA + AP
      | r = OP
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 + AP
      | r = z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AP
      | r = z - z_1
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = OA + AB
      | r = OB
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 + AB
      | r = z_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AB
      | r = z_2 - z_1
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | q = \exists t \in \R
      | l = AP
      | r = t AB
      | c = as $A$, $P$ and $B$ are collinear
}}
{{eqn | ll= \leadsto
      | l = z - z_1
      | r = t \paren {z_2 - z_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z
      | r = \paren {1 - t} z_1 + t z_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x - x_1
      | r = t \paren {x_2 - x_1}
      | c = 
}}
{{eqn | l = y - y_1
      | r = t \paren {y_2 - y_1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x - x_1} {x_2 - x_1}
      | r = \dfrac {y - y_1} {y_2 - y_1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Slope-Intercept Form

Let $\LL$ be the straight line in the Cartesian plane such that:
:the slope of $\LL$ is $m$
:the $y$-intercept of $\LL$ is $c$
Then $\LL$ can be described by the equation:
:$y = m x + c$
such that $m$ is the slope of $\LL$ and $c$ is the $y$-intercept.

Proof:
Let $\LL$ be the straight line defined by the general equation:
:$\alpha_1 x + \alpha_2 y = \beta$
We have:
{{begin-eqn}}
{{eqn | l = \alpha_1 x + \alpha_2 y
      | r = \beta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \alpha_2 y
      | r = y_1 - \alpha_1 x + \beta
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = y
      | r = -\dfrac {\alpha_1} {\alpha_2} x + \dfrac {\beta} {\alpha_2}
      | c = 
}}
{{end-eqn}}
Setting $x = 0$ we obtain:
:$y = \dfrac {\beta} {\alpha_2}$
which is the $y$-intercept.
Differentiating $(1)$ {{WRT|Differentiation}} $x$ gives:
:$y' = -\dfrac {\alpha_1} {\alpha_2}$
By definition, this is the slope of $\LL$ and is seen to be constant.
The result follows by setting:
{{begin-eqn}}
{{eqn | l = m
      | r = -\dfrac {\alpha_1} {\alpha_2}
      | c = 
}}
{{eqn | l = c
      | r = \dfrac {\beta} {\alpha_2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Slope-Intercept Form

Let $\LL$ be the straight line in the Cartesian plane such that:
:the slope of $\LL$ is $m$
:the $y$-intercept of $\LL$ is $c$
Then $\LL$ can be described by the equation:
:$y = m x + c$
such that $m$ is the slope of $\LL$ and $c$ is the $y$-intercept.

Proof:
:500px
Let the straight line $\LL$  make an angle $\psi$ with the $x$-axis.
The slope $m$ of $\LL$ is then given by:
:$m = \tan \psi$
Let $B := \tuple {0, c}$ be the $y$-intercept of $\LL$.
Let $P := \tuple {x, y}$ be an arbitrary point on $\LL$.
Let the perpendicular $MP$ to the $x$-axis be constructed from $P$ to intersect the $x$-axis at $M$
Let $BK$ be constructed perpendicular $MP$ from $B$ to intersect $MP$ at $K$.
Then we have:
{{begin-eqn}}
{{eqn | l = BK
      | r = x
      | c = by construction
}}
{{eqn | l = KP
      | r = y - c
      | c = by construction
}}
{{eqn | l = KP
      | r = BK \tan \psi
      | c = {{Defof|Tangent of Angle}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = x \tan \psi + c
      | c = 
}}
{{eqn | r = m x + c
      | c = Definition of $m$
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Intercept Form

Let $\LL$ be a straight line which intercepts the $x$-axis and $y$-axis respectively at $\tuple {a, 0}$ and $\tuple {0, b}$, where $a b \ne 0$.
Then $\LL$ can be described by the equation:
:$\dfrac x a + \dfrac y b = 1$

Proof:
:400px
From the General Equation of Straight Line in Plane, $\LL$ can be expressed in the form:
:$(1): \quad \alpha_1 x + \alpha_2 y = \beta$
where $\alpha_1, \alpha_2, \beta \in \R$ are given, and not both $\alpha_1, \alpha_2$ are zero.
Substituting for the two points whose coordinates we know about:
{{begin-eqn}}
{{eqn | q = x = a, y = 0
      | l = \alpha_1 \times a + \alpha_2 \times 0
      | r = \beta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \alpha_1
      | r = \dfrac \beta a
      | c = 
}}
{{end-eqn}}
and: 
{{begin-eqn}}
{{eqn | q = x = 0, y = b
      | l = \alpha_1 \times 0 + \alpha_2 \times b
      | r = \beta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \alpha_2
      | r = \dfrac \beta b
      | c = 
}}
{{end-eqn}}
We know that $\beta \ne 0$ because none of $a, b, \alpha_1, \alpha_2$ are equal to $0$.
Hence:
{{begin-eqn}}
{{eqn | l = \dfrac \beta a x + \dfrac \beta b y
      | r = \beta
      | c = substituting for $\alpha_1$ and $\alpha_2$ in $(1)$
}}
{{eqn | ll= \leadsto
      | l = \dfrac x a + \dfrac y b
      | r = 1
      | c = dividing both sides by $\beta$
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Intercept Form

Let $\LL$ be a straight line which intercepts the $x$-axis and $y$-axis respectively at $\tuple {a, 0}$ and $\tuple {0, b}$, where $a b \ne 0$.
Then $\LL$ can be described by the equation:
:$\dfrac x a + \dfrac y b = 1$

Proof:
By definition, $\LL$ passes through $\tuple {a, 0}$ and $\tuple {0, b}$.
From the Two-Point Form of Equation of Straight Line in Plane, $\LL$ can be expressed in the form:
{{begin-eqn}}
{{eqn | l = \dfrac {y - 0} {x - a}
      | r = \dfrac {b - 0} {0 - a}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = -a y
      | r = b x - b a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac x a + \dfrac y b
      | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Two-Intercept Form

Let $\LL$ be a straight line which intercepts the $x$-axis and $y$-axis respectively at $\tuple {a, 0}$ and $\tuple {0, b}$, where $a b \ne 0$.
Then $\LL$ can be described by the equation:
:$\dfrac x a + \dfrac y b = 1$

Proof:
:400px
We have that $\LL$ is passes through the two points $A = \tuple {a, 0}$ and $B = \tuple {0, b}$.
Let $P = \tuple {x, y}$ be an arbitrary point on $\LL$.
We have:
{{begin-eqn}}
{{eqn | l = \triangle OBP + \triangle OAP
      | r = \triangle OAB
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {b x} 2 + \dfrac {a y} 2
      | r = \dfrac {a b} 2
      | c = Area of Triangle in Terms of Side and Altitude
}}
{{eqn | ll= \leadsto
      | l = b x + a y
      | r = a b
      | c = multiplying both sides by $2$
}}
{{eqn | ll= \leadsto
      | l = \dfrac x a + \dfrac y b
      | r = 1
      | c = dividing both sides by $a b$ and rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Normal Form

Let $\LL$ be a straight line such that:
:the perpendicular distance from $\LL$ to the origin is $p$
:the angle made between that perpendicular and the $x$-axis is $\alpha$.
Then $\LL$ can be defined by the equation:
:$x \cos \alpha + y \sin \alpha = p$

Proof:
:400px
Let $A$ be the $x$-intercept of $\LL$.
Let $B$ be the $y$-intercept of $\LL$.
Let $A = \tuple {a, 0}$ and $B = \tuple {0, b}$.
From the Equation of Straight Line in Plane: Two-Intercept Form, $\LL$ can be expressed in the form:
:$(1): \quad \dfrac x a + \dfrac y a = 1$
Then:
{{begin-eqn}}
{{eqn | l = p
      | r = a \cos \alpha
      | c = {{Defof|Cosine of Angle}}
}}
{{eqn | ll= \leadsto
      | l = a
      | r = \dfrac p {\cos \alpha}
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = p
      | r = b \sin \alpha
      | c = {{Defof|Sine of Angle}}
}}
{{eqn | ll= \leadsto
      | l = b
      | r = \dfrac p {\sin \alpha}
      | c = 
}}
{{end-eqn}}
Substituting for $a$ and $b$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \dfrac x a + \dfrac y a
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {x \cos \alpha} p + \dfrac {y \sin \alpha} p
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \cos \alpha + y \sin \alpha
      | r = p
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Equation of Straight Line in Plane/Normal Form

Let $\LL$ be a straight line such that:
:the perpendicular distance from $\LL$ to the origin is $p$
:the angle made between that perpendicular and the $x$-axis is $\alpha$.
Then $\LL$ can be defined by the equation:
:$x \cos \alpha + y \sin \alpha = p$

Proof:
:400px
Let $P = \tuple {x, y}$ be an arbitrary point on $\LL$.
Let $O$ be the origin of the Cartesian plane in which $\LL$ is embedded.
Let $PQ$ be the perpendicular dropped from $P$ to the $x$-axis.
Let $QS$ be the perpendicular dropped from $Q$ to the line $ON$.
Let $PR$ be the perpendicular dropped from $P$ to the line $QS$.
By definition of cosine:
:$OS = OQ \cos \alpha$
By definition of sine:
:$PR = PQ \sin \alpha$
Then:
{{begin-eqn}}
{{eqn | l = p
      | r = ON
      | c = 
}}
{{eqn | r = OS + SN
      | c = 
}}
{{eqn | r = OS + PR
      | c = 
}}
{{eqn | r = OQ \cos \alpha + PQ \sin \alpha
      | c = 
}}
{{eqn | r = x \cos \alpha + y \sin \alpha
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Perpendicular Distance from Straight Line in Plane to Point/General Form

Let $\LL$ be a straight line embedded in a cartesian plane, given by the equation:
:$a x + b y + c = 0$
Let $P$ be a point in the cartesian plane whose coordinates are given by:
:$P = \tuple {x_0, y_0}$
Then the perpendicular distance $d$ from $P$ to $\LL$ is given by:
:$d = \dfrac {\size {a x_0 + b y_0 + c} } {\sqrt {a^2 + b^2} }$

Proof:
We have that $\LL$ has the equation:
:$(1): \quad a x + b y + c = 0$
500px
Let a perpendicular be dropped from $P$ to $\LL$ at $Q$.
The perpendicular distance $d$ that we are to find is then $PQ$.
In order to simplify the algebra that will inevitably follow, we are to make a transformation as follows.
Let $\MM$ be constructed parallel to $\LL$.
Construct a perpendicular from $\MM$ to pass through the origin.
Let this perpendicular intersect $\MM$ at $R$ and $\LL$ at $S$.
We have that $PQSR$ is a rectangle, and so $RS = PQ$.
It remains to establish the length of $RS$.
We can manipulate $(1)$ into slope-intercept form as:
:$y = -\dfrac a b x - \dfrac c b$
Thus the slope of $\LL$ is $-\dfrac a b$.
From Condition for Straight Lines in Plane to be Perpendicular, the  slope of $RS$ is then $\dfrac b a$.
The next step is to find the coordinates of $R$ and $S$.
From Equation of Straight Line in Plane: Point-Slope Form, the equation of $\MM$ can be given as:
:$y - y_0 = -\dfrac a b \paren {x - x_0}$
or:
:$(2): \quad y = \dfrac {-a x + a x_0 + b y_0} b$
From Equation of Straight Line in Plane: Slope-Intercept Form, the equation of $RS$ can be given as:
:$(3): \quad y = \dfrac b a x$
$\MM$ and $RS$ intersect where these are equal:
:$\dfrac b a x = \dfrac {-a x + a x_0 + b y_0} b$
which gives us:
:$x = \dfrac {a \paren {a x_0 + b y_0} } {a^2 + b^2}$
Substituting back for $y$ in $3$, we find that:
:$R = \tuple {\dfrac {a \paren {a x_0 + b y_0} } {a^2 + b^2}, \dfrac {b \paren {a x_0 + b y_0} } {a^2 + b^2} }$
Now to find the coordinates of $S$, which is the intersection of $\LL$ and $RS$.
We can express $\LL$ as:
:$y = -\dfrac {a x + c} b$
and so:
:$\dfrac b a x = -\dfrac {a x + c} b$
which leads to:
:$x = -\dfrac {a c} {a^2 + b^2}$
Substituting back for $y$ in $3$, we get (after algebra):
:$S = \tuple {\dfrac {-a c} {a^2 + b^2}, \dfrac {-b c} {a^2 + b^2} }$
It remains to find the length $d$ of $RS$.
From the Distance Formula:
{{begin-eqn}}
{{eqn | l = d
      | r = \sqrt {\paren {\dfrac {-a c} {a^2 + b^2} - \dfrac {a \paren {a x_0 + b y_0} } {a^2 + b^2} }^2 + \paren {\dfrac {-b c} {a^2 + b^2} - \dfrac {b \paren {a x_0 + b y_0} } {a^2 + b^2} }^2 }
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {\paren {-a \paren {a x_0 + b y_0 + c} }^2 + \paren {-b \paren {a x_0 + b y_0 + c} }^2} {\paren {a^2 + b^2}^2 } }
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {\paren {a^2 + b^2} \paren {a x_0 + b y_0 + c}^2} {\paren {a^2 + b^2}^2 } }
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {\paren {a x_0 + b y_0 + c}^2} {a^2 + b^2} }
      | c = 
}}
{{eqn | r = \dfrac {\size {a x_0 + b y_0 + c} } {\sqrt {a^2 + b^2} }
      | c = as length is positive
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Straight Line in Plane/Point-Slope Form

Let $\LL$ be a straight line embedded in a cartesian plane, given in slope-intercept form as:
:$y = m x + c$
where $m$ is the slope of $\LL$.
Let $\LL$ pass through the point $\tuple {x_0, y_0}$.
Then $\LL$ can be expressed by the equation:
:$y - y_0 = m \paren {x - x_0}$

Proof:
As $\tuple {x_0, y_0}$ is on $\LL$, it follows that:
{{begin-eqn}}
{{eqn | l = y_0
      | r = m x_0 + c
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c
      | r = y_0 - m x_0 
      | c = 
}}
{{end-eqn}}
Substituting back into the equation for $\LL$:
{{begin-eqn}}
{{eqn | l = y
      | r = m x + \paren {y_0 - m x_0}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y - y_0
      | r = m \paren {x - x_0}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Shortest Possible Distance between Lattice Points on Straight Line in Cartesian Plane

Let $\LL$ be the straight line defined by the equation:
:$a x - b y = c$
Let $p_1$ and $p_2$ be lattice points on $\LL$.
Then the shortest possible distance $d$ between $p_1$ and $p_2$ is:
:$d = \dfrac {\sqrt {a^2 + b^2} } {\gcd \set {a, b} }$
where $\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.
{{explain|Review the above -- it is not given that $a$ and $b$ are integers.}}

Proof:
Let $p_1 = \tuple {x_1, y_1}$ and $p_2 = \tuple {x_2, y_2}$ be on $\LL$.
Thus:
{{begin-eqn}}
{{eqn | l = a x_1 - b y_1
      | r = c
}}
{{eqn | l = a x_2 - b y_2
      | r = c
      | c = 
}}
{{end-eqn}}
From Solution of Linear Diophantine Equation, it is necessary and sufficient that:
:$\gcd \set {a, b} \divides c$
for such lattice points to exist.
Also from Solution of Linear Diophantine Equation, all lattice points on $\LL$ are solutions to the equation:
:$\forall k \in \Z: x = x_1 + \dfrac b m k, y = y_1 - \dfrac a m k$
where $m = \gcd \set {a, b}$.
So we have:
{{begin-eqn}}
{{eqn | l = x_2
      | r = x_1 + \dfrac b m k
}}
{{eqn | l = y_2
      | r = y_1 - \dfrac a m k
      | c = 
}}
{{end-eqn}}
for some $k \in \Z$ such that $k \ne 0$.
The distance $d$ between $p_1$ and $p_2$ is given by the Distance Formula:
{{begin-eqn}}
{{eqn | l = d
      | r = \sqrt {\paren {x_1 - \paren {x_1 + \dfrac b m k} }^2 + \paren {y_1 - \paren {y_1 - \dfrac a m k} }^2}
      | c = 
}}
{{eqn | r = \sqrt {\paren {\dfrac {b k} m}^2 + \paren {\dfrac {a k} m}^2}
      | c = 
}}
{{eqn | r = \sqrt {\dfrac {k^2 \paren {a^2 + b^2} } {m^2} }
      | c = 
}}
{{eqn | r = k \dfrac {\sqrt {a^2 + b^2} } m
      | c = 
}}
{{end-eqn}}
This is a minimum when $k = 1$.
Hence the result.
{{qed}}
Theorem: Decomposition into Even-Odd Integers is not always Unique

For every even integer $n$ such that $n > 1$, if $n$ can be expressed as the product of one or more even-times odd integers, it is not necessarily the case that this product is unique.

Proof:
Let $n \in \Z$ be of the form $2^2 p q$ where $p$ and $q$ are odd primes.
Then:
:$n = \paren {2 p} \times \paren {2 q} = 2 \times \paren {2 p q}$
A specific example that can be cited is $n = 60$:
:$60 = 6 \times 10$
and:
:$60 = 2 \times 30$.
Each of $2, 6, 10, 30$ are even-times odd integers:
{{begin-eqn}}
{{eqn | l = 2
      | r = 2 \times 1
}}
{{eqn | l = 6
      | r = 2 \times 3
}}
{{eqn | l = 10
      | r = 2 \times 5
}}
{{eqn | l = 30
      | r = 2 \times 15
}}
{{end-eqn}}
Every $n \in \Z$ which has a divisor in that same form $2^2 p q$ can similarly be decomposed non-uniquely into even-times odd integers.
{{qed}}