Can infinity shorten proofs a lot? I've just been asked for a good example of a situation in maths where using infinity can greatly shorten an argument. The person who wants the example wants it as part of a presentation to the general public. The best I could think of was Goodstein sequences: if you take a particular instance of Goodstein's theorem, then the shortest proof in Peano arithmetic will be absurdly long unless the instance is very very small, but using ordinals one has a lovely short proof. 
My question is this: does anyone have a more down-to-earth example? It doesn't have to be one where you can rigorously prove that using infinity hugely shortens the shortest proof. Just something where using infinity is very convenient even though the problem itself is finite. (This is related to the question asked earlier about whether finite mathematics needs the axiom of infinity, but it is not quite the same.)
A quick meta-question to add: when I finally got round to registering for this site, I lost the hard-earned reputation I had gained as a non-registered user. I am now disgraced, so to speak. Is that just my tough luck?
 A: Is there anything wrong with the simplest case - mathematical induction? If I want to show that the sum of the first million cubes is whatever it is, much easier to prove the general formula then specialise to n = 1000000.
Now I see from above Qiaochu Yuan has discounted induction as an answer. But why? Induction relies on the natural numbers being a certain initial algebra, i.e., being taken as an entity, which happens to have infinite cardinality.
A: A good example is a solution to Hilbert's third problem: it is not possible to cut the unit cube into finitely many polyhedral pieces and reassemble then as the regular tetrahedron of unit volume. The shortest proof requires construction of a Dehn's invariant which, in turn, requires the existence of a Hamel basis of the set of real numbers regarded as a linear space over $\mathbb Q$. The existence of such Hamel basis follows from the axiom of choice.
There are variants of the proof that reqire working with finitely dimensional linear spaces only, but the argument mentioned above is more elegant and leads to more general results. 
A: An example that I came to think of even though it doesn't have to involve infinity is the existence of a finite field with a specified number $q=p^n$ of elements. One can show by an enumerative argument (Möbius inversion) that there must be an irreducible polynomial of degree $n$ over $\mathbb{Z}_p$ (there simple aren't enough lower degree polynomials to factor all of them). If $f$ is such a polynomial, then $\mathbb{Z}_p[x]/f(x)$ provides a field of $q$ elements. 
An alternative is to use the fact that every field has an algebraic closure, and to verify that the set of zeros of $x^q-x$ in the algebraic closure of $\mathbb{Z}_p$ is closed under the field operations (and that they are distinct).
It's true that we really only need the splitting field of $x^q-x$ which, as it turns out, consists of only those $q$ zeros, but that's something that emerges from the proof, and it might conceivably have been much bigger.
A: I once had a teaching assistant in calculus who admitted that he was unable to give an epsilon, delta proof that a the Heaviside stepfunction was not continuous.  To take a slightly less trivial example, the proof that $y=x^2$ is not uniformly continuous using $\epsilon, \delta$ is somewhat involved for a freshman.  Using an infinite number $H$, this becomes transparent.  Consider the infinitesimal $e=1/H$.  Then the points $x=H$ and $x=H+e$ are infinitely close, but the corresponding values of $y$ are not by a trivial calculation.  This implies a failure of uniform continuity by general theory.
A: A simple instance where infinity makes things simple is when proving that there exist transcendental numbers. Instead of having to come up with ways to tell a transcendental number from an algebraic one, you simply say «well, there are too many numbers for all of them to be algebraic, so there you have it».
A: One of my colleagues (Silver) gave a general purpose talk last week. You can't untie a knot $A$ by tying another knot $B$ into the rope. 
Proof. First show that the connect-sum of long knots is abelian by sliding $A$ through $B$. Then form the decreasing-in-size connect-sum $(AB)(AB)(AB) \dots$. Regroup: $A(BA)(BA) \dots$. If $AB = 0$, i.e. the unknot, then the left-hand grouping is the unknot. The right-hand-grouping is $A$ since $BA=AB=0$. Since $A$ is a knot, then $A=0$, a contradiction. QED
The nice thing about the argument is that it uses an infinitely long piece of rope, an infinite sequence of knots, and the knots shrink to being infinitesimally small.
A: The precise asymptotics of the partition function $p(n)$ are, as far as I know, totally inaccessible by finitary tools.  More generally the methods of complex analysis are a great way to obtain incredibly precise asymptotics on many finitary sequences of concrete interest, i.e. trees satisfying certain properties or sequences related to the running times of algorithms, etc.  
A related example is comparing the elementary and non-elementary proofs of the prime number theorem; my recollection is that the elementary proof is quite a bit more involved.
A: This isn't particularly down-to-earth, but of course before February or March you had the situation where the density Hales-Jewett theorem (which can be phrased in completely finitary language) was only provable via ergodic-theory methods (which are infinitary.)
A: This is probably neither the sort of infinity nor the sort of simplification you're looking for, but Bézout's theorem is a challenge to prove, let alone state, without a line at infinity.  I don't know if it would be suitable for a general audience either, but in its favor, it has a very nice statement using both the infinite and the infinitesimal (i.e., contact multiplicity).
A: Perhaps fitting in here is Lindenstrauss's proof of Lyapunov's convexity theorem.
http://atlas-conferences.com/c/a/e/y/06.htm 
"the slickest proof to end all proofs" (Halmos)
although the result is in $\mathbb{R}^n$, for the proof we go to an infinite-dimensional space
A: Using Eilenberg-Maclane spaces (namely $K(\mathbb{Z},2)=\mathbb{P}^{\infty}(\mathbb{C})$) and cellular approximation,one can show that any 3-fold with a positive Betti number has a map to the sphere $S^2$ which is not nullhomotopic. I am not sure how "down to earth" this example is, but it shows that even when studying finite dimensional objects it is natural to consider infinite-dimensional things. 
A: Short version of "there exist functions not computable by Turing machine" using infinities:
There are an uncountable number of predicates, but only a countable number of Turing machines, so there are some predicates that are not computable by a Turing machine.
(That's weaker than the usual proof of the uncomputability of the Halting Problem of course, because it doesn't tell you that "does this Turing machine halt?" is one of those predicates.)
A: I am surprised no one has mentioned any examples from physics. Fluid mechanics for example obtains some beautiful results by assuming that a fluid is continuous, while at the molecular level it is a discrete object. An example from my physics highschool textbook:

