EDIT: never mind my brain is dysfunctional today

that is the formal proof. n/m=2^(1/2) where n,m are elements of Z the set of integers. n/m must be irreducible and thus n & m must not both be even.

(n/m)^2 = 2 --> n^2=2(m)^2 thus n^2 must be divisible by 2 and thus it is divisible by 4 as any even square must be divisible by 4 as one of the prime divisors of its root must be two. Thus two can be divide out of n^2 and it will still be even thus so will m^2 since m^2=(n^2)/2 and n^2/2 is even thus so is m^2. A contradiction. I cannot write it in FOL due to symbol notation not being availible.

The case of an irrational times a rational being irratoin is as follows:

N=irrational P= rational p=n/m where n,m are in z (set of integers)
N*n/m=(Nn)/m. Assume NP is rational NP=n'/m' thus (Nn)/m=n'/m'
Thus N=(n'm)/(m'n) where n'm and m'n are in z thus N is rational, a contradiction.

I can also give one for a rational plus an irrational is always irrational. The first is from the Rudin texts so you will have a tough time finding a more formal proof. I suppose you could argue form the peano axioms, but it would only involve showing everything from propositions derived from the axioms, which are stated in the rudin book Principles of Mathematical Analysis. Proofs like this ammount to pretty simple algebraic manipulations combined with propositions.