Proof of The Least Positive Zero of the Cosine

Each result cited below is universally quantified over the data in its own statement; it is applied to the data named at the point of use.

Numerals and order. Write $2=1+1$ and $3=2+1$. By claim 6 of Elementary Order Arithmetic in an Ordered Field one has $0<1$; claim 3 of that lemma, applied with $0<1$ and $r\le r$, gives $r<r+1$ for every $r\in\mathbb{R}$, so $0<1<2<3$, and claim 2 of that lemma gives $0<2$, $0<3$ and $1<3$. The additive identity and additive inverses of the field $\mathbb{R}$ give $1-0=1$ and $3-1=2$. The order of $\mathbb{R}$ is a total order, as recorded in the preamble of Elementary Order Arithmetic in an Ordered Field; we use below that a real number which is neither zero nor negative is positive, and that two real numbers neither of which is less than the other are equal.

Standing facts about $\cos$ and $\sin$. Every point of $\mathbb{R}$ is an interior point of the interval $\mathbb{R}$ by Basic Facts about Intervals of the Real Line (i), and by Basic Facts about Intervals of the Real Line (v) a closed interval $[a,b]$ with $a<b$ is an interval every point of which strictly between $a$ and $b$ is an interior point of it. By Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine (ii) and claim 1 of Restriction Stability of Continuity and of the Derivative, the restriction of $\cos$ or of $\sin$ to such an $[a,b]$ is continuous on $[a,b]$; by Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine (v) and claim 2 of Restriction Stability of Continuity and of the Derivative, it is differentiable at every $t$ with $a<t<b$, with derivative $-\sin t$ in the case of $\cos$ and $\cos t$ in the case of $\sin$. So Mean Value Theorem on a Closed Real Interval and on Any Interval and Intermediate Value Theorem on a Closed Real Interval, and Continuous Images of Intervals apply to these restrictions, and are used below without repeating this verification. Also $\cos0=1$ and $\sin0=0$ by Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine (iii).

Claim 1 (mean value identities). Let $a,b\in\mathbb{R}$ with $a<b$. Then there are $c,d$ with $a<c<b$ and $a<d<b$ such that

$$\sin b-\sin a=\cos(c)\,(b-a), \qquad \cos b-\cos a=-\sin(d)\,(b-a).$$

Indeed claim 1 of Elementary Order Arithmetic in an Ordered Field, applied with $c=-a$, turns $a<b$ into $0=a-a<b-a$, so $b-a$ is nonzero and, by claim 7 of that lemma, invertible; Mean Value Theorem on a Closed Real Interval and on Any Interval, applied to the restriction of $\sin$ to $[a,b]$, gives $c\in(a,b)$ with $\cos c=(\sin b-\sin a)(b-a)^{-1}$, and multiplying by $b-a$ gives the first identity. The second follows in the same way from the restriction of $\cos$, whose derivative at $d$ is $-\sin d$.

Claim 2 (a negative value forces an earlier zero). Let $t\in\mathbb{R}$ with $0\le t$ and $\cos t<0$. Then there is $c$ with $0\le c\le t$ and $\cos c=0$.

Since $\cos0=1$ and $0<1$, we have $\cos t<0<1=\cos 0$, so $t\ne0$ and hence $0<t$. Then $\cos t\le0\le\cos0$, so Intermediate Value Theorem on a Closed Real Interval, and Continuous Images of Intervals, applied to the restriction of $\cos$ to $[0,t]$ with $y=0$, gives $c\in[0,t]$ with $\cos c=0$.

Claim 3 (the cosine has a zero in $[0,3]$). The set

$$Z=\{t\in\mathbb{R}:0\le t\le3\ \text{and}\ \cos t=0\}$$

is nonempty.

Suppose $Z$ is empty; we derive a contradiction in five steps.

(i) $0<\cos t$ for every $t$ with $0\le t\le3$. Such a $t$ has $\cos t\ne0$, since otherwise $t\in Z$. If $\cos t<0$, Claim 2 gives $c$ with $0\le c\le t\le3$ and $\cos c=0$, so $c\in Z$, again impossible. Being neither zero nor negative, $\cos t$ is positive.

