Technically, this is a proof that the positive rationals are not closed under exponentiation. If we do not care about closure under exponentiation, we do not have to assume the existence of the irrationals in the algebraic structure we are working with.