Formal vs. informal proof that sqrt(2) is irrational

[Protoman2050]

What's the difference b/w a formal and an informal proof, in mathematics? I have an informal proof that sqrt(2) is irrational:

1. Assume sqrt(2)=x/y, where x and y are nonzero integers and relatively prime
2. ysqrt(2)=x
3. 2y^2=x^2
4. x=2z, since x^2 is even by this, since it is able to be divided by 2, and it and the lhs are equal
5. 2y^2=(2z)^2=4z^2
6. y^2=2z^2
7. According line 4, since x is even, y must also be even
8. But then they must both share a factor, 2. But this contradicts our assumption that x and y do not share a common factor
9. Therefore, sqrt(2) is irrational
Btw, is there a less messy version of this?

This is an informal proof, but what's the formal proof?

Thanks!

[Quatl]

EDIT: never mind my brain is dysfunctional today

[Zetetic11235]

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.