(ii) $0<\sin t$ for every $t$ with $0<t\le3$. By Claim 1 on $[0,t]$ there is $c$ with $0<c<t$ and $\sin t=\sin t-\sin0=\cos(c)(t-0)=\cos(c)\,t$. Here $0<\cos c$ by (i), since $0\le c\le3$, and $0<t$; so $0<\sin t$ by claim 5 of Elementary Order Arithmetic in an Ordered Field.

(iii) If $0\le u<v\le3$ then $\sin u<\sin v$ and $\cos v<\cos u$. By Claim 1 on $[u,v]$ there are $c,d$ with $u<c<v$ and $u<d<v$ such that $\sin v-\sin u=\cos(c)(v-u)$ and $\cos v-\cos u=-\sin(d)(v-u)$. Now $0<v-u$, and $0<\cos c$ by (i) while $0<\sin d$ by (ii), because $0<d$ and $d\le3$. Hence $0<\cos(c)(v-u)$ and $0<\sin(d)(v-u)$ by claim 5 of Elementary Order Arithmetic in an Ordered Field. Since $\cos(c)(v-u)=\sin v-\sin u$, claim 1 of that lemma, applied with $c=\sin u$, turns $0<\sin v-\sin u$ into $\sin u<\sin v$; and since $\sin(d)(v-u)=\cos u-\cos v$, the same claim applied with $c=\cos v$ turns $0<\cos u-\cos v$ into $\cos v<\cos u$.

(iv) $1<\sin1+\sin1$. By Claim 1 on $[0,1]$ there is $c$ with $0<c<1$ and $\sin1=\sin1-\sin0=\cos(c)(1-0)=\cos c$; by (iii) with $u=c$, $v=1$ we get $\cos1<\cos c=\sin1$. Again by Claim 1 on $[0,1]$ there is $d$ with $0<d<1$ and $\cos1-1=\cos1-\cos0=-\sin(d)(1-0)=-\sin d$, that is $\cos1=1-\sin d$; by (iii) with $u=d$, $v=1$ we get $\sin d<\sin1$, so claim 4 of Elementary Order Arithmetic in an Ordered Field gives $-\sin1<-\sin d$ and claim 1 of that lemma, applied with $c=1$, gives $1-\sin1<1-\sin d=\cos1$. Chaining this with $\cos1<\sin1$ by claim 2 of that lemma yields $1-\sin1<\sin1$, and claim 1 once more, applied with $c=\sin1$, turns that into $1<\sin1+\sin1$.

(v) By Claim 1 on $[1,3]$ there is $d$ with $1<d<3$ and $\cos3-\cos1=-\sin(d)(3-1)=-2\sin d$, that is $\cos3=\cos1-2\sin d$. By (iii) with $u=1$, $v=d$ we get $\sin1<\sin d$, so claim 10 of Elementary Order Arithmetic in an Ordered Field, applied with the factor $2$, which is positive by claim 8 of that lemma, gives $2\sin1<2\sin d$; and $2\sin1=(1+1)\sin1=\sin1+\sin1$ by distributivity and the multiplicative identity, so (iv) and claim 2 of Elementary Order Arithmetic in an Ordered Field give $1<2\sin d$. Claim 4 of that lemma turns this into $-2\sin d<-1$, and claim 3 of that lemma, applied with $-2\sin d<-1$ and $\cos1\le\cos1$, gives

$$\cos3=\cos1-2\sin d<\cos1-1 .$$

By The Pythagorean Identity for Sine and Cosine (ii) and claim 3 of Properties of the Absolute Value in an Ordered Field we have $\cos1\le|\cos1|\le1$; transitivity of $\le$, obtained from claims 2 and 3 of Elementary Arithmetic in an Ordered Field, gives $\cos1\le1$, and claim 3 of that lemma gives $\cos1-1\le0$. Hence $\cos3<0$ by claim 2 of Elementary Order Arithmetic in an Ordered Field, contradicting (i). Therefore $Z$ is nonempty.

Claim 4 (clause 1). By Claim 3 the set $Z$ is nonempty, and $0$ is a lower bound for it, so $x_{0}=\inf Z$ exists by Existence of the Infimum of a Nonempty Subset of $\mathbb{R}$ Bounded Below. As $0$ is a lower bound and $\inf Z$ is the greatest lower bound, $0\le x_{0}$; and choosing any $z\in Z$ gives $x_{0}\le z\le3$, so transitivity of $\le$ gives $x_{0}\le3$ and $x_{0}$ lies in $[0,3]$.

