Formalization of Lemma for proof of AM-GM inequality

Question

The question is not about how to prove the lemma (I proved it by induction) but I wanted to understand the correct formalization of the lemma:

Lemma used to prove AM-GM inequality: If $ a_1,a_2,...,a_n $ are real and positive numbers satisfying $ a_1 \cdot a_2 \cdot ... \cdot a_n =1 $ then $ \sum_{k=1}^n a_k \geq n $.

My attempts at formalization:

1. $ \forall n \in {\bf{N}} \forall x_1 \in {\bf{R}} \forall x_2 \in {\bf{R}} ...\forall x_n \in {\bf{R}} ( ( x_1,x_2,...,x_n > 0 \land x_1 \cdot \cdot \cdot x_n = 1 ) \Rightarrow x_1 + ... + x_n \geq n ) $

2. $ \forall n\in \mathbb{N}\, \forall x_k\in \mathbb{R}_{>0}\,(k=1,\ldots,n)\, : \,\prod_{k=1}^nx_k =1\Longrightarrow \sum_{k=1}^nx_k\geq n $

3. $ (\forall n\in \mathbb{N})(\forall k \in \{1,2,\ldots,n\})(\forall x_k\in \{r\in \mathbb{R}\, : \,r>0\})\, : \, \prod_{k=1}^nx_k =1\Longrightarrow \sum_{k=1}^nx_k\geq n $

Are these formalizations correct?

Regarding (1): back when I proved the lemma I formalized it to (1) above, but I'm not sure if it is correct now logically ( after reading the following question : How to formalize $\text{span}(S)=\{c_1v_1+\cdots+c_kv_k\mid v_1,~\cdots,~v_k\in S,~c_1,~\cdots,~c_k\in F\}$ rigorously in first order language? ) since I have $ n $ quantifiers followed by the first quantifier ( $ \forall n \in \Bbb N $ ) where it is written " $ \forall n \in {\bf{N}} \forall x_1 \in {\bf{R}} \forall x_2 \in {\bf{R}} ...\forall x_n \in {\bf{R}} $ " ( and I think this is called 'not well-formed' in first-order logic )

Regarding (2): looks little bit awkward for a beginner like me, but it means the same thing as (3) which seems clearer.

Regarding (3): I'm not sure if it is a correct formalization, because in the induction step, where I assume the claim for $ n $ and prove it for $ n+1 $ then afterwards I'll also have to continue my proof like so: " Let $ k \in \{1,2,\ldots,n,n+1\} $ be arbitrary . Let $ x_k \in \{r\in \mathbb{R}\, : \,r>0\}\, $ be arbitrary " but then I'd stumble upon a difficulty when I'll have to assume $ \prod_{k=1}^{n+1} x_k =1$ since I've introduced only one arbitrary variable ( $ x_k $ ) and not $ n+1 $ arbitrary variables.

If you have other formalization that is correct, can you please write it very rigorously and precisely? ( I would like to know better how to formalize correctly regarding theories that discuses $ n $ number of mathematical objects )

Thanks in advance for any help!

Answer 1

1. Attempt (1) is perfectly fine, and the most standard among the three.
2. Attempt (2) is also fine, except that I would replace the colon (which normally is read “such that”, and in never necessary in the language of first-order logic) with a set of parentheses like in (1). Also, $\mathbb R^+$ is an alternative to $\mathbb R_{>0},$ and perhaps use different dummy variables $i$ and $k$ for the $\Pi$ and $\Sigma.$
3. In attempt (3), the declaration for $k$ feels pedantic. $\{r\in \mathbb{R}\, : \,r>0\}$ is simply $(0,\infty).$ The parentheses around each quantifier are unnecessary.

My own attempt: $$\forall n\in\mathbb N \;\;\forall a_1,\ldots,a_n\in\mathbb R^+ \,\Bigl(a_1\ldots a_n =1\implies a_1+\ldots+a_n \geq n\Bigr)$$ or $$\forall n\in\mathbb N \;\;\forall a_1,\ldots,a_n\in\mathbb R^+ \left(\prod_{j=1}^n a_j =1\implies \sum_{k=1}^n a_k \geq n\right).$$

P.S. Note that the parentheses are required here: the convention (quantifiers apply to as little as is construeable) is to read $$\forall n\in\mathbb N \;\;\forall a_1,\ldots,a_n\in\mathbb R^+ \prod_{j=1}^n a_j =1\implies \sum_{k=1}^n a_k \geq n$$ as $$\left(\forall m\in\mathbb N \;\;\forall b_1,\ldots,b_m\in\mathbb R^+ \prod_{j=1}^m b_j =1\right)\implies \sum_{k=1}^n a_k \geq n,$$ with the variables $n$ and $a_1,\ldots,a_n$ free.

P.P.S. Unlike parentheses, a colon is unable to indicate the scope of quantifiers.