# is this predicate logic statement correct for this indirect proof?

Just for context, my goal is to prove the square root of 2 is an irrational number. I already did this using proof by contradiction both algebraically and geometrically, however, I want to begin the proof writing the original premise in predicate logic (or first-order logic).

So we know if we were to assume the square root of two is rational, we would write it as $$\sqrt2 = \frac{a}b$$ such that $$a$$ and $$b$$ are relatively prime and $$b\ne0$$ But how would I state this in logical form? Currently I have $$(\forall\mathbb{R}(a \land b\iff \frac{a}{b} \ne 2\cdot\mathbb{Z})\implies\mathbb{Q}(\sqrt2 ))$$

What I'm trying to say is something like "For all real numbers a and b if and only if the quotient of a and b is not equal to 2 times some integer, then the square root of 2 is rational"

Is my translation correct?

You could write it compactly like $$\exists p\exists q(p^2=2q^2)$$ where the domain is the natural numbers. This way you don't even need to talk about irrational numbers or square roots, or even division and rationals explicitly, only natural numbers and multiplication on natural numbers.