The example you have is great! I imagine it would be really hard to actually have all parts with similar difficulty. E.g. in your example, L2 is an immediate observation, while L1 and L3 (particularly the latter) require some manipulations with $n!$. It's still great, but I would expect (I might be wrong, of course) the group solving L2 to finish much faster than other groups.
Here are two examples that I think have a similar spirit, although the division of work between different parts is far from equal.
Irrationality of $\pi$
A proof of $\pi \notin \mathbb{Q}$ found in Bourbaki's book (it might be due to someone else, see one of the comments) is naturally divided into parts, somewhat similarly to your proof of $e \notin \mathbb{Q}$. Take $f_n(x) = \frac{1}{n!} b^n x^n (\pi-x)^n$. Then:
- L1: $\int_0^\pi f_n(x) \sin(x) dx > 0$
- L2: $\int_0^\pi f_n(x) \sin(x) dx \to 0$ as $n \to \infty$
- L3: If $\pi$ is a fraction $a/b$, then derivatives of any order of $f_n$ at $0$ and $\pi$ have integer values. Possible hint: write $b^n x^n (\pi-x)^n$ as $x^n (a-bx)^n$, and use the symmetry between $x=0$ and $x=\pi$.
- L4: If $f$ is any polynomial of degree $2n$, then $\int_0^\pi f(x) \sin(x) dx$ is a sum of terms $\pm \left[ f^{(k)}(x) \sin x \right]_0^\pi$ and $\pm \left[ f^{(k)}(x) \cos x \right]_0^\pi$ for $k=0,1,\ldots,2n$.
Here L3 and L4 together imply $\int_0^\pi f_n(x) \sin(x) dx \in \mathbb{Z}$, which contradicts L1 and L2.
Liouville's theorem and a construction of a transcendental number
Lioville's theorem states that irrational algebraic numbers don't have efficient rational approximations. More precisely: if $a \in \mathbb{R}$ is an algebraic number of degree $d>1$, then $|a-\frac{p}{q}| \ge \frac{c}{q^d}$. The proof consists of basically three steps, and in the fourth step one can use the theorem to show that a certain number is not algebraic.
- L1: Assume that $a$ is a root of the polynomial $f(x) = a_0+a_1 x+\ldots+a_d x^d$ with integer coefficients. Assume that $d$ here is the smallest possible. Then $f$ doesn't have rational roots.
- L2: Assume that $f(x) = a_0+a_1 x+\ldots+a_d x^d$ has integer coefficients and $f(p/q) \neq 0$ (where $p,q \in \mathbb{Z}$). Then $|f(p/q)| \ge q^{-d}$.
- L3: Let $f$ be any polynomial. Justify that there's a constant $C > 0$ (depending on $a$ and $f$) such that $|f(x)-f(a)| \le C |x-a|$ for $x \in [a-1,a+1]$. Remark: one doesn't even need derivatives to check that.
- L4: Let $L := \sum_{n=1}^\infty 10^{-n!}$ (Liouville's number). Then for any $d \in \mathbb{N}$ and $c > 0$ there is a rational approximation $p/q$ such that $q^d |a-\frac{p}{q}| < c$.
Here L1, L2, L3 together imply Liouville's theorem mentioned before. If $L$ were algebraic (i.e., a root of a polynomial with integer coefficients), it would contradict this law.
