Trying to prove that $x\sin(\frac{\pi}{x})\ge\pi \cos(\frac{\pi}{x})$ for $x\ge 1$

The proof of the original statement that $f(x)\equiv x\sin\frac{\pi}{x}$ is a monotonically increasing function of $x$ for $x>1$ can be done as follows:

First, we show that the second derivative $f''(x)$ of the function is negative:

Simplify[D[x Sin[π/x], x, x] < 0, Assumptions -> x > 1]

True

This means that the first derivative $f'(x)$ is a monotonically decreasing function of $x$ for $x>1$.

Now we show that the derivative of the function approaches zero as $x\to\infty$:

Limit[D[x Sin[π/x], x], x -> ∞]

0

Since the derivative has been shown to be decreasing and to have a limit of zero for $x\to\infty$, it follows that $f'(x) > 0$ for $x>1$. This proves the desired statement about $f(x)$.

Edit

To take the other route proposed in the edited version of the question, you could do the following:

Resolve[ForAll[{x}, x > 1 && Tan[π/x] >= π/x, f'[x] >= 0], Reals]

True

Edit 2

In the Resolve statement above, ForAll has three arguments: the variable {x}, a condition, and the statement to be proved. In words, this says the following: for all $x$ that satisfy the condition $x>1$ and $\tan(\pi/x)\ge \pi/x$, it holds that $f'(x)\ge0$. Of course, the condition can actually be simplified because the tangent inequality as stated here only holds for $x>2$.

To make the condition fully consistent with the desired interval $x>1$, we simply have to replace $x$ by $2 x$ in the tangent inequality. This leaves the inequality unaffected but extends its range of validity to $x>1$. Therefore, we get the following statement that can be fed to Mathematica:

Resolve[ForAll[x, x > 1 && Tan[π/(2 x)] >= π/x/2, f'[x] >= 0], Reals]

True

Mathematica often responds well when provided a little expert assistance. Let's focus on techniques that have a wide application rather than just to this problem.

1. Can the function be decomposed into simpler pieces? Yes, obviously: $f(x)$ is the product of $x$ and $\sin{\pi / x}$. Both are obviously increasing for $x \in [1,2]$. After that, $\sin{\pi / x}$ turns around: it decreases while $x$ continues to increase. The challenge is to show that the increase in $x$ overpowers the decrease in the rest of the function. However, perhaps we have accomplished something: we can focus on the cases $x \ge 2$.

2. It can be more difficult, both theoretically and computationally, to determine characteristics of a function on an infinite (or noncompact) set like the interval $[2,\infty)$ than it is to work on a compact (finite) set. From the appearance of $\pi/x$ in $f$ and the infinite limit of its domain, it is both natural and immediate to attempt the change of variable $y = 1/x$. Because this change reverses the direction of $x$, we now wish to show that $g(y) = \sin{\pi y}/y$ is decreasing on the interval $[0, 1/2]$.

Let's begin a Mathematica implementation by creating $g$ and its derivative:

ClearAll[g, dg];
g[y_] := Sin[\[Pi] y] / y;
dg[y_] := Evaluate @ D[g[y], y]

Why not try the obvious: can we demonstrate that the derivative of $g$ is everywhere negative on this interval simply by requesting its supremum?

Maximize[{dg[y], 0 < y <= 1/2}, y]

The only solution is y -> 0 (reached in 0.11 seconds). This technique exploits two properties of Maximize announced in its documentation:

Maximize will return exact results if given exact input.

If the maximum is achieved only infinitesimally outside the region defined by the constraints, or only asymptotically, Maximize will return the supremum and the closest specifiable point.

Mathematica issues a warning message, because this is a boundary value and in fact dg is not defined at $0$, so to be sure, let's check:

 In[3]:= Limit[dg[y], y -> 0]
Out[3] = 0

Whence--because the supremum is $0$ and occurs uniquely at $y=0$--the derivative of $g$ is non-positive throughout $[0,1/2]$ and negative on $(0,1/2]$, QED.

This problem can also be solved via Taylor's Theorem (with remainder, not just naive inspection of the coefficients) by computing the power series of $g$ around $0$ out to first order and analyzing the remainder term. It becomes so trivial with this approach that Mathematica's power is unneeded, so I won't pursue the details here. It is noteworthy, though, that this solution is available only for g, not for f (where the expansion would be around $\infty$, which doesn't accomplish anything in this case).

---

More generally, when tackling more complex or recalcitrant problems, try to decompose them into simpler pieces; use mathematical identities to reformulate the subproblems; attack the subproblems in multiple ways (rather than focusing on just one method, such as that based on a tangent identity in this problem); and let mathematical principles guide you.

I have no rigorous training in mathematics - I'm not quite sure what constitutes a proof and what doesn't.

How can I properly use Mathematica to prove some theorems like this one? Well, what you can do is use Mathematica to help visualise the function as well as computing derivatives, integrals or limits. My approach is a bit hacky :)

The function

Okay, so we're dealing with x Sin[Pi/x] which is, obviously, a periodic function. It is also even (its plot is symmetric and x Sin[Pi/x] == -x Sin[Pi/-x] evaluates to True). The fact that the function is even is interesting if you want to generalize your "proof".

From the plot of Sin[x],

you can get a good idea of what the plot of x Sin[Pi/x] will look like, even before asking Mathematica to generate it. The fact that Sin[x] has a value between 0 and 1 while $ 0\lt x \leq \pi$ is obvious from the graph. What is also obvious is that the function's value has negative sign from $\pi \leq x \leq 2\pi$.

What are we expecting?

We're expecting a sinusoidal with ascending amplitude and frequency (the x multiplying Sin[Pi/x]). We can guess that because at values of x below 1, we will be evaluating the sine of a number larger than $\pi$, this trend being reversed at x=1. What happens after x=1? Let's ask Mathematica.

Plotting the functions

It turns out we were right about the amplitude and frequency. Right up to a point, at x=1 - past this point, there are no more zeros. There's no need to go further, because it is obvious that our function has an asymptote. But what if we had our PlotRange wrong, and the (presumably more complicated) function really does have zeros after x=1? Let's again ask Mathematica.

It turns out that the limit of our function

Limit[x Sin[Pi/x], x -> \[Infinity]]

is $\pi$. Confirmation of asymptotic behaviour.

What about $\pi \cos (\frac{\pi}{x})$?

You could take a guess like we did before, or simply not bother and ask Mathematica right away.

It is clear from this image that the inequality $x \sin (\frac{\pi}{x})\geq \pi \cos (\frac{\pi}{x})$ can be valid for $x \geq 1$. To confirm, we need to check the limit of the cosine function with

Limit[Pi Cos[Pi/x], x -> \[Infinity]]

which also evaluates to $\pi$. Good news.

But how can I prove it's increasing?

As halirutan said, you can use derivatives. As a non-mathematician, I would be convinced by the plots of the functions, and their limits. If you want to know how fast each function converges to $\pi$, then go ahead and take a look at each function's first/second derivative plot.

This approach might not qualify as rigorous, but I think it shows how you can use Mathematica to walk through math problems.