Also see https://math.andrej.com/2009/12/28/constructive-gem-irration... for a similar proof using 2^(log_2 3)