This is going to be hard to make precise, because it depends on details of the proof theory, but here I'm considering a foundation of ZFC just after constructing the real numbers as a complete ordered field, and the rational numbers as a subset of the reals. From such a basis, what is the shortest proof of that there exists an irrational number?
Here are some other statements from which the result follows easily:
- The rational numbers are not complete.
- The rational numbers are countable and the real numbers are not.
- There is a real number $x$ such that $x^2=2$, and no rational number can have this property.
If there are methods other than the countable/uncountable proof or $\sqrt 2\not\in\Bbb Q$ that you think can be done with a shorter proof from the axioms, I would also be interested to hear.
Remember not to assume too much here. All of the proofs mentioned here are hiding some significant complexity: proving that the real numbers are uncountable requires constructing a cantor-set-like family of infinite series; proving that $\sqrt 2$ exists requires the construction of the square root function via the babylonian method or similar. I'm curious if there is some clever manipulation of the complete ordered field axioms that directly leads to the existence of an irrational number without the detours.