I have a problem that I know how to solve logically, but I can not seem to be able to write the statement of the theorem in predicate form. The exact statement is as follows.
$$\text{For every } n \in \mathbb{N}, \text{ if } n \ge 1 \text{ then } 2^{2^n} - 1 \text{ is divisible by at least } n \text{ distinct primes.}$$
I began trying to write the statement in predicate form as follows.
$$\forall n \in \mathbb{N},\ n \ge 1 \implies \textit{<something here referencing each distinct prime } p_i \text{>},\ p_i\ |\ 2^{2^n} - 1$$
I do not, however, know what to put in the angled brackets. I think it might use something along the lines of $\operatorname{gcd}$ to make sure each prime is distinct, but I do not know how to check that the prime is distinct and iterate over each prime in the predicate.
The simplest is probably
$$\forall n \in \mathbb{N},\ n \ge 1 \implies \mathrm{card} \;\{p \;|\; p \textrm{ is prime} \wedge p\,|\, 2^{2^n} - 1 \} \ge n$$
But to write "$p \textrm{ is prime}$" more formally, you would need something like:
$$p\in \Bbb N \wedge p\gt1 \wedge \left[\forall k, (k\in\Bbb N \wedge k\ge 1 \wedge k\,|\,p)\implies (k=1\vee k=p)\right]$$
You could also write for the whole sentence:
$$\forall n \in \mathbb{N},\ n \ge 1 \implies \exists\, p\in\Bbb N^n, (\forall i \in\Bbb N, 1\le i\le n \implies p_i>1 \wedge p_i\,|\,2^{2^n}-1) \wedge (\forall i,j \in \Bbb N, 1\le i<j\le n\implies p_i\wedge p_j=1)$$
(here I use the same $\wedge$ for "logical and" and GCD, so it may look awkward)
However, the latter does not state that the $p_i$ are primes. But it's not really a problem if you consider they are pairwise coprime, hence their prime factors are distinct.