Computes the derivative from the one-dimensional product and reciprocal rules, establishes continuity of the reciprocal factor from an explicit local Lipschitz bound, and verifies the four inequalities by ordered-field arithmetic.
Proof
Each result cited below is universally quantified over the data appearing in its own statement, and is applied here to the data named in the step in question. Throughout, D denotes the function from R to R with D(s)=1+Ξ΅s2, and powers are those of Natural Number Power of an Element of a Field, so that s1=s and sS(m)=sms for every natural number m with successor S(m), by claim 1 of Properties of Natural Number Powers in a Field; in particular s2=ss, s3=s2s and s4=s3s. By claim 1 of One-Dimensional Derivatives, Partial Derivatives, and Smoothness on the Real Line, R is an interval every point of which is an interior point of it; all applications below of the one-dimensional differentiation rules take the interval to be R and the interior point to be the point under discussion.
Second, for every natural number m the map sβ¦sm is continuous at every point of R in both readings, and so is sβ¦3s2+Ξ΅s4. Indeed, by claim 2 of Constants, Affine Functions, Sums, Products and Quotients of Cα΅ Functions the constant functions and the single coordinate function of R1, which is the identity map, are smooth on R1, and by claim 3 of that lemma sums, scalar multiples and products of smooth functions are smooth; so each sβ¦sm, being an iterated product of the identity map, and also sβ¦3s2+Ξ΅s4, are smooth on R1. By claim 3 of Euclidean Space Is Open in Itself they are continuous at every point of R1 in both readings.
Third, by claim 5 of Continuity of Sums and Products of Real-Valued Functions on a Metric Space, applied in the metric space (R,dRβ) with A=R, a pointwise product of functions continuous on R in the metric reading is continuous on R in that reading. Applying this to ΟΞ΅β(s)=s3w(s), and twice to ΟΞ΅β²β(s)=(3s2+Ξ΅s4)w(s)w(s) β first to the product of w with itself and then to the product of the result with sβ¦3s2+Ξ΅s4 β shows that ΟΞ΅β and ΟΞ΅β²β are continuous at every point of R in the metric reading, hence also in the Euclidean reading by Euclidean, Metric and Sequential Continuity of a Real Function of a Real Variable (ii).
Finally, by claim 2 of One-Dimensional Derivatives, Partial Derivatives, and Smoothness on the Real Line the partial derivative of ΟΞ΅β with respect to the first variable exists at every point of R1 and β1βΟΞ΅β(s)=ΟΞ΅β²β(s). Thus the single coordinate function of ΟΞ΅β is continuous at every point of R1 in the Euclidean sense, its single first-order partial derivative exists at every point, and that partial derivative is continuous at every point in the Euclidean sense; by clauses 1 and 3 of Functions of Class Cα΅ on an Open Subset of ββΏ, ΟΞ΅β is of class C1 on R1.
Claim 3. Let sβR. By the argument of claim 1 applied to s and to s2 one has 0β€s2 and 0β€s4=(s2)2, hence 0β€3s2 and 0β€Ξ΅s4 and so 0β€3s2+Ξ΅s4; and 0β€w(s)2 likewise. By clause 2 of Ordered Field the product of two nonnegative elements is nonnegative, so 0β€ΟΞ΅β²β(s).
which is nonnegative, since Ξ΅β1 is positive by claim 7 of Elementary Order Arithmetic in an Ordered Field and since 0β€s2 and 0β€Ξ΅s4. Multiplying by the nonnegative number w(s)2 (clause 2 of Ordered Field) and using D(s)2w(s)2=(D(s)w(s))2=1 gives
Taking absolute values and using claim 4 of Properties of the Absolute Value in an Ordered Field repeatedly, together with β£βyβ£=β£yβ£ from claim 2 of that lemma and, by the preliminary remark, β£Ξ΅β£=Ξ΅ and β£w(s)β£=w(s),