This isn't quite right -- Abel proved that there's no quintic formula before Galois came along. Galois theory gives a whole lot more insight, lets you understand why some quintics do have solutions in radicals, etc., but Galois doesn't (or at least shouldn't) get credited for proving that there isn't a quintic formula, because he wasn't the first to do that.
Don't let the truth get in the way of a good story! hahahaha
But yeah you're right
edit: i don't recall Abel's proof, but Galois reformulation of what it means to be solvable by radicals, introducing the permutation group of the roots is the big thing in my mind.
In lay terms the best I can say is that for n greater than or equal to 5, the set of all possible permutations of n things is complicated. For n less than 5 the set of all possible permutations of n things is simple just because n is small. That's what leads to there being general formulas for n = 2, 3, 4.
Galois translated whether a polynomial has a solution for x in terms of the coefficients using algebraic operations up to using radicals into a property of the group of permutations of the roots of the polynomial. The property of the group is whether the group is solvable. For n greater than or equal to 5, the general permutation group on n objects is not solvable but for n less than 5 is is. There just are not that many permutation groups for n = 2, 3, and 4 objects and all these permutation groups are solvable. Generically a group is not solvable and so we see this with larger n.
