The definition of iterated product is the easy part of the proof, the bottleneck is elsewhere. Even quite weak theories of bounded arithmetic, such as PV (this is an open theory with function symbols for polynomial-time functions), can prove that the product of a sequence of natural numbers exists (and is divisible by each element of the sequence), by formalizing the usual inductive definition in a straightforward way.
The next thing you need is to show that every number greater than one is divisible by a prime. PV is not known (and not expected) to prove this, but it is provable in the slightly stronger theory $S^1_2$.
Thus, $S^1_2$ can formalize Euclid’s proof as the statement “there is no sequence containing all primes”.
As Carl noted, this is not a very natural rendering of the statement “there are infinitely many primes” (especially in weak theories, where sequences can only have logarithmic length). The statement one really wants to prove is “the set of primes is unbounded”. In order to infer this from Euclid’s proof, you need the principle that any bounded set can be put in a sequence, and this is equivalent to the axiom that exponentiation is total. Thus, formalization of Euclid’s proof in this sense can be done in $I\Delta_0+\mathrm{EXP}$ (and a fortiori in very strong theories like PRA).
It is possible to prove that there exist unboundedly many primes in theories weaker than $I\Delta_0+\mathrm{EXP}$, but this requires a much more elaborate proof than Euclid’s. Paris, Wilkie and Woods have shown the unboundedness of primes in the theory $I\Delta_0+\Omega_1$ (where $\Omega_1$ roughly says that $x^{\log x}$ exists for every $x$), and more precisely, in its subtheory $I\Delta_0+\mathrm{WPHP}(\Delta_0)$ (the latter is the weak pigeonhole principle: there is no $\Delta_0$-definable injection from $[0,2x]$ to $[0,x]$). It can be seen that their proof actually goes through in the theory $S^1_2+\mathrm{rWPHP}(\Theta)$ (itself included in $T^3_2$ and $S^4_2$), where $\Theta$ is the set of provably total $\Sigma^b_2$-definable functions of $S^1_2$ (which coincides with functions from the complexity class $\mathrm{FP}^{\mathrm{NP}[\mathrm{wit},\log n]}$), and $\mathrm{rWPHP}(\Theta)$ is a version of WPHP where the injection is supplied with an explicit retraction, both coming from $\Theta$. To the best of my knowledge, this is the weakest theory known to prove the unboundedness of primes.
To add to quid's suggestion (look around Michel Waldschmidt's webpage), I'd say specifically that Waldschmidt's slides on Schanuel's conjecture are probably worth looking at. This may be more for one's general education about transcendental number theory than any suggestion for research, since Schanuel's conjecture is widely regarded as a Holy Grail of transcendental number theory, and a proof seems to be nowhere in sight. It is, however, quite beautiful!
Best Answer
The infinitude of primes (more precisely, the existence of arbitrarily large primes) might actually be necessary to prove the transcendence of $\pi$. As I explained in an earlier answer, there are structures which satisfy many axioms of arithmetic but fail to prove the unboundedness of primes or the existence of irrational numbers. Shepherdson presented a simple method for constructing such models, I will present such a model where $\pi$ is rational!
The Shepherdson integers $S$ consist of all Puiseux polynomials of the form $$a = a_0 + a_1T^{q_1} + \cdots + a_kT^{q_k}$$ where $0 < q_1 < \cdots < q_k$ are rationals, $a_0 \in \mathbb{Z}$, and $a_1,\dots,a_k \in \mathbb{R}$. This is a discrete ordered domain, where $a < b$ iff the most significant term of $b-a$ is positive; this corresponds to making $T$ infinitely large. This ring $S$ satisfies open induction axioms $$\phi(0) \land \forall x(\phi(x) \to \phi(x+1)) \to \forall x(x \geq 0 \to \phi(x))$$ where $\phi(x)$ is a quantifier free formula (possibly with parameters). So the ring $S$ satisfies the same basic axioms as $\mathbb{Z}$, but only a very limited amount of induction. In the field of fractions of $S$, $\pi$ is equal to the ratio $\pi T/T$. In other words, $\pi$ is a rational number!
Is $\pi T/T$ really $\pi$? The integers form a subring of $S$, and if $p,q \in \mathbb{Z}$ then $p/q < \pi T/T$ in $S$ if and only if $p/q < \pi$ in $\mathbb{R}$. So $\pi T/T$ defines the same Dedekind cut as $\pi$ does, which is a very accurate description of $\pi$. Indeed, any proof of the transcendence of $\pi$ must ultimately be based on the comparison of $\pi$ and its powers with certain rational numbers, which $\pi T/T$ will accomplish just as well as the real number $\pi$. However, the usual definitions of $\pi$ are not easily formalizable in this basic theory, so there is much room for debate here and I wouldn't claim that $\pi T/T$ satisfies all reasonable definitions of $\pi$. Shepherdson only presented this argument for real algebraic numbers like $\sqrt{2}$, which have a finitary description in this theory and leave little room for debate. In any case, the conclusion to draw from this is that basic arithmetic with open induction does not suffice to prove that $\pi$, or any other real number, is irrational (never mind transcendental).
What about primes? In the ring $S$, the only primes are the ones from $\mathbb{Z}$. Although there are infinitely many primes in $S$, it is not true that there are arbitrarily large primes. For example, there are no primes larger than $T$. Thus $S$ is a model where the unboundedness of primes fails and so does the irrationality of $\pi$. This only shows that basic arithmetic with open induction does not suffice to prove either result. A possible line of attack to show that the unboundedness of primes is necessary to prove the transcendence of $\pi$ would be to show that the minimum amount of induction necessary to prove that $\pi$ is transcendental also suffices to prove the unboundedness of primes. Unfortunately, I do not know how much induction is necessary to prove the transcendence of $\pi$. (And the minimum amount of induction necessary to prove the unboundedness of primes is still an open problem.)
Well, here is a partial answer, which is a bit of a bummer. There is another Shepherdson domain $S_0$ similar to the above where $\pi$ is transcendental over $S_0$ and $S_0$ does not have arbitrarily large primes. This shows that the transcendence of $\pi$ does not imply the unboundedness of primes over basic arithmetic with open induction. The ring $S_0$ is the subring of $S$ where the coefficients of the Puiseux polynomial are restricted to be algebraic numbers. The unboundedness of primes fails in $S_0$ because the real algebraic numbers form a real closed field just like $\mathbb{R}$. The number $\pi$ is transcendental over $S_0$ because it is transcendental over the field of real algebraic numbers.
This is not entirely surprising since open induction is a very weak base theory and the Shepherdson type rings are very pathological. To constrain such pathologies Van Den Dries suggested requiring that the domain is integrally closed in its field of fractions; he called such domains normal but I don't know if this is standard terminology. Neither $S$ nor $S_0$ are normal. More convincing examples would be normal discrete ordered domains. The methods of Macintyre and Marker (Primes and their residue rings in models of open induction, MR1001418) suggest that normal analogues of $S$ and $S_0$ might exist.
The conclusion that I draw from this is that open induction is probably too weak a base theory to study this question. Stronger base theories run into the difficulty that it is still not known just how little induction is necessary to prove the unboundedness of primes. The next reasonable candidate is bounded-quantifier induction (IΔ0), which is not known to imply the unboundedness of primes. Using the Euler product $\pi^2/6 = \prod_p (1-p^{-2})^{-1}$ looks promising, but so far I can only make sense of this product in IΔ0 + Exp which is known to prove the unboundedness of primes.