Why haven't mathematicians come up with an efficient way of writing “sufficiently”, e.g. “for $n$ sufficiently large” Consider a typical proof in an introductory analysis course:

Claim: Let $(x_n)_\mathbb{N}$ and $(y_n)_\mathbb{N}$ be convergent sequences in $\mathbb{R}$ (or $\mathbb{C}$) and let $x,y$ be their respective limits. Then $(x_n+y_n)_\mathbb{N}$ is convergent and its limit is $x+y$.
Proof: Let $\varepsilon >0$. There exists $n_1$ resp. $n_2$ such that $$\forall n \geq n_1, |x_n-x| < \varepsilon/2$$ resp. $$\forall n \geq n_2, |y_n - y| < \varepsilon/2.$$ Let $n_0 = \max(n_1,n_2).$ The triangle inequality implies that $$\forall n \geq n_0, |(x_n + y_n) - (x+y)| \leq |x_n - x| + |y_n - y| < \varepsilon/2 + \varepsilon/2 = \varepsilon.$$ This proves the claim.

As a first-year student, this is a proof structure that comes up a lot. And yet, a significant portion of it seems redundant. Namely, the actual value of $n_0$ that I chose is of almost no significance. I could just as well have chosen $n_1 + n_2$ or $\max(n_1,n_2)+52.$
The only thing that's important is that $n_0$ be greater than both $n_1$ and $n_2$, which is necessarily possible due to the fact that $\mathbb{N}$ is totally-ordered and not bounded above.
This remark has led me to come up with a notation which I use extensively in my notes and saves me vast amounts of ink. This notation is the following:

I define the notation $\mathbb{N}^\infty$ to mean “any set of the form $\mathbb{N}\setminus \left\{0,\ldots,n_0\right\}$ where $n_0 \in \mathbb{N}$. (The $\infty$-symbol is supposed to symbolise “sufficiently close to infinity”.) Like little-oh and big-oh notation, $\mathbb{N}^\infty$ does not refer to a specific object but rather a generic object with a certain property. However, $\mathbb{N}^\infty$ sets have the following useful property: any finite intersection of $\mathbb{N}^\infty$ sets is $\mathbb{N}^\infty$. (This is kind of like how any finite sum of $o(f)$ functions is $o(f).$)

The last property has the following consequence:

Let $P_1,\ldots,P_k$ be predicates on $\mathbb{N}.$ Suppose that for all $i=1,\ldots,k$ we have $$\forall n \in \mathbb{N}^\infty,P_i(n) \textrm{ is true}.$$ Then $$\forall n \in \mathbb{N}^\infty, (P_1(n)\wedge\ldots\wedge \ P_k(n)) \textrm{ is true}$$
This is just a fancy way of saying “If, in a finite set of predicates, each predicate is true for sufficiently large $n$, then for sufficiently large $n$, each predicate is simultaneously true.” Note that this fails if the number of predicates is infinite.

Using this notation, the definition of the limit can be written as follows:

We say that $(x_n)_\mathbb{N}$ tends to some number $x$ iff for all $\varepsilon >0,$ $$\forall n \in \mathbb{N}^\infty, |x_n - x| < \varepsilon.$$

Using the property that I just stated, proof I gave above can also be rewritten:

Proof: Let $\varepsilon >0$. Then $$\forall n \in \mathbb{N}^\infty,|x_n - x| < \varepsilon/2$$ and $$\forall n \in \mathbb{N}^\infty,|y_n - y| < \varepsilon/2$$ hence by the triangle inequality, $$\forall n \in \mathbb{N}^\infty,|(x_n+y_n) - (x+y)| < \varepsilon.$$

Not only is this version more concise, but in my opinion it is better from a pedagogical point of view. When a student unfamiliar with analysis reads the first version (see above), there is some chance that we will be side-winded by the construction of $n_0$ (which as I said bears little to no importance), and he will be detracted from the actual crux of the proof which is the use of the triangle inequality. On the other, if the same student reads the second version, assuming that he understands the notation, he won't be side-winded by information that is not strictly necessary to his conceptual understanding of the proof. Finally, and perhaps most importantly, there is no loss in rigour in using the $\mathbb{N}^\infty$ notation provided that the “rules of the game” are well-understood.
In a similar vein, for functional limits I use the notation $I^a$ (where $I$ is an interval and $a$ is in the closure of $I$) to signify “the intersection of $I$ with some open interval centred around $a$”. Here, the $a$ in the exponent is intended to symbolise “sufficiently close to $a$”. We again have the property that any finite intersection of $I^a$ sets is $I^a$.
In a way that is similar to the above, this notation allows us to simplify definitions and proofs in a way that is in my opinion non-negligeable and pedagogically fruitful.
Finally, I would like to ask:

