How to avoid getting bogged down in details in proofs?

Question

I was trying to prove that (the slow version of) Euclid's algorithm is correct when I realized that I had to prove that gcd(a,b) = gcd(a-b,b) for a>b. I then I realized that I had to prove that when a=b gcd(a,b)=a.

It seems intuitively obvious that the gcd of a number with itself is just that number itself, since a number obviously divides itself. But I realized that I also needed to prove that there is no bigger number that divides n other than n itself. I thought this should be obvious but actually I could not find a proof of it online. This is my attempt to prove that the gcd of a number is itself (please tell me if there is a shorter proof):

Suppose there is a natural number d that divides the natural number n with d > n. Then we have natural numbers k and s such that:

sd = n since d divides n
d = n + k since d is greater than n
s(n+k) = n
sn + sk = n
sn - n + sk = 0
s(n-1) + sk = 0
There are 2 possible cases:
1. n-1 = 0. Then s(n-1) = 0. As s >= 1 and k >= 1, sk >= 1 (I realize that I will have to prove this too at some point...). But we have sk = 0 >= 1, a contradiction. 
2. n-1 >= 1. Then s(n-1) >= 1. Then s(n-1) + sk >= 2. But we already have s(n-1) + sk = 0, a contradiction. 

My question is:

Is it really necessary to prove such facts and if not, how can I avoid getting bogged down in such details?

Answer 1

Of course it's necessary to prove these facts! In mathematics we cannot appeal solely to intuition.

In any case, your proof is more complicated that it needs to be: it's true that, by your hypothesis, $sd = n$. But since $s>1$, you can conclude $sd > d > n$; so you have simultaneously $sd = n$ and $sd > n$, contradiction. Therefore there cannot be a $d>n$ that divides $n$.

Answer 2

Just to offer a slightly different point of view I will quote from Doron Zielberger's Opinion #43:

The reason mathematics has advanced so much was not because of the Euclidean axioms-lemma-theorem straitjacket, but in spite of it. Luckily, when we actually discover mathematics, we do it the Babylonian way, empirically and algorithmically. It is only when it is time to present it, that we put on the stifling Greek formal attire.

Available here: http://www.math.rutgers.edu/~zeilberg/Opinion43.html

If you are worried your version of Euclid's algorithm won't work without a proof of correctness, that's silly. If you are presenting a proof to an instructor demonstrating your ability prepare proper proofs then details count (a lot).