The Famous problem of Antiquity

Here is a gist of a proof, I think, (some gaps are left for you to fill in):

We require that both sequences be real. So for each $n > 0$ , $a_n, b_n$ must be such that there exist reals $a_{n+1}, b_{n+1}$ such that the two recursive equalities are met. Using that $x+y=A, x y =1$ has a real solution iff $|A| \geq 2$ , we determine that $(a_n + b_n)^4 \geq 2^8 (a_n b_n)$ , i.e., $(a_1+b_1)^4 \geq 2^8 2^{4(n-1)} (a_1 b_1)^{2^{1-n}}$ for all $n > 0$ . If $a_1 b_1 \neq 0$ , then $(a_1 b_1)^{2^{1-n}} \rightarrow 1$ as $n \rightarrow \infty$ . But then $(a_1+b_1)^4 \geq 2^8 2^{4(n-1)} (a_1 b_1)^{2^{1-n}}$ is a contradiction, since the right side grows to $\infty$ as $n \rightarrow \infty$ . Thus, $a_1 b_1 = 0$ . $a_1 > 0,$ so $b_1 = 0$ . In order for $b_{2016} = 1$ , at some $m \leq 2016$ , we must have $b_m \neq 0$ . For example, we can take $a_1 = 2^{2015}, b_1 = 0, a_m = 0, b_m = a_1/(2^{m-1})$ for $m \geq 2$ . No matter where we choose to switch $a_m$ to zero and $b_m$ to nonzero, we must have $a_1 = 2^{2015}$ .