Evaluate $\int_0^{\pi/2}\log\cos(x)\,\mathrm{d}x$

For the sake of simplicity, all the integral variables I use are $x$ even there are a lot of substitutions. Because lots of variables could make one confused.

Let $I$ denote the integral value. By substitute $x$ for $\pi/2-x$, we have: \begin{equation} I=\int_0^{\frac{\pi}{2}}\log\cos(x)dx=\int_0^{\frac{\pi}{2}}\log\sin(x)dx \end{equation} And then, we have: \begin{equation} I=\int_0^{\frac{\pi}{2}}\log(2\cos(\frac{x}{2})\sin(\frac{x}{2}))dx\\ =\frac{\pi}{2}\log2+\int_0^{\frac{\pi}{2}}\log\cos(\frac{x}{2})dx+\int_0^{\frac{\pi}{2}}\log\sin(\frac{x}{2})dx\\ =\frac{\pi}{2}\log2+2\int_0^{\frac{\pi}{4}}\log\cos(x)dx+2\int_0^{\frac{\pi}{4}}\log\sin(x)dx\\ =\frac{\pi}{2}\log2+I_1+I_2 \end{equation} In the second step from bottom, I use the substitution that $x=x/2$.

For $I_1$, use the substitution that $x=\pi/2-x$ we obtain \begin{equation} I_1=2\int_{\frac{\pi}{4}}^{\frac{\pi}{2}}\log\sin(x)dx \end{equation} It gives that $I_1+I_2=2I$. So we have \begin{equation} I=\frac{\pi}{2}\log2+2I\\ I=-\frac{\pi}{2}\log2 \end{equation}

$$ \int_0^{\pi/2} \ln \cos xdx =I=\int_0^{\pi/2} \ln \sin x dx. $$ By symmetry we have $\ln \cos x=\ln \sin x$ on the interval $[0,\pi/2]$. This is true for any even/odd function on this interval, as is an exercise in Demidovich-Problems in Analysis. Thus we have $$ 2I=\int_0^{\pi/2}\ln \cos x dx+ \int_0^{\pi/2} \ln \sin x dx= \int_0^{\pi/2} \ln(\sin x \cos x)dx=\int_0^{\pi/2} \ln\big(\frac{1}{2}\cdot\sin(2x)\big) dx. $$ All I used was $\ln(a\cdot b)=\ln(a)+\ln(b)$ and $2\sin x \cos x=\sin(2x)$. Now we split the integral back up to obtain $$ -\int_0^{\pi/2}\ln(2)dx+\int_0^{\pi/2}\ln(\sin(2x))dx=2I. $$ Thus we can now substitute $u=2x$ to obtain $$ -\frac{\pi\ln(2)}{2}+\frac{1}{2}\int_0^\pi \ln \sin (u) du=2I $$ But the integral of $\ln \sin u$ is 2I, thus we have $$ -\frac{\pi\ln(2)}{2}+I=2I, \ \to {\boxed{I=-\frac{\pi \ln(2)}{2}.}} $$

How comes I forgot to write my favorite proof?

We have a well-known identity:

$$\prod_{k=1}^{n-1}\sin\left(\frac{\pi k}{n}\right)=\frac{2n}{2^n}\tag{1}$$ and since $\log\sin x$ is an improperly Riemann-integrable function over $(0,\pi)$, it follows that:

$$ \int_{0}^{\pi}\log\sin\theta\,d\theta = \lim_{n\to +\infty}\frac{\pi}{n}\sum_{k=1}^{n-1}\log\sin\left(\frac{\pi k}{n}\right)=-\pi\log 2,\tag{2}$$ so: $$ \int_{0}^{\pi/2}\log\cos\theta\,d\theta = \int_{0}^{\pi/2}\log\sin\theta\,d\theta = \color{red}{-\frac{\pi}{2}\log 2}.\tag{3}$$