Is there a rational number between any two irrationals?

Let $x,y\in\mathbb{R}$, $x\neq y$. Without loss of generality, suppose $x<y$. Then there exists a positive $z$ such that $y-x=z$.

By Archimedes' axiom, there exists a natural number $n$ such that $$n > \dfrac{1}{z}$$ $$nz > 1$$ $$ny - nx > 1$$ So there exists an integer $m$ such that $$nx < m < ny$$ $$x < \frac{m}{n} < y$$ i.e. $m/n$ is a rational number between $x$ and $y$.

Since $x$ and $y$ can be any real numbers, in particular they can be irrationals.

Let $a$ and $b$ be distinct irrationals; we lose no generality to suppose $a<b$. Assume they have equal integer parts, since otherwise there is an integer between them and the question is trivial. They have infinite decimal expansions, $.a_1a_2a_3\ldots$ and $.b_1b_2b_3\ldots$. These cannot agree in every position since otherwise $a=b$. So say they agree up to the $n-1$th position and differ at the $n$th. Then $$ x= \;.b_1b_2b_3\ldots b_n 0000000\ldots$$

is a rational number strictly between $a$ and $b$:

$$\begin{align} a &= \;.a_1a_2\ldots a_{n-1}a_n\ldots \\& <\; .a_2a_2\ldots a_{n-1}b_n000\ldots &= x \end{align}$$

because $a_n < b_n$, and

$$\begin{align} x & = \;.b_1b_2b_3\ldots b_n 0000000\ldots \\ & < \;.b_1b_2b_3\ldots b_nb_{n+1}\ldots & = b \end{align}$$

because not all of $b_{n+1}, b_{n+2}, \ldots$ can be zero.

For example, there is a rational number betwen $\sqrt2 = 1.4142\ldots$ and $\sqrt3 -\frac14 = 1.482\ldots$; this method produces the rational number $1.48000\ldots = \frac{37}{25}$. You can of course do the same thing in base 2; then you get $x = 1._20111000\ldots = \frac{23}{16}$, which also works.

It would also be fairly easy to produce a similar argument based on the continued fraction expansions of $a$ and $b$, but I think this is simpler.

We can construct one explicitly. Assume $0\lt a \lt b$. Let $n= \max(2,\lceil \frac 2{b-a}\rceil)$. Then let $m=\lceil na \rceil$ and $a \lt \frac m n \lt b$