Since the notions of “sufficiently large” and “sufficiently close to” are so ubiquitous in analysis, why haven't mathematicians come up with a way to convey them efficiently?

 A: It's good that you're trying to make things easier and clear. But I don't think the notation $\mathbb{N}^\infty$ is a good one: to me, it looks like $\mathbb{N}\cup \{\infty\}$.
Unfortunately, inventing good notation that becomes widely used is very rare. Witness the Iverson bracket, which is very nice but never really caught on, even when championed by Knuth, no less. On the other hand, Landau's Big O notation was mainly restricted to analysts when it was brought to the masses by computer scientists in the analysis of algorithms.
The truth is that nothing beats good, clear, words.
The same proof with words looks to me both efficient and clear:

Proof: Let $\varepsilon >0$. Then, for $n$ sufficiently large, $$|x_n - x| < \varepsilon/2$$ and $$|y_n - y| < \varepsilon/2$$ Hence, by the triangle inequality, for $n$ sufficiently large, $$|(x_n+y_n) - (x+y)| < \varepsilon.$$

I've seen the notation like "$n \gg 1$" used for "$n$ sufficiently large", but I don't think it's clear in writing. It may work on the blackboard.
A: What follows is a slightly edited MathJax version of my 21 December 2004 sci.math post Generalized Quantifiers that discusses a way to economize the writing of some of the things you’re asking about.
Let $\exists^{\infty}$ mean "there exist infinitely many" and let $\forall^{\infty}$ mean "for all but finitely many".
These are the "there exists" and "for all" quantifiers modulo the smallness notion "finite". Other notions of smallness could be considered, such as countable, meager (= first Baire category), and Lebesgue measure zero. Of course, to use the latter two notions we need the variables being quantified over to belong to spaces where these notions make sense.
Negation $\sim$ distributes through these new quantifiers the same way it distributes through $\exists$ and $\forall :$
$$ (\sim)\left(\exists^{\infty}\right) \;\;\; \text{is the same as} \;\;\; \forall^{\infty}(\sim) $$
and
$$ (\sim)\left(\forall^{\infty}\right) \;\;\; \text{is the same as} \;\;\; \exists^{\infty}(\sim) $$
It follows that the negation of a finite sequence of such quantifiers can be rewritten using the same method that one can use to rewrite the negation of a finite sequence of ordinary quantifiers, namely switch all the $\exists$'s to $\forall$'s and switch all the $\forall$'s to $\exists$'s, and then take the negation of the right-most expression.
We can often use these new quantifiers to give shorter definitions, such as $``x_n$ converges to $L"$ can be expressed as
$$(\forall \epsilon >0)\left(\forall^{\infty} n\right)(|x_n - L| < \epsilon).$$
The negation of this can be carried out formally in the way I described above. Thus, $``x_n$ does not converge to $L"$ becomes
$$(\exists \epsilon >0)\left(\exists^{\infty} n\right)(|x_n - L| \geq \epsilon).$$
For another example, the $\liminf$ of a sequence $\{A_n\}$ of sets is $\{x: \; \left(\forall^{\infty} n\right)(x \in A_n)\}$ and the $\limsup$ of the sequence $\{A_n\}$ of sets is $\{x: \; \left(\exists^{\infty} n\right)(x \in A_n)\}.$
In these and in other ways, I found the $\exists^{\infty}$ and $\forall^{\infty}$
quantifiers quite useful in a graduate real analysis class that I taught in 2001.
For the ordinary quantifiers we have the following logical strength chart in which no implication can be reversed (in general):
$$ (\forall)(\forall) \implies  (\exists)(\forall)  \implies  (\forall)(\exists) \implies  (\exists)(\exists) $$
The analogous chart also holds for $\exists^{\infty}$ and $\forall^{\infty}:$
$$ (\forall^{\infty})(\forall^{\infty}) \implies  (\exists^{\infty})(\forall^{\infty})  \implies  (\forall^{\infty})(\exists^{\infty}) \implies  (\exists^{\infty})(\exists^{\infty}) $$
I have not investigated the logical relationships for various sequences of these four quantifier types, but I have noticed that $\forall^{\infty}$ does not commute with $\forall$ (and hence by considering negations, $\exists^{\infty}$ does not commute with $\exists .$
More specifically, $\;(\forall^{\infty})(\forall)\;$ is strictly stronger than $\;(\forall)(\forall^{\infty}).\;$ For example, note that $\;(\forall x \in {\mathbb R})(\forall^{\infty} n \in {\mathbb N})(x < n)\;$ is true and $\;(\forall^{\infty} n \in {\mathbb N})(\forall x \in {\mathbb R})(x < n)\;$ is false. The underlying issue is that in order for $\;(\forall^{\infty} r)(\forall s)\;$ to be true, we need the existence of a co-finite collection of $r$'s each of which uniformly works for every $s.$ Indeed, for the example I gave, we do not even have a single $r$ that uniformly works for each $s.$
The distinction between $\;(\forall^{\infty})(\forall)\;$ and $\;(\forall)(\forall^{\infty})\;$ is really a $(\exists)(\forall)$ verses $(\forall)(\exists)$ distinction if you look at things the right way. Let $C$ be a variable that runs over the set of co-finite collections of $r$'s. Then $\;(\forall^{\infty} r)(\forall s)\;$ becomes $\;(\exists C)(\forall r \in C)(\forall s),\;$ which is equivalent to $\;(\exists C)(\forall s)(\forall r \in C),\;$ whereas $\;(\forall s)(\forall^{\infty} r)\;$ becomes $\;(\forall s)(\exists C)(\forall r \in C).\;$ Note we have $\;(\exists C)(\forall s)\;$ in the former and we have $\;(\forall s)(\exists C)\;$ in the latter.
I have not tried to develop these ideas into a general framework, meaning quantifiers modulo various notions of smallness and how they logically relate to each other relative to how the various notions of smallness relate to each other, besides observing trivial things like the weaker the notion of smallness (e.g. Lebesgue measure zero is weaker than countable, which in turn is weaker than finite), then the stronger and weaker are the corresponding versions of $\exists$ and $\forall.$
A: They have: the phrase for sufficiently large $n$ is agreed to be both clear and word efficient. Perhaps first year students underestimate the amount of writing that is sometimes required in proofs.
Add 

Not only is this version more concise, but in my opinion it is better from a pedagogical point of view.

No, in my experience abusing symbols simply helps in confusing students and makes their write up messy and unclear. Students and professors are humans and are quite good at using words when communicating, and this should not be forgotten when learning mathematics. 
A: Your question, with its focus on $n_0$, seems to express a hidden concern with existentially quantified statements $\exists x \in X \,\, P(x)$ and their proofs. To explain what I mean by this, let me write out the definition of convergence making the existential quantifier explicit:


*

*$(x_n)_{\mathbb N}$ converges to $L$ if and only if $\forall \epsilon > 0$ $\exists n_0 \in \mathbb{N}$ such that $\forall n \ge n_0$, $|x_n-L|<\epsilon$.


Concerning proofs which use this definition, you write "The actual value of $n_0$ that I chose is of almost no significance". 
I think you are underplaying the key role of existential statements in mathematics. The value of the object whose existence you are trying to verify is of a very high significance: if you choose it wrong then what you are trying to prove about that object is false. To see this in a more extreme example, imagine picking the wrong $x$ when attempting to prove the statement "$\exists x \in \mathbb{R}$ such that $x^2=2$".
It so happens that in proving limit statements, there's only finitely many wrong choices of $n_0$, and infinitely many right choices. And yes, once one has made a correct choice, any other correct choice could have been made. But the key thing here is that you must make a choice. That is forced on you by the nature of the existential quantifier. To prove $\exists x \in X \,\, P(x)$, I want you to show me the $x$, and to verify for me that $P(x)$ is true with that value that you showed me. Then and only then will I accept that you have proved the statement.
