Sturm sign variation counts distinct real polynomial roots

The degrees of nonzero Euclidean remainders strictly decrease by [F1], so the sequence terminates. Changing each Euclidean remainder by a minus sign changes neither common divisors nor termination. Thus [F6] and the stated gcd $1$ make the last nonzero remainder a nonzero constant $c$. Backward substitution in the division equations gives $A,B\in \mathbb{Q}[x]$ with $A{P}_0+B{P}_1=c$; dividing by $c$ gives a Bezout identity with right side $1$.

Between zeros of the sequence, every polynomial keeps its sign: a sign change would give a zero by [F3] and [F4]. Each term has finitely many zeros by [F5], so it suffices to compute how $V$ changes when a real point crosses a zero of one or more sequence terms.

No two consecutive terms can vanish at the same real $c$. By step 1.1 there are $A,B\in \mathbb{Q}[x]$ with $A{P}_0+B{P}_1=1$; evaluating at $c$ rules out a common zero of $P_0,P_1$ even over $\mathbb{C}$. For $1\le j<s$, the recurrence $P_{j-1}=Q_j{P}_j-P_{j+1}$ propagates simultaneous zeros of $P_j,P_{j+1}$ backward to $P_0,P_1$.

Suppose $P_j(c)=0$ for an internal index $1\le j<s$. The no-adjacent-zero property in [step 2.1] makes $P_{j-1}(c)$ and $P_{j+1}(c)$ nonzero, and the recurrence gives $P_{j-1}(c)=-P_{j+1}(c)$. They have opposite signs. On either side of $c$, the signs of these neighbors are fixed; after zero entries are deleted, the adjacent nonzero neighbors of each internal zero contribute exactly one sign change. If several internal terms vanish at $c$, their indices are nonconsecutive, so these adjacent-pair contributions may share an endpoint but remain distinct terms in the total variation. Thus internal zeros do not change $V$.

If $P_0(c)=0$, then squarefreeness gives $P_1(c)=P_0^{\mathrm{\prime }}(c)\mathrm{\ne }0$. Factor $P_0(x)=(x-c)u(x)$ by [F5]; the product rule gives $u(c)=P_1(c)$, so near $c$ the sign of $P_0(x)P_1(x)$ is the sign of $x-c$. Thus the initial pair contributes one sign change just to the left and none just to the right. Any simultaneous internal zeros contribute no net change by [step 3.1], so $V$ decreases by exactly one as $c$ is crossed from left to right.

The endpoints are not roots of $P$ by hypothesis. As one moves from $a$ to $b$, $V$ is constant except at the finitely many roots of sequence terms; by [step 3.1] internal zeros do not change it and by [step 4.1] each distinct root of $P$ lowers it by one. Therefore $V(a)-V(b)$ is exactly the number of distinct roots in $(a,b)$.