[aleph_minus_one]

> So we're already halfway done with the proof.

Indeed the Cook-Levin theorem

> https://en.wikipedia.org/wiki/Cook%E2%80%93Levin_theorem

which actually proves that there exist NP-complete problems in NP is not a trivial result (and was at that time a highly surprising one).

So, indeed, "one half of the proof" has been done; the other half (which seems to be much harder) of P vs NP is still open.