# Show that $\int_0^{\frac{\pi}{2}}\frac{ x}{ \tan x}dx=\frac{\pi}{2} \ln 2$

I would like to prove that

$$\int_0^{\frac{\pi}{2}}\frac{ x}{ \tan x}dx=\frac{\pi}{2} \ln 2.$$

None of the integration techniques seems to work.

For $t>0$, define
$f(t)=\int_0^{\frac{\pi}{2}}\frac{\tan^{-1}(t \tan x)}{\tan x}dx,$
and not that
$f(1)=\int_0^{\frac{\pi}{2}}\frac{x}{\tan x}dx.$
Then
$f'(t)=\int_0^{\frac{\pi}{2}}\frac{\tan x}{1+(t \tan x)^2}\cdot \frac{1}{\tan x}dx=\int_0^{\frac{\pi}{2}}\frac{1}{1+(t \tan x)^2}dx$
$=\int_0^{\frac{\pi}{2}}\frac{\sec^2 x}{1+(t \tan x)^2}\cdot \frac{1}{1+\tan^2 x}dx$
$=\int_0^{\infty}\frac{1}{1+t^2 u^2}\cdot\frac{1}{1+u^2}du (u=\tan x)$
$=\frac{1}{t^2-1}\int_0^{\infty} \frac{t^2}{1+t^2 u^2}-\frac{1}{1+u^2}du$
$=\frac{1}{t^2-1} \big( t^2\cdot \frac{\tan^{-1}(tu)}{t}-\tan^{-1}u\big)|_0^{\infty}$
$=\frac{1}{t^2-1} \big( t^2\cdot \frac{\frac{\pi}{2}}{t}-\frac{\pi}{2}\big)-0=\frac{1}{t^2-1} (t-1)\frac{\pi}{2}$
$=\frac{\pi}{2}\frac{1}{t+1}.$
Thus
$f'(t)=\frac{\pi}{2}\frac{1}{t+1} \Rightarrow f(t)=\frac{\pi}{2}\ln (t+1)+C.$
It is easy to see that $f(0)=0=C$. Hence
$f(t)=\frac{\pi}{2}\ln (t+1).$
Therefore
$\int_0^{\frac{\pi}{2}}\frac{x}{\tan x}dx=f(1)=\frac{\pi}{2}\ln (2).$