Correct way to denote things in logical notation (with quantifiers)? I am having trouble denoting things with quantifiers. For example, I'd like to define when a sequence is bounded from above. There is my definition:

Sequence $\{ a_n \}$ is bounded from above if and only if there exists a real number $K$ for which for every positive integer $n$ the following holds: $ a_n \leq K$

I'll try to use less words and more symbols...

Sequence $\{ a_n \}$ is bounded from above $ \iff \exists K \in \mathbb{R} \implies \forall n \in \mathbb{N} \setminus {0} \implies a_n \leq K $

But sometimes, I see things like this:

Sequence $\{ a_n \}$ is bounded from above $ \iff \left( \exists K \in \mathbb{R} \right) \left( \forall n \in \mathbb{N} \setminus {0} \right) \implies a_n \leq K $

I assume there is an "and" hidden between the parentheses. 
What would be correct? I am confused.
 A: You don't write the $\implies$ after the quantor.
The correct syntax is $\forall x : \phi(x)$ where $\phi(x)$ is a correct statement. Ditto $\exists x: \phi(x)$
We also use $\forall x \in A: \phi(x)$ as a shortcut for
$\forall x:( (x \in A) \implies \phi(x))$ and $\exists x \in A: \phi(x)$ for 
$\exists x: ((x \in A) \land \phi(x))$
The $\implies$ stands between statements, so it's always used in ($\phi \implies \psi$)-like statements (with an antecedent and a consequent).
So if $f: X \to \mathbb{R}$ is a function,we can write $f$ is bounded above by
$$\exists K \in \mathbb{R}: (\forall x \in X: (f(x) \le K))$$ with some "superfluous" brackets (being a bit formal). As a real-valued sequence is just a function from $\mathbb{N}\setminus\{0\}$ to $\mathbb{R}$, the above applies to sequences as well, changing $X$ to $\mathbb{N}\setminus\{0\}$ and $f(n)$ to $a_n$ if you prefer.
A: There is no such thing as an implication in your statement hence you cannot write $\Rightarrow$ somewhere. An implication would be appropriate if your statement contains an 'if' in some form somewhere e.g.

For all natural numbers a,b,c it holds that if a and b are greater or equal than c then the sum of a and b is already greater than c.
$\forall a,b,c \in \mathbb{N}_{\geq0}: (a \geq c \land b \geq c)\Rightarrow (a+b \geq c)$

If you know what you are talking about you can leave out the brackets.
I would write

Let $R_f$ be $\dots$ . The sequence $\{ a_n \}$ is bounded from below if and only if
$\exists K \in R_f : \forall n \in \mathbb{N}_{\geq0}: a_n \leq K$

You can read the colons as 'such that' or 'for which...'
If you are lazy you can also leave out the colons.
If you want to clarify that it is a definition or shorten your definition you can do this

Sequence $\{ a_n \}$ is bounded from below $:\Leftrightarrow$ ...

or

Sequence $\{ a_n \}$ is bounded from below $\stackrel{def}{\Leftrightarrow}$ ...