Suppose you have a circular grain storage, with a diameter of 2 meters and 10 meters high. The grain weights about $X \ kg/m^3$. What is the pressure at two meters depth? at four meters depth?

The problem is easier to solve if we think of the grain as a fluid and apply, say, Pascal's principle.
A: I can't think of any good specific examples off the top of my head, but I'm sure that there must be lots of examples where you can much more easily prove something about an affine variety by adding "points at infinity", i.e. by looking at the projectivization of the variety.
A: One way of generating very simple examples of this kind  is to define a family of predicates $F(n)$ by recursion over the natural numbers. Then, there can usually be no proof of $\forall n. F(n)$ in Peano arithmetic, since $F(n)$ won't usually be a schema in the sense the first-order Peano induction axiom requires -- it can be a different formula at each numeral. 
For example, one very simple example is to define 
$F(0)   = (0 = 0)$
$F(n+1) = (n+1 = n+1) \wedge F(n)$
Now, it's clearly the case that $\forall n. F(n)$. However, since it's a different tautology for each argument, Peano arithmetic can't prove this proposition correct (indeed, it's not even a formula of first-order logic). We can only prove each instance correct, which becomes an infinite number of (incredibly trivial) propositions to prove....
A: While browsing Wikipedia, I came across this statement:
"The introduction of projective techniques made many theorems in algebraic geometry simpler and sharper: For example, Bézout's theorem on the number of intersection points between two varieties can be stated in its sharpest form only in projective space".
I think this fact can be stated in simple terms without any explicit reference to algebraic geometry and projective space, just talking about intersections of graphics of polynomials, the product of their degrees, and "combing space to get the point of infinity" (or some better and longer explanation).
A: Maybe you want something more proof-theoretic, like Gödel's speed-up theorem.  The example from the Wikipedia article says: the statement "This statement cannot be proved in Peano arithmetic in fewer than a googolplex symbols" is provable in Peano arithmetic, but the shortest proof has at least a googolplex symbols (explanation given there).  On the other hand, the theory PA+CON(PA) gives a short proof.  
Similarly, second-order arithmetic (since it proves CON(PA)) gives a short proof, and I guess that would count as "adding infinity".  Or you could look at hereditarily finite set theory (ZFC with the axiom of infinity replaced by its negation).  I'm pretty sure regular ZFC proves this theory consistent, so again the speed-up theorem works out about the same way as it does with PA.
A: A down-to-earth example: the Stirling approximation to the factorial.
At least the derivation given on the Wikipedia page compares the explicit sum representation of $\ln(n!)$ with a Riemann sum approximation of the integral $\int \ln(x) \mathrm{d}x$. One only needs finite integers to talk about factorials. On the other hand, one needs at least a couple of kinds of infinities for the real analysis involved in describing the integral and accompanying error estimates. However, the simplicity of this derivation of the Stirling formula is undeniable.
A: Hindman's theorem is an example where (slightly?) higher infinity simplifies a proof greatly.  The theorem asserts that, if you partition the set of positive integers into finitely many subsets, then there is an infinite set $H$ of positive integers such that all sums of finitely many members of $H$ lie in the same piece of your partition.  (If, like me, you consider 0 to be such a finite sum, of 0 terms, then explicitly exclude it from the conclusion, so that the statement makes sense.)  Hindman's original proof worked in the natural domain of the result, second-order arithmetic, but Hindman himself has suggested that this proof is such as would be useful for torturing students.  There is a non-torturous proof, due to Galvin and Glazer, but an essential part of that proof involves considering a semigroup whose points are ultrafilters on the natural numbers - so we're well beyond second-order arithmetic.  In fact, a key lemma in the proof depends on applying Zorn's Lemma to a certain poset of subsemigroups of this semigroup.  So we're even farther "up" from the natural domain of the theorem.  (By the way, the reason for "slightly?" in the first line of this answer is that, although we're well above where most mathematicians like to work, we're nowhere near what set theorists would call "large cardinals".)
A: Consider the following question of Erdos and Hajnal:
Question (Erdos-Hajnal) Is there a finite $K_4$-free graph which, when the edges colored by $2$ colors, always contains a monocolored triangle.
The question is answered by Shelah, and his argument uses infinity. I think this is the only known proof.
Shelah's proof of the theorem is simply as follows: 

