Proof: by Ivan Niven (1915-1999),
Bull.Amer.Math.Soc. 53 (1947),509):
Assume  = a/b with positive integers a and b. We will deduce a contradiction. For an integer n>0 define
It satisfies f(x) = f(-x) and the inequality
|
0 < f(x) <n an/n!
|
for all x in [0,]. For all j, smaller or equal to n, the j-th derivative of f
is zero for x=0 and x=. For j larger or equal to n, the j-th derivative of f
is an integer at 0 and . The function
|
F(x) = f(x) - f(2)(x) + f(4)(x) - ... + (-1)n f2n(x)
|
now has the property that F(0) and F() are integers and F + F'' = f. Therefore,
|
(F'(x) sin(x) - F(x) cos(x))' = f sin(x)
|
By the fundamental theorem of calculus,  f(x) sin(x) dx is an integer.
By the inequality however, this integral is strictly between 0 and 1 for large n. QED.
|
|
is irrational.