What is the shortest proof that there is an irrational number? 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.
 A: I'm not sure if this is the shortest approach, but proving that $\sqrt 2$ is irrational doesn't require too much effort. First, prove that no rational squares to $2$. Then, define the set
$$
E=\{x\in\Bbb Q:x<0\text{ or }x^2<2\} \, .
$$
(Those familiar with the construction of the reals will recognise $E$ as the Dedekind cut of $\sqrt 2$.)
This set does not have a supremum in the rationals: if $r\in\Bbb Q$ is an upper bound of $E$, then $s=(2r+2)/(r+2)$ is a smaller upper bound of $E$. Proof that $s$ is an upper bound of $E$:
$$
\left(\frac{2r+2}{r+2}\right)^2-2=\frac{2(r^2-2)}{(r+2)^2}>0 \, .
$$
Proof that $s<r$:
$$
\frac{2r+2}{r+2}=r-\frac{r^2-2}{r+2}<r \, .
$$
Since the reals have the least upper bound property, and $E$ is obviously non-empty and bounded above, $E$ must have a supremum in $\Bbb R$. And since $E$ does not have a supremum in $\Bbb Q$, this supremum must be irrational.
Remark: this approach doesn't actually prove that $(\sup E)^2=2$, but since we are given the ordered field axioms for free, it is not too much work to prove this. In the comments, user21820's outlines one possible approach. Below, I offer another way of showing that there is a real number which squares to $2$.
Using the least upper bound property of $\mathbb R$, we can prove that if a sequence which is increasing and bounded above, then its supremum is its limit. Now consider the sequence $(a_n)_{n\in\mathbb N}$ given by $a_0=1$, and
$$
a_{n+1}=\frac{2a_n+2}{a_n+2} \, .
$$
It can easily be proven by induction that this sequence is increasing and bounded above. Let $l=\lim_{n\to\infty}a_n$. We have
$$
l=\lim_{n\to\infty}a_{n+1}=\lim_{n\to\infty}\frac{2a_n+2}{a_n+2}=\frac{\lim_{n\to\infty}2a_n+2}{\lim_{n\to\infty}a_n+2}=\frac{2l+2}{l+2} \, ,
$$
and so $l^2+2l=2l+2$, meaning that $l^2=2$. Since $(a_n)_{n\in\mathbb N}$ is a positive sequence of terms, we see that $l$ equals the positive square root of $2$.
A: Suppose $\log_2 3 = \dfrac m n$ for some $m,n\in\{1,2,3,\ldots\}.$
Then $2^m = 3^n,$ so an even number equals an odd number.
Now consider the set of all positive fractions $m/n$ for which $2^m<3^n$ and the complementary set for which $2^m>3^n.$
A: I realized that in your case there is a better approach than Joe's answer. Since you have the full completeness axiom, you should not apply it to a set of rationals. Rather, you should apply it to $E = \{ x : x∈ℝ ∧ x^2 < 2 \}$. Then you can much more easily prove that its supremum $t$ satisfies $t^2 = 2$, without any further use of the completeness axiom in any form (including the archimedean property).
$
\def\lfrac#1#2{{\large\frac{#1}{#2}}}
$
Sketch: Clearly $1 ∈ E$ and $E ≤ 2$, so let $t = \sup(E)$. If $t^2 > 2$, then $\big(t-\lfrac{t^2-2}{2t}\big)^2$ $=2+\big(\lfrac{t^2-2}{2t}\big)^2 > 2$, so $t-\lfrac{t^2-2}{2t}$ is a smaller upper bound for $E$ than $t$. $t^2 < 2$, then $\big(t+\lfrac{2-t^2}{3t}\big)^2$ $= t^2+\lfrac{2-t^2}{3t}·\big(2t+\lfrac{2-t^2}{3t}\big)$ $< t^2+\lfrac{2-t^2}{3t}·3t = 2$ because $\lfrac{2-t^2}{3t}$ $< \lfrac{4t^2-t^2}{3t}$, so $t+\lfrac{2-t^2}{3t} ∈ E$ contradicting definition of $t$.
A: I really like this short elementary proof that $e$ is irrational given by A. R. G. MacDivitt and Yukio Yanagisawa (The Mathematical Gazette , Volume 71 , Issue 457 , October 1987 , pp. 217, DOI: https://doi.org/10.2307/3616765)
Step 1: Suppose $e$ is rational; $e$ being defined by the infinite sum, $\sum_{k=0}^\infty \frac{1}{k!}$; that is:
$$\sum_{k=0}^\infty \frac{1}{k!}=\frac{m}{n}\tag{1},$$
where $m$ and $n$ are positive integers.
Step 2: Multiply both sides of (1) by $n!$, thus
$$n!\left(1+\frac{1}{1!}+\frac{1}{2!}+\frac{1}{3!}+...+\frac{1}{n!} \right)+\frac{1}{(n+1)}+\frac{1}{(n+1)(n+2)}+...=n!\,\frac{m}{n}\tag{2}$$
so that $S=\frac{1}{(n+1)}+\frac{1}{(n+1)(n+2)}+...$ is a positive integer, with $nS\ge1$.
Step 3: Construct contradiction.
$nS\ge1$ can be written $(n+1)S-1\ge S$, implying that
$$\frac{1}{(n+2)}+\frac{1}{(n+2)(n+3)}+...\ge \frac{1}{(n+1)}+\frac{1}{(n+1)(n+2)}+...;$$
which after comparing both sides of the inequality term by term can immediately seen to be a contradiction.