(a) $\cos x_{0}=0$. Suppose not, and put $\varepsilon=|\cos x_{0}|$, which is positive by claim 1 of Properties of the Absolute Value in an Ordered Field. By Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine (ii) and continuity of $\cos$ at $x_{0}$ relative to $\mathbb{R}$, formed with the metric $d_{\mathbb{R}}$ of The Real Numbers: Standing Notation and Background (i), there is $\delta>0$ such that every $t\in\mathbb{R}$ with $|t-x_{0}|<\delta$ satisfies $|\cos t-\cos x_{0}|<\varepsilon$. No such $t$ lies in $Z$: if $\cos t=0$ then $|\cos t-\cos x_{0}|=|-\cos x_{0}|=|\cos x_{0}|=\varepsilon$ by claim 2 of Properties of the Absolute Value in an Ordered Field, not less than $\varepsilon$. But claim 4 of Approximation Property of the Supremum and the Infimum in $\mathbb{R}$, applied to $Z$ with the positive number $\delta$, gives $z\in Z$ with $z<x_{0}+\delta$; since $x_{0}$ is a lower bound, $x_{0}\le z$, so $0\le z-x_{0}$ by claim 3 of Elementary Arithmetic in an Ordered Field, while claim 1 of Elementary Order Arithmetic in an Ordered Field, applied to $z<x_{0}+\delta$ with $c=-x_{0}$, gives $z-x_{0}<\delta$. Therefore $|z-x_{0}|=z-x_{0}<\delta$ by Absolute Value in an Ordered Field. This is a contradiction, so $\cos x_{0}=0$.

(b) $0<x_{0}$. If $x_{0}=0$ then $\cos x_{0}=\cos0=1$, which is nonzero, contradicting (a). With $0\le x_{0}$ this gives $0<x_{0}$.

(c) $0<\cos t$ for every $t$ with $0\le t<x_{0}$. Such a $t$ satisfies $t<x_{0}\le3$, so $0\le t\le3$; and $t\notin Z$, since $x_{0}$ is a lower bound for $Z$ and $t<x_{0}$. Hence $\cos t\ne0$. If $\cos t<0$, Claim 2 gives $c$ with $0\le c\le t\le3$ and $\cos c=0$, so $c\in Z$ while $c\le t<x_{0}$, contradicting that $x_{0}$ is a lower bound for $Z$. Being neither zero nor negative, $\cos t$ is positive.

(d) Uniqueness. Let $y\in\mathbb{R}$ satisfy $0<y$, $\cos y=0$ and $0<\cos t$ for every $t$ with $0\le t<y$. If $y<x_{0}$ then $0\le y<x_{0}$, so $0<\cos y$ by (c), contradicting $\cos y=0$. If $x_{0}<y$ then $0\le x_{0}<y$, so $0<\cos x_{0}$ by the assumed property of $y$, contradicting (a). Neither is less than the other, so $y=x_{0}$.

Together with $x_{0}\le3$ this proves clause 1.

Claim 5 (clause 2). Let $t$ satisfy $0<t\le x_{0}$. By Claim 1 on $[0,t]$ there is $c$ with $0<c<t$ and $\sin t=\sin t-\sin0=\cos(c)(t-0)=\cos(c)\,t$. Here $0\le c$ and $c<t\le x_{0}$, so $0<\cos c$ by clause 1; with $0<t$, claim 5 of Elementary Order Arithmetic in an Ordered Field gives $0<\sin t$.

In particular $0<\sin x_{0}$. By The Pythagorean Identity for Sine and Cosine (i),

$$(\cos x_{0})^{2}+(\sin x_{0})^{2}=1,$$

and $(\cos x_{0})^{2}=0\cdot0=0$ by (a) of Claim 4 and claim 1 of Zero Products and Elementary Identities in a Field; hence $(\sin x_{0})^{2}=1=1\cdot1=1^{2}$. Since $0<\sin x_{0}$ gives $0\le\sin x_{0}$, and $0\le1$ by claim 1 of Elementary Arithmetic in an Ordered Field, claim 3 of Monotonicity of Squaring on the Nonnegative Elements of an Ordered Field gives $\sin x_{0}=1$. This proves clause 2 and completes the proof.