How do I formally prove a universal implication? A textbook I am reading (Discrete Mathematics and its Applications by Rosen) went from introducing formal propositional and predicate logic (including popular rules of inference like Modus Ponens, Modus Tollens, and Universal Generalization) to introducing direct methods of proof for theorems of the form ∀n(P(n)->Q(n)).
Apparently, most mathematical proofs of any kind of theorem are "informal" and omit many logical rules of inference and argumentative steps for the sake of conciseness. However, because the textbook doesn't provide even one example of a detailed "tedious" proof that expresses most or all rules of inference and axioms used in the proof, though I have a general idea of the connection between the two, I have been struggling to fully tie together the ideas of formal logic to the ideas of mathematically proving theorems of the form ∀n(P(n)->Q(n)). Can anyone provide an example of a detailed mathematical proof of a simple theorem that omits few (if any) logical steps in the argument? I have personally struggled with (as a personal exercise) meticulously proving the theorem "for all integers, if n is odd then the square of n is odd", but any logically detailed argument proving a simple theorem similar to that would be very useful.
 A: More a reflection than an answer, but too long for a comment.
Your observation that

Apparently, most mathematical proofs of any kind of theorem are
  "informal" and omit many logical rules of inference and argumentative
  steps for the sake of conciseness.

is true. I think it should follow that starting an undergraduate text on discrete mathematics with formal logic - truth tables, rules of inference, quantification - only confuses students when they are then expected to construct convincing proofs using everyday clear thinking. They rightly wonder whether all that formality is necessary and ask questions like this one.
Of course it is necessary in other contexts - when studying logic, when designing programs to prove theorems - but not in introductory courses.
Edit, suggested by @Bram28 's excellent answer. Rosen's Universal Generalization that replaces "for all elements $x$ such that" by "let $x$ be an arbitrary element such that" is close to what is often called "proof by representative special case". Those are not proofs but tell you clearly how a formal (or informal) proof will work. 
For (a toy) example, to prove that the square of an odd number is odd, look at what happens when you square $15$. The distributive law tells you
$$
15^2 = (2\times 7 + 1)^2 = 4 \times 49 + 2 \times (2\times 7) + 1
$$
which is the sum of two even numbers and $1$, hence odd. There was nothing special about $15$ in this argument - you can clearly see  how it represents all odd numbers.
(Parenthetically, this example/proof suggests the even stronger theorem that the square of an odd number is congruent to $1$ modulo $4$.)
If you search for "representative special case" (with the quotation marks so that you get just links to the whole phrase) you find this from Hilbert:

The art of doing mathematics consists in finding that special case
  which contains all the germs of generality. 
  (Example for Hilbert quote),

a quote from Polya , and other links worth following.
A: Yes, I noticed that about the Rosen book as well: he never provides a detailed example for Universal Generalization ... which is very frustrating, as that rule is actually a bit tricky because of the constraint put on the constant being used. That is, Rosen defines the rule as:

$P(c)$ for an arbitrary $c$
$\therefore \forall x \ P(x)$

But doesn't really specify how the $x$ being 'arbitrary' is handled formally. His informal discussion says:

Universal generalization is used when we show that ∀xP(x) is true by taking an arbitrary element c from the domain and showing that P(c) is true. The element c that we select must be an arbitrary, and not a specific, element of the domain. That is, when we assert from ∀xP(x) the existence of an element c in the domain, we have no control over c and cannot make any other assumptions about c other than it comes from the domain.

