formalization - reducing a theorem to set theory using first order logic

Deducing a non-trivial theorem directly from ZFC is a tedious business. First you will need to define the integers in terms of sets. The natural numbers are most commonly encoded as von Neumann ordinals. Then you have to define addition and multiplication. These are functions, which are typically encoded as sets of ordered pairs from $mathbb{N}timesmathbb{N}$ to $mathbb N$. An ordered pair is typically encoded as $(x,y) := lbracelbrace xrbrace,lbrace x,yrbracerbrace$. Then you will have to define primes, etc.

If you really want to go through this exercise, then I would recommend learning Mizar, which is a system for formal proofs. Mizar is based on Tarski-Grothendieck set theory, which is a slight extension of ZFC. Most of the groundwork that I've described above has already been done by previous users of Mizar, so that you just need to "drill down" through the existing definitions in order to figure out how to do things, and don't have to encode it all from scratch yourself.