Prove that the elements of sequences $(a_n),(b_n)$ are rational numbers such that $a_n<\sqrt{2}<b_n=a_n+2^{-n}$ for all $n \geq 1$ using induction

For reference I am in Introduction to Abstract Math; I have taken Discrete Math, Calculus 1, and Linear Algebra. I am stuck on the inductive step of the proof below. What would be a good approach to go about doing it? I have no idea.

Let $a_0 = 1$ and $b_0 = 2$. For $n \geq 0$, define $m_n, a_{n+1},$ and $b_{n+1}$ as follows:

(i) Let $m_n = (a_n +b_n)/2$.

(ii) If $m^2_n \leq 2$, let $a_{n+1} = m_n$ and $b_{n+1} = b_n$;

If $m^2_n > 2$, let $a_{n+1} = a_n$ and $b_{n+1} = m_n$.

Compute the first six terms of the sequences $(a_n), \: (b_n),$ and $(m_n)$.

$$m_0 = (a_0 + b_0)/2 = (1 + 2)/2 = \frac{3}{2}$$ $$m_0^2 = \frac{9}{4} > 2, \: \therefore a_1 = a_0 = 1, \: b_1 = m_0 = \frac{3}{2}$$ $$m_1 = (a_1 + b_1)/2 = \left(1 + \frac{3}{2}\right) /2 = \frac{5}{4}$$ $$m_1^2 = \frac{25}{16} \leq 2, \: \therefore a_2 = m_1 = \frac{5}{4}, \: b_2 = b_1 = \frac{3}{2}$$ $$m_2 = (a_2 + b_2)/2 = \left(\frac{5}{4} + \frac{3}{2}\right)/2 = \frac{11}{8}$$ $$m_2^2 = \frac{121}{64}\leq 2, \: \therefore a_3 = m_2 = \frac{11}{8}, \: b_3 = b_2 = \frac{3}{2}$$ $$m_3 = (a_3 + b_3)/2 = \left(\frac{11}{8} + \frac{3}{2}\right)/2 = \frac{23}{16}$$ $$m_3^2 = \frac{529}{256} > 2, \: \therefore a_4 = a_3 = \frac{11}{8}, \: b_4 = m_3 = \frac{23}{16}$$ $$m_4 = (a_4 + b_4)/2 = \left(\frac{11}{8} + \frac{23}{16}\right)/2 = \frac{45}{32}$$ $$m_4^2 = \frac{2025}{1024} \leq 2, \: \therefore a_5 = m_4 = \frac{45}{32}, \: b_5 = b_4 = \frac{23}{16}$$ $$m_5 = (a_5 + b_5)/2 = \left(\frac{45}{32} + \frac{23}{16}\right)/2 = \frac{91}{64}$$ $$m_5^2 = \frac{8281}{4096} > 2, \: \therefore a_6 = a_5 = \frac{45}{32}, \: b_6 = m_5 = \frac{91}{64}$$ $$m_6 = (a_6 + b_6)/2 = \left(\frac{45}{32} + \frac{91}{64}\right)/2 = \frac{181}{128}$$ $$(a_n)=\left(1, 1, \frac{5}{4}, \frac{11}{8}, \frac{11}{8}, \frac{45}{32}, \frac{45}{32}, \: \ldots \right)$$ $$(b_n)=\left(2, \frac{3}{2}, \frac{3}{2}, \frac{3}{2}, \frac{23}{16}, \frac{23}{16}, \frac{91}{64}, \: \ldots \right)$$ $$(m_n)=\left(\frac{3}{2}, \frac{5}{4}, \frac{11}{8}, \frac{23}{16}, \frac{45}{32}, \frac{91}{64}, \frac{181}{128}, \: \ldots \right)$$

Use induction to prove that $a_n$ and $b_n$ are rational numbers such that $$a_n < \sqrt{2} < b_n = a_n + 2^{-n} \textrm{ for all } n \geq 1.$$

Base Case

Try to see if the statement holds true for $n=0$. $$a_0 < \sqrt{2} < b_0 = a_0 + 2^0$$ $$1 < \sqrt{2} < 2 = 1 + 1$$ $$1 < \sqrt{2} < 2 = 2$$ Thus, the statement is true for $n=0$.

Here's where I got stuck, I don't know where to start for this.

At the risk of sounding like I'm taking your question too literally, the best way to start is to start writing down the "boilerplate" of the proof. Because we're doing induction on a non-negative integer $n$ you start with the first two sentences below[0], "Consider..." and "Assume...". Then we need to prove something about $a_{n+1}$ and $b_{n+1}$ so we better figure out what they are. This immediately leads to the next sentence ("The definitions of...").

Consider the case $n+1$ for $n \ge 0$. Assume the inductive hypothesis, $a_n < \sqrt{2} < b_n$. The definitions of $a_{n+1}$ and $b_{n+1}$ depend on whether $m_n^2 \le 2$ so we consider each case separately:

If $m_n^2 \le 2$, then $a_{n+1} = ***$ and $b_{n+1} = ***$. Then $***$. So $a_{n+1} < \sqrt{2} < b_{n+1}$.

If $m_n^2 > 2$, then $a_{n+1} = ***$ and $b_{n+1} = ***$. Then $***$. So $a_{n+1} < \sqrt{2} < b_{n+1}$.

Now you have a much more concrete problem: fill in the $***$s. But it's important to understand that in order to get to this point the only non-mechanical knowledge I used was that we would need to know the definitions of $a_{n+1}$ and $b_{n+1}$. But the first two sentences are entirely mechanical because it's a proof by induction. And then the rest is mechanical because the only way to get at the definitions of $a_{n+1}$ and $b_{n+1}$ is by getting "inside" the case analysis found in their definition using our own case analysis. Of course in general practice you may discover things like there are some shared facts between the cases and so on so that the basic pattern ends up getting changed as you write the proof, but the pattern is still where you'll start.

In this case, try proving the $m_n^2 > 2$ case first, because it turns out it doesn't even depend on definition of $m$ (i.e. statement (i)). There's a bit more trouble to prove the final inequality is strict for the $m_n^2 \le 2$ case and you'll have to know something about $m$.

[0] These may need to be rewritten depending on target audience preferences; e.g. we may need to use indexes shifted back by one so we talk about $n-1$ and $n$. Or there may be a set way of writing induction proofs you're supposed to be following, so use that instead. But it will amount to the same thing.

Suppose the statement is true for $n$. Then $m_{n} = (a_n+b_n)/2$ is rational.

If $m_{n}^{2}\leq 2$ then $a_{n+1} = m_{n}\leq\sqrt{2}$. But since $m_{n}$ is rational $a_{n+1}< \sqrt{2}$. In this case we also have $b_{n+1} = b_{n} > \sqrt{2}$ and $b_{n+1} = a_{n}+2^{-n} = 2a_{n+1}-b_{n+1}+2^{-n}$. Therefore, $b_{n+1} = a_{n+1}+2^{-(n+1)}$.

If $m_{n}^{2} > 2$ then $a_{n+1} = a_{n} < \sqrt{2}$ and $b_{n+1} = m_{n} > \sqrt{2}$ and $b_{n+1} = (a_{n+1}+a_{n+1}+2^{-n})/2 = a_{n+1}+2^{-(n+1)}$.

In both cases it is clear that $a_{n+1}$ and $b_{n+1}$ are rational.