Well, unless you know what you're doing, that's still not very clear, I agree.
Indeed, it is for this reason I always recommend against using the Rosen book to learn formal proofs ... it's a nice textbook on discrete mathematics, but on this particular section it is actually very poor (actually, another complaint I have about the book is that its treatment on Turing-machines is far too sparse: it does not give the reader any sense of how important Turing-machines are in the foundations of computer science).
Also, before going on, I think that Ethan Bolker makes an excellent point about formal proofs: most computer scientists (and even most mathematicians) don't really need to know how exactly formal proofs work ... you just need to know how to do proofs at somewhat more informal level ... and Rosen's book is much better on that score. That said, formal proofs do teach you to be precise and organized about your proofs, so I am not totally against doing formal proofs either, even if they are overkill for most situations.
Indeed, you asked about formal proofs, and how to use in particular the Universal Generalization rule, so let me try and address that in the rest of my Answer.
Again, Rosen never really gives a precise formalization of the rule. But, fortunately, other textbooks (dedicated to just formal logic) have ways of formalizing this. Let me give some examples.
Suppose you have premises:
$\forall x (P(x) \to Q(x))$
$\forall x (Q(x) \to R(x))$
From this, we should be able to infer:
$\forall x (P(x) \to R(x))$
Here is a formal proof you could do:
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Premise\\
2&\forall x (Q(x) \to R(x))&Premise\\
3&P(c) \to Q(c)&Universal \ Instantiation \ on \ 1\\
4&Q(c) \to R(c)&Universal \ Instantiation \ on \ 2\\
5&P(c) \to R(c)&Hypothetical \ Syllogism \ on \ 3,4\\
6&\forall x (P(x) \to R(x))&Universal \ Generalization \ on \ 5\\
\end{array}
Now, why is this a correct use of the rule Universal Generalization (and thus a proper proof?).  It is because when the $c$ was used for the first time, it came from a Universal Instantiation .. meaning that indeed we weren't making any additional assumptions about $c$ other than it being some arbitrary object from the domain. That is, on line 3 we effectively said: "Let $c$ be an arbitrary object from the domain. Well, then because of line 1 we have $\forall x (P(x) \to Q(x))$, this should be true for all objects, and thus also for $c$, and hence we have $P(c) \to Q(c)$.  More importantly, on line 6, we say: "We have found (on line 5) that $P(c) \to R(c)$.  OK, but since $c$ was an arbitrary object from the domain, then line 5 effectively states that $P(c) \to R(c)$ is true for any $c$, and hence we can conclude that it is true for all objects from the domain, i.e. we have $\forall x (P(x) \to R(x))$
Some formalizations actually make the step of saying "Let $c$ be an arbitrary object from the domain." very explicit by giving it its own line. In those formalizations, the proof would look something like this:
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Premise\\
2&\forall x (Q(x) \to R(x))&Premise\\
3&c&Introduce \ c\\
4&P(c) \to Q(c)&Universal \ Instantiation \ on \ 1\\
5&Q(c) \to R(c)&Universal \ Instantiation \ on \ 2\\
6&P(c) \to R(c)&Hypothetical \ Syllogism \ on \ 3,4\\
7&\forall x (P(x) \to R(x))&Universal \ Generalization \ on \ 3-6\\
\end{array}
The single $c$ on line 3 is of course not a claim, but again it is a way of saying $\exists x \ P(x)$ "Let $c$ be an arbitrary object from the domain." So then, on line 7, the proof notes that the $c$ used in line 6, was introduced on line 3, meaning that $c$ is arbitrary, and hence line 6 can be universally generalized.
To do formal proofs, I myself like to use a piece of software called Fitch, in which they use 'subproofs' to indicate assumptions. You can use those very subproofs to formalize the introduction of new constants as well:

Notice how the rules are called a little differently here: Generalization is 'Introduction', while Instantiation is 'Elimination'. Indeed, in a Fitch system, you have Introduction and Elimination rules for all logical operators ... and no other rules.  In fact, the Hypothetical Syllogism (HS) in this proof is used as a Lemma: it refers to an earlier proof I already did that derives Hypothetical Syllogism from more basic Introduction and Elimination rules. If we expand this Lemma in the proof, we get:

Here, $\to$ Elim is of the same as Modus Ponens, and $\to$ Intro formalizes the important proof technique of Conditional Proof.
Now, notice that many universal claims have a conditional as the main connectives of their body. Indeed, you yourself explicitly asked about how to prove statements of the form $\forall x (P(x) \to Q(x))$. This example is no exception. Thus, you get a Conditional Proof inside a Universal Proof. This pattern is so common that these two often get combined into what is called a Universal Conditional Proof. For example, to prove that "All $P$'s are $R$'s", you typically start your proof with "Let's consider any $P$ ..." and try to show that this $P$ is an $R$. What's cool, is that Fitch can be used to formalize this proof technique as well:

