I am having some trouble writing a bijection between $\mathbb{N} = \{0, 1, 2, 3, \ldots\}$ and $\mathbb{N}^2$, particularly using the definition that $\mathbb{N}$ includes $0$. (Otherwise, it is straightforward.) Here is what I have so far.
Consider an arbitrary positive integer, $z$. I claim that we can write $z$ as the the unique product of some power of $2$ and an odd number, that is, we may write $z = 2^a m^b$ for some odd $m$ (since $m^b$ is odd for any odd $m$ and integral power $b$).
Proof of claim. If $z$ is odd, we may write $$z = 1 \cdot z = 2^0 z,$$ and the result is proved. If $z$ is even, $z$ is divisible by $2$. Let $k$ be the highest power of $2$ that divides evenly into $z$. Then, $$z = 2^k \cdot r,$$ for some integer $r$. If $r$ is even, then write $r = 2j$ for some integer $j$, but then $$z = 2^k \cdot 2j = 2^{k+1} j,$$ meaning that there exists a higher power of $2$ that divides evenly into $z$, a contradiction. Hence, $r$ must be even, and the construction is proved.
Hence, for any positive $z \in \mathbb{N}$, we may write $$z = 2^a m^b$$ for integers $a$ and $b$. We may $z$ to the pair $(a,b)$ when $z$ is positive. When $z = 0$, map $z$ to $(0,0)$.
The problem is I cannot figure out how to write this bijection as an explicit formula from $\mathbb{N}$ to $\mathbb{N}^2$. Is there a way to do this?
The decomposition $2^a m^b$ is not unique for all integers, but it would be without the $b$. For example, the number $18$ could be written as $2^1 \times 9^1$ or $2^1 \times 3^2$.
Instead, just use the decomposition $2^a(2b + 1)$, where $a, b \in \Bbb{N}$ (including $0$). To prove this, we basically use the proof you presented. Dividing by the highest power of $2$ of a positive integer must yield an odd number, which means that every positive integer can be expressed in this form. This expression is unique, since the $a$ in $2^a(2b + 1)$ can be recovered by finding the highest power of $2$ that divides the given number, and the $b$ follows instantly from this.
Every positive integer can be expressed uniquely in this form, so every natural number can be expressed in the form $2^a(2b + 1) - 1$. We can therefore write an explicit bijection: $$f : \Bbb{N}^2 \to \Bbb{N} : (a, b) \mapsto 2^a(2b + 1) - 1.$$ If you want a bijection from $\Bbb{N}$ to $\Bbb{N}^2$, consider $f^{-1}$. It's actually most simple to express as a method: to compute $f^{-1}(n)$, let $a$ be the highest power of $2$ that divides $n$, and let $b = 2^{-a}n$. If you want a symbolic formula for whatever reason, you could try: $$f^{-1}(n) = \left(\log_2(\gcd(n + 1,2^{n+1})), \frac{n + 1}{\gcd(n + 1, 2^{n + 1})}\right).$$