He constructs a forcing extension which adds a graph $X$ with the same property but 
  with $\aleph_0$ colors. Then $X$ has the edge-coloring property for $2$ colors, 
  as well. Then using compactness theorem, $X$ must contain a finite subgraph $Y$ with the same property.
   As forcing cannot create new finite graphs, $Y$ is already present 
  in the ground model.  By Godel, $ZFC$ proves that there is such a graph. 

A: Maybe "analytic number theory" belongs here as an answer.  Certain number theory results are most simply proved using complex analysis.
A: The Mazur Swindle?  See the Wikipedia page, for example. 
A: The axiom system PRA of "primitive-recursive arithmetic" is finitistic, but it has been known for a few decades that it has the same set of $\Pi^0_1$ consequences as the infinitistic theory $\text{WKL}_0$ of second-order arithmetic. In particular, there is a primitive recursive function $f$ that turns a formal proof of a $\Pi^0_1$ statement in $\text{WKL}_0$ into a proof in PRA. Roughly put, a $\Pi^0_1$ formula says that all natural numbers have some particular property, depending on the formula, where the property can be stated using a formula in the language of rings with no quantifiers. 
The advantage of working in $\text{WKL}_0$ is that the proofs can be much shorter. I think this was always suspected, but Caldon and Ignjatovic recently established (pdf) a formal superexponential lower bound for $f$, at least on an infinite set of formulas.  Their result is phrased for a different infinitary system, $I\Sigma^0_1$, that lies between PRA and $\text{WKL}_0$. $I\Sigma^0_1$ is a fragment of Peano arithmetic, unlike $\text{WKL}_0$; its main difference from PRA is that $I\Sigma^0_1$ allows direct universal quantification over the set of natural numbers during the proof, while PRA does not. 
In their paper, the set of formulas for the lower bound is explicitly laid out.  These may not be particularly concrete, because they relate to consistency statements.
If we expand PRA to allow for existential quantification, we can get a slightly larger theory in which $\Pi^0_2$ statements can be expressed. It is known that $\text{WKL}_0$ is still conservative over this larger theory for $\Pi^0_2$ statements. In 1994, Kikuchi and Tanaka (pdf) gave a nice example of how this could be used to show that the second incompleteness theorem is provable in PRA, by using model-theoretic, infinitary methods in $\text{WKL}_0$ and relying on the conservation result. 
A: I'm not sure whether this is more "down-to-earth" but take 0-1 laws of random graphs. The probability of a first order property to be satisfied by a random graph distributed $G(n,p)$ tends to 0 or 1.
The proof is by showing that the limit theory satisfied by these graphs has only one countable model, and is therefore complete.
A: Nachum Dershowitz has lots of work on termination proofs and many of these make use of ordinal arithmetic. In particular, if you have a computer program that moves from one state to another, and you can label each state with an ordinal, and you know that the ordinal for each new state is strictly less than the ordinal for the previous state, then the program must eventually terminate. Goodstein's Theorem is a special case, showing termination for a highly contrived sequence. But more realistic examples arise when studying termination of rewrite rules.
A basic example is proving termination of the rewrite rules that define symbolic differentiation. Like in the case of Goodstein's theorem you have the same problem that differentiation might take a step forward in decreasing the powers in a monomial, but then takes what looks like a giant step back as applying the Leibniz rule to a product can lead to many more terms. But Floyd came up with a neat labelling by ordinals resulting in a really simple termination proof. See example 8 here for example.
Also see the conclusion in this paper.
Apparently the idea for this originated with Alan Turing.
A: If you want a situation where there is only an infinite proof then there is the strengthened finite Ramsey theorem which is not provable in PA but can be deduced from the infinite Ramsey theorem. see:
http://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theorem
A: The Poincare conjecture might qualify as an example.  One can phrase this conjecture in a purely combinatorial fashion, involving finite simplicial complexes, but the only known proof of this conjecture uses Ricci flow, and in particular the various monotonicity properties of this flow which are proven by integration by parts, as well as the repeated use of limits.  In principle, this proof can be finitised by working with finite element versions of Ricci flow, but it would definitely lengthen the proof substantially.  (On the other hand, Perelman's proof is not exactly short to begin with, so this may not be the best example...) 
A: There is a theorem that if a set of edge colored square tiles can be used to tile the positive orthant then it can also be used to tile the entire plane. (The edges are colored and in the edge-to edge tiling you need to match the colors). 
The easy argument (using infinity) is: draw a rooted tree where the level $k$ vertices  are all possible tilings of a $(2k-3) \times (2k-3)$ squares (and there is a root at level 1). This is a tree with each vertex has a finite number of children. The fact about the positive quadrant asserts that there are vertices of arbitrary large level, and Konig's theorem then asserts that there is an infinite path which then gives the tiling of the plane. (Proving Konig's theorem is based on moving from a vertex with infinitely many descendants to one of his children with infinitely many descendants.)
I am not sure that this qualifies as an answer since I am not aware of any "finite" proof and there is something infinite in the statement itself. But there may be special cases where a tiling of the positive orthant be explicitly presented, and it will allow a finite proof which can be very complicated.
A: Every finite partial order has a maximal element. 
One can prove that by induction and looking at cases, but I think the most natural way is to argue that if there is no maximal element, one must have a strictly increasing infinite sequence, which is impossible.
A: Maybe you could use some complex transformation related to Möebius functions (of the kind "circles and lines are the same") to prove several 2D-geometric statements at once.
A: What about the puzzle named escape on Joel David Hamkins' homepage?
http://jdh.hamkins.org/escape/
That not all the squares occupied by the three stones in the initial configuration can be vacuated is shown with infinite series.