See how that works?  OK, now let's look at a different example. Suppose we have:
$\forall x (P(x) \to Q(x))$
$\exists x \ P(x)$
From this, we should be able to prove $\exists x \ Q(x)$, but not $\forall x \ Q(x)$
OK, let's see how this fleshes out formally. First, a valid proof using Existential Generalization (this is actually very similar to example 13 from Rosen):
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Premise\\
2&\exists x \ P(x)&Premise\\
3&P(c) &Existential \ Instantiation \ on \ 2\\
4&P(c) \to Q(c)&Universal \ Instantiation \ on \ 1\\
5&Q(c)&Modus \ Ponens \ on \ 3,4\\
6&\exists x \ Q(x) &Existential \ Generalization \ on \ 5\\
\end{array}
OK, so first note that Existential Generalization does not come with any constraints on the constant that is being used. Rosen says that you merely need $P(c)$ for some constant $c$ in order to conclude $\exists x \ P(x)$ ... so it doesn't matter where this $c$ comes from. And that makes sense: if you know that $P(c)$, then you can conclude $\exists x \ P(x)$, no matter how this $c$ is being used or how it was introduced.
OK, but what goes wrong if we do:
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Premise\\
2&\exists x \ P(x)&Premise\\
3&P(c) &Existential \ Instantiation \ on \ 2\\
4&P(c) \to Q(c)&Universal \ Instantiation \ on \ 1\\
5&Q(c)&Modus \ Ponens \ on \ 3,4\\
6&\forall x \ Q(x) &Universal \ Generalization \ on \ 5\\
\end{array}
OK, what goes wrong here is that the $c$ wasn't an arbitrary object, i.e. it wasn't just any object. Rather, it was one-of-those-objects that, given line $2$, we know to exist and that have property $P$. So, we can't universally generalize.
Using the method of having to explicitly introduce an arbitrary object, we would see how the proof fails as well:
\begin{array}{lll}
1&\forall x (P(x) \to Q(x))&Premise\\
2&\exists x \ P(x)&Premise\\
3&c&Introduce \ c\\
4&P(c) &Existential \ Instantiation \ on \ 2\\
5&P(c) \to Q(c)&Universal \ Instantiation \ on \ 1\\
6&Q(c)&Modus \ Ponens \ on \ 3,4\\
7&\forall x \ Q(x) &Universal \ Generalization \ on \ 3-6\\
\end{array}
Now, the problem is on line 4:  $c$ was already introduced (on line 3) as a completely arbitrary object. But that means that we cannot be for certain that $c$ has property $P$. Yes, sure, line 2 tells us that some objects have property $P$, but that does not mean that given any arbitrary object $c$, I can say for certain that it has property $P$. So, again, line 4 fails.
Indeed, like Universal Generalization, the Existential Elimination rule comes with an important constraint:  The constant that you use to instantiate for the variable that is existentially quantified should not just be any constant, but a new constant, i.e. a constant that has not been used earlier in the proof. To see this, consider:
\begin{array}{lll}
1&P(c)&Premise\\
2&\exists x \ Q(x)&Premise\\
3&Q(c) &Existential \ Instantiation \ on \ 2\\
4&P(c) \land Q(c)&Conjunction \ on \ 1,3\\
5&\exists x (P(x) \land Q(x))&Existential \ Generalization \ on \ 4\\
\end{array}
Here, line 3 is where things go wrong. Sure, from line 2 we know that there are some objects that have property $Q$, but of course this does not mean that specifically object $c$ (that line 1 already makes reference to, and thus has a certain use/role for) has property $Q$.
Unfortunately, in his semi-formal way of describing the rule, Rosen fails to point out this important restriction, and instead merely says:

$\exists x \ P(x)$
$\therefore P(c)$ for some element $c$

No! It needs to be for some new element $c$!
In his informal description of the rule, Rosen writes:

Existential instantiation is the rule that allows us to conclude that there is an element c in the domain for which P(c) is true if we know that ∃xP(x) is true.We cannot select an arbitrary value of c here, but rather it must be a c for which P(c) is true. Usually we have no knowledge of what c is, only that it exists. Because it exists, we may give it a name (c) and continue our argument.

... I suppose here he gets it right ... but it is not very clear: did you understand that $c$ had to be a new constant from this?
Once again, I like how Fitch does things.  Here is the formalization of the valid proof in Fitch:

When the system verifies this proof, and gets to line 7, it checks to make sure that the $c$ that was used to eliminate the existential (and hence was introduced at the start of the subproof) is indeed a new constant, rather than a constant already used. So, in this case, it checks out. But, in the following 'proof' it does not:

OK, finally, let's do an actual proof: let's prove that an odd number squares will be an odd number itself.  Of course, we'll need to decide on what axioms to use, i.e. what we can use as premises. Here, we could decide to use the Peano Axioms, but starting with those from scratch, the proof would become really long. So, instead, here is a proof in Fitch that does use a few of those axioms, but also assumes some basic properties of commutation, association, and distribution regarding addition and multiplication:

See how tedious this becomes?  ... this is why practicing computer scientists and mathematicians rarely do formal proofs.
A: 
Can anyone provide an example of a detailed mathematical proof of a simple theorem that omits few (if any) logical steps in the argument? 

Yes. See my formal proof (updated) resolving the famous Barber Paradox. There, I prove that: 

A resident of a village can shave those and only those men living
  there who do not shave themselves if and only if that resident is
  not a man.

The proof is an ordered list of 100 lines of proof, each line being generated by invoking a single axiom of set theory or rule of logic, e.g. line 1 is generated using the Premise Rule. The Conclusion Rule (e.g. line 13) is invoked to make universal generalizations by either direct or indirect proof. Commentary is in a blue font.
A: Actually writing out a fully formal proof is not generally done. I once saw a proof of 1+1 = 2 from basic axioms that took several dozen lines. If you want to prove "n is odd -> n^2 is odd", you'd take a definition of "odd", such as $\exists k: n = 2k+1$, then use that to show $n^2$ fits the definition. You'd have to use several applications of the distributive rule and the commutative  nature of multiplication over the integers to get from $(2k+1)(2k+1)$ to $4k^2+4k+1$. Then you could write that as $2(2k^2+2k)+1$. Then you could observer that taking $k_2 = (2k^2+2k)$, we have $n^2=2k_2+1$, which satisfies the definition of being odd. To be rigorous, you'd have to show that $(2k^2+2k)$ is an integer (that can be done by invoking the closure of integers over multiplication and addition).
