Prove for all sequences $\{a_n\}$ and $\{b_n\}$, if $\lim a_n = a$ and $\lim b_n = b$, then $\lim a_n + b_n = a+b$ entirely in first-order logic I already know how to prove this statement in "English," but I would to see a proof of it entirely in first-order logic.  Here is the English proof:
(1) Let $\{a_n\}$ and $\{b_n\}$ be arbitrary sequences.
(2) Assume $\lim_{n\to\infty} a_n = a$ and $\lim_{n\to\infty} b_n = b$.
(3) This means for every $\epsilon_a >0$ there exists $N_a$ such that for every $n \in N$, if $n\geq N_a$, then $\left|a_n-a\right|< \epsilon_a$ and for every $\epsilon_b >0$ there exists $N_b$ such that for every $n \in N$, if $n\geq N_b$, then $\left|b_n-b\right|< \epsilon_b$.
(4) Now, let $\epsilon>0$.
(5) Since $\lim a_n = a$ and $\lim b_n = b$, there exists $N_a$ such that for every $n \in N$, if $n\geq N_a$, then $\left|a_n-a\right|< \epsilon_a= \epsilon/2$ and there exists $N_b$ such that for every $n \in N$, if $n\geq N_b$, then $\left|b_n-b\right|< \epsilon_b = \epsilon/2$.
(6) Choose $N=\max\{N_a, N_b\}$.
(7) Let $n$ be a natural number.
(8) Assume $n\geq N$.
(9) Notice that $\left|(a_n + b_n) - (a+b)\right| = \left|a_n + b_n - a - b\right| = \left|(a_n-a) + (b_n-b)\right|$.
(10) By the triangle inequality we have $\left|(a_n-a) + (b_n-b)\right|\leq \left|a_n-a\right| + \left|b_n-b\right|$.
(11) Since $N=\max\{N_a, N_b\}$, if $N=N_a$, then $N=N_a\geq N_b$. Also, since $n\geq N$, we have $n\geq N_a\geq N_b$.  So, $\left|a_n-a\right|< \epsilon/2$ and $\left|b_n-b\right|< \epsilon/2$.  The same result holds if $N=N_b$.
(12) So, we have $\left|(a_n + b_n) - (a+b)\right|=\left|(a_n-a) + (b_n-b)\right|\leq \left|a_n-a\right| + \left|b_n-b\right|<\epsilon/2 + \epsilon/2=\epsilon$.
(13) Finally, we can conclude that $\lim a_n + b_n = a + b$.  Q.E.D.
The first thing I would like to see is a formal line by line first-order logic proof of the above with each step justified.  I'm not sure how to translate the above with quantifiers and I'm not sure what order to present each step of the proof.
Also, recall step (5) where we have "for every $\epsilon_a >0$ there exists $N_a$..." and "for every $\epsilon_b >0$ there exists $N_b$..."  This step translates $\lim a_n = a$ and $\lim b_n = b$ using the definition of the limit.  Is it wrong to put subscripts on each $\epsilon$ and $N$ for $\lim a_n =a$ and $\lim b_n=b$?  I guess I don't understand why we need the subscripts.
 A: I won't answer your first question (mostly because it's tedious; not hard, just very tedious), but I will answer your second. 
You're absolutely justified in putting those different subscripts on the sequences, but it's important to understand why. One of those could be extremely badly behaved. Maybe $\{a\}_n^\infty$ bounces around between 1 and -1 for the first 1 million terms. Maybe the first billion. Maybe it is equal to $n^2$ for the first 10 billion terms, then turns into something convergent. 
The point is, it doesn't matter. We know that it converges, and so therefore, there is some $N_a$ and $\epsilon_a$ such that if we get far enough along ($N_a$) we'll be as close as we want ($\epsilon_a$). 
The sequence $\{b_n\}_{n=1}^\infty$ could be equally badly behaved, or much better (it could be constant, for example), but it doesn't matter. The fact that we know it converges means we don't care about the first $n$ terms. The $N_a$ and $N_b$ could be wildly different, but since they're finite we can always just take their max. This is the real heart of this proof: no matter how big two finite numbers are, their max is always finite. It's a more powerful statement than you would guess at first glance. 
You should be able to go line-by-line to turn this into first order logic. Again, it will be tedious...
