Is it possible to prove algebraically that these formulas for calculating a rotated point produce the same result? The following shows 2 formulas to calculate a point $(x',y')$, which is $(x,y)$ rotated $\theta$ degrees.
$$\begin{bmatrix}x'\\y'\end{bmatrix}=\begin{bmatrix}\cos\theta&-\sin\theta\\\sin\theta&\cos\theta\end{bmatrix}\begin{bmatrix}x\\y\end{bmatrix}=\begin{bmatrix}h\cos(\theta')\\h\sin(\theta')\end{bmatrix}$$
where
$$h=\sqrt{x^2+y^2}\\\theta'=\theta+\operatorname{arctan2}(x, y)$$
where
$$\operatorname{arctan2}(x, y) =
\begin{cases}
 \arctan(\frac y x) &\text{if } x > 0 \\
 \arctan(\frac y x) + \pi &\text{if } x < 0 \text{ and } y \ge 0 \\
 \arctan(\frac y x) - \pi &\text{if } x < 0 \text{ and } y < 0 \\
 +\frac{\pi}{2} &\text{if } x = 0 \text{ and } y > 0 \\
 -\frac{\pi}{2} &\text{if } x = 0 \text{ and } y < 0 \\
 0 &\text{if } x = 0 \text{ and } y = 0
\end{cases}$$
The first one is applying a 2D rotation matrix, and the second one is from a computer program I wrote some time ago, which directly handles the process of rotating a point, but computationally much slower.
I was wondering why these two produce the same result. Of course, they do the same operation geometrically, but is it possible to prove algebraically that the equality always hold for any real number $x$, $y$, and $\theta$?

Following about the study of the geometric transformations of the plane it's known that the counterclockwise rotations of center $O$ are described by the linear equations:
$$
\begin{cases}
x' = x\,\cos\theta - y\,\sin\theta \\
y' = x\,\sin\theta + y\,\cos\theta \\
\end{cases}\,.
$$
At this point we can decline two cases:

*

*if $x^2+y^2=0$, i.e. $x=y=0$, we have $x'=y'=0$;


*if $x^2+y^2\ne0$, instead, we can write:
$$
\begin{cases}
x' = \sqrt{x^2+y^2}\left(\frac{x}{\sqrt{x^2+y^2}}\,\cos\theta - \frac{y}{\sqrt{x^2+y^2}}\,\sin\theta\right) \\
y' = \sqrt{x^2+y^2}\left(\frac{x}{\sqrt{x^2+y^2}}\,\sin\theta + \frac{y}{\sqrt{x^2+y^2}}\,\cos\theta\right) \\
\end{cases}
$$
and given that:
$$
\small
-1 \le \frac{x}{\sqrt{x^2+y^2}} \le 1\,,
\quad \quad
-1 \le \frac{y}{\sqrt{x^2+y^2}} \le 1\,,
\quad \quad
\left(\frac{x}{\sqrt{x^2+y^2}}\right)^2+\left(\frac{y}{\sqrt{x^2+y^2}}\right)^2=1
$$
it's possible to write:
$$
\begin{cases}
x' = \sqrt{x^2+y^2}\left(\cos\varphi\,\cos\theta - \sin\varphi\,\sin\theta\right) \\
y' = \sqrt{x^2+y^2}\left(\cos\varphi\,\sin\theta + \sin\varphi\,\cos\theta\right) \\
\end{cases}
$$
which thanks to the cosine and sine addition formulas are equivalent to:
$$
\begin{cases}
x' = \sqrt{x^2+y^2}\,\cos(\varphi+\theta) \\
y' = \sqrt{x^2+y^2}\,\sin(\varphi+\theta) \\
\end{cases}\,.
$$
This is exactly what you wrote, where:
$$
\cos\varphi := \frac{x}{\sqrt{x^2+y^2}}\,,
\quad \quad \quad
\sin\varphi := \frac{y}{\sqrt{x^2+y^2}}
$$
and from trivial graphical considerations it's possible to retrace all the cases with which 2-argument arctangent function was built:
$$
\varphi = \text{atan2}(y,\,x)\,.
$$
The fact that you, artificially, also defined the case $x=y=0$ means that all possible cases are covered and this proves the equality between the two formulations, even if the first is cleaner.
