Prime Counting Function from the Sieve of Eratosthenes

This may seem a very simple question, but I did not find any answer for it on the Internet.

It is known that the Sieve of Erastothenes can be analytically stated as:

$$\pi(x)-\pi(x^{\frac{1}{2}})+1=\sum_{d} (-1)^{\nu(d)} \left \lfloor \frac {x}{d} \right \rfloor$$

Where the sum is over the divisors $d$ of the primorial of order $\sqrt{x}$ (the product of all the primes lower or equal to $\sqrt{x}$), $\nu(d)$ is the number of prime divisors of $d$ and $\pi(x)$ is the Prime Counting Function .

Where can I find a proof of this statement? When I search for information about this sieve online, I only find algorithms for counting primes and approximations or bounds for $\pi(x)$. I understand that this can be a simple subject, but I would like to read a formal proof about it.

Thank you.

Consider a number $x$ and a list of primes $p_i$ less than $\sqrt{x},$ $p_1,p_2,...,p_m.$ Sieve out multiples of primes in the list less than $x,$ to wit: $2, 4, 6,...,$ etc., $3,6,9,...,$ etc., so that we have taken out $[x/2], [x/3],...,[x/p_i]$, etc., numbers.

Some of those we removed are are duplicates since, for example, $6$ would be removed both as a multiple of $2$ and of $3$. So remove from this initial sieving multiples of two primes, $2\cdot3, 3\cdot 5,$ etc., so we are excluding from the sieve $[x/6],[x/15],...,[x/(p_ip_j)]$ numbers.

But again we are removing some numbers twice, such as 30, which has as divisors both $2\cdot3$ and $3\cdot 5.$ We throw those back into the sieve.

We continue until we reach the prime $p_m.$ Having sieved for all primes less than $\sqrt{x}$ we are left with primes between $\sqrt{x}$ and $x$, as well as $1,$ which was not sieved.

So we have

$$\pi(x)-\pi(\sqrt{x})+ 1 = x-[x/2]-[x/3]...+[x/(2\cdot3]+[x/(3\cdot 5)]...- [x/(2\cdot3\cdot 5)])...$$

A more compact notation for this expression is

$$\pi(x)-\pi(\sqrt{x})=~-1 + \sum_{d|D}\mu(d)\left[\frac{x}{d}\right]$$

in which $\mu(x)$ is the Mobius function and $D$ is the product of primes less than or equal to $\sqrt{x}$. A proof that the Mobius function assigns the correct sign to each expression $[x/d]$ can be found in many references $^1$. The point is that the right hand side is the number of numbers in $(1,x)$ which are coprime to primes less than or equal to $p_m,$ the largest prime not exceeding $\sqrt{x}.$ We subtract 1 because it is left over and not considered a prime.

The expression on the right can also be expressed in terms of sets. Anything that captures the inclusion-exclusion process described above is acceptable.

$^1 [x]$ is the floor function, often denoted $\lfloor x \rfloor$ in modern texts.

$^2$ See, for example, Narkiewicz, The Development of Prime Number Theory at p.33.