If the cosine had no zero in it would be positive there, making the sine increasing and the cosine decreasing; two applications of the mean value theorem on give , and a third on then forces . The least positive zero is the infimum of the zero set, which belongs to it by continuity.
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 and . By claim 6 of Elementary Order Arithmetic in an Ordered Field one has ; claim 3 of that lemma, applied with and , gives for every , so , and claim 2 of that lemma gives , and . The additive identity and additive inverses of the field give and . The order of 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 and . Every point of is an interior point of the interval by Basic Facts about Intervals of the Real Line and Their Interior Points §whole-line, and by Basic Facts about Intervals of the Real Line and Their Interior Points §closed-interval a closed interval with is an interval every point of which strictly between and is an interior point of it. By Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine §continuous and claim 1 of Restriction Stability of Continuity and of the Derivative, the restriction of or of to such an is continuous on ; by Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine §derivative and claim 2 of Restriction Stability of Continuity and of the Derivative, it is differentiable at every with , with derivative in the case of and in the case of . So Mean Value Theorem on a Closed Real Interval and Intermediate Value Theorem on a Closed Real Interval apply to these restrictions, and are used below without repeating this verification. Also and by Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine §values.
Claim 1 (mean value identities). Let with . Then there are with and such that
Indeed claim 1 of Elementary Order Arithmetic in an Ordered Field, applied with , turns into , so is nonzero and, by claim 7 of that lemma, invertible; Mean Value Theorem on a Closed Real Interval, applied to the restriction of to , gives with , and multiplying by gives the first identity. The second follows in the same way from the restriction of , whose derivative at is .
Claim 2 (a negative value forces an earlier zero). Let with and . Then there is with and .
Since and , we have , so and hence . Then , so Intermediate Value Theorem on a Closed Real Interval, applied to the restriction of to with , gives with .
Claim 3 (the cosine has a zero in ). The set
is nonempty.
Suppose is empty; we derive a contradiction in five steps.
(i) for every with . Such a has , since otherwise . If , Claim 2 gives with and , so , again impossible. Being neither zero nor negative, is positive.
(ii) for every with . By Claim 1 on there is with and . Here by (i), since , and ; so by claim 5 of Elementary Order Arithmetic in an Ordered Field.
(iii) If then and . By Claim 1 on there are with and such that and . Now , and by (i) while by (ii), because and . Hence and by claim 5 of Elementary Order Arithmetic in an Ordered Field. Since , claim 1 of that lemma, applied with , turns into ; and since , the same claim applied with turns into .
(iv) . By Claim 1 on there is with and ; by (iii) with , we get . Again by Claim 1 on there is with and , that is ; by (iii) with , we get , so claim 4 of Elementary Order Arithmetic in an Ordered Field gives and claim 1 of that lemma, applied with , gives . Chaining this with by claim 2 of that lemma yields , and claim 1 once more, applied with , turns that into .
(v) By Claim 1 on there is with and , that is . By (iii) with , we get , so claim 10 of Elementary Order Arithmetic in an Ordered Field, applied with the factor , which is positive by claim 8 of that lemma, gives ; and by distributivity and the multiplicative identity, so (iv) and claim 2 of Elementary Order Arithmetic in an Ordered Field give . Claim 4 of that lemma turns this into , and claim 3 of that lemma, applied with and , gives
By The Pythagorean Identity for Sine and Cosine §bounds and claim 3 of Properties of the Absolute Value in an Ordered Field we have ; transitivity of , obtained from claims 2 and 3 of Elementary Arithmetic in an Ordered Field, gives , and claim 3 of that lemma gives . Hence by claim 2 of Elementary Order Arithmetic in an Ordered Field, contradicting (i). Therefore is nonempty.
Claim 4 (clause 1). By Claim 3 the set is nonempty, and is a lower bound for it, so exists by Existence of the Infimum of a Nonempty Subset of Bounded Below. As is a lower bound and is the greatest lower bound, ; and choosing any gives , so transitivity of gives and lies in .
(a) . Suppose not, and put , 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 §continuous and continuity of at relative to , formed with the metric of The Real Numbers: Standing Notation and Background §numbers, there is such that every with satisfies . No such lies in : if then by claim 2 of Properties of the Absolute Value in an Ordered Field, not less than . But claim 4 of Approximation Property of the Supremum and the Infimum in , applied to with the positive number , gives with ; since is a lower bound, , so by claim 3 of Elementary Arithmetic in an Ordered Field, while claim 1 of Elementary Order Arithmetic in an Ordered Field, applied to with , gives . Therefore by Absolute Value in an Ordered Field. This is a contradiction, so .
(b) . If then , which is nonzero, contradicting (a). With this gives .
(c) for every with . Such a satisfies , so ; and , since is a lower bound for and . Hence . If , Claim 2 gives with and , so while , contradicting that is a lower bound for . Being neither zero nor negative, is positive.
(d) Uniqueness. Let satisfy , and for every with . If then , so by (c), contradicting . If then , so by the assumed property of , contradicting (a). Neither is less than the other, so .
Together with this proves clause 1.
Claim 5 (clause 2). Let satisfy . By Claim 1 on there is with and . Here and , so by clause 1; with , claim 5 of Elementary Order Arithmetic in an Ordered Field gives .
In particular . By The Pythagorean Identity for Sine and Cosine §identity,
and by (a) of Claim 4 and claim 1 of Zero Products and Elementary Identities in a Field; hence . Since gives , and 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 . This proves clause 2 and completes the proof.
Loading…
Prerequisites
7d8d774d-9b16-4046-b348-99032ac41baf