Why do we ever bother to translate bits of mathematical English into the symbolism of first-order logic?
Primarily because the quantifier-variable plus connectives representation of statements is wonderfully clear and non-ambiguous about logical structure. Careless or sloppy vernacular talk may fail to distinguish between the propositions represented by $P \lor (Q \land R)$ and $(P \lor Q) \land R$ [Recall the ambiguous invitation: "Bring your partner or come alone and have a good time!"]. Logical notation forces us to distinguish, as it also forces us to distinguish $\forall x \neg Px$ and $\neg\forall xPx$ [compare the ambiguous "Everyone has not yet arrived"], and to distinguish $\forall x\exists yRxy$ and $\exists y\forall xRxy$, and so on and so forth.
So the key thing in rendering statements of mathematical English into the notation of first-order logic is to do enough to make logical structure perspicuous (in particular do enough to reveal the scope of various logical operators, i.e. to reveal just which bits of the proposition they govern). In this case, the statement after the colon has something like this sort of logical shape
$$\exists n\forall s[l(s)\geq n \to \exists x\exists y\exists z(s = x^{\cap}y^{\cap}z \land y \neq 0 \land \forall i\,x^{\cap}y^i{}^{\cap}z \in L )]$$
if we take the quantifiers to be implicitly appropriately sorted so $s, x, y, z$ run over $L$-strings, and $n$ and $i$ over non-negative numbers (and where ${}^{\cap}$ is concatenation). The further finer details (e.g. whether you choose to explicitly type the variables by writing e.g. $\forall x \in L$ where $L$ is the set of $L$-strings) won't matter -- in most contexts -- so much as revealing the overall quantificational structure and scope dependencies.
I hope this helps ...