Proof of Addition Formulas for Sine and 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. Sums, constant multiples and products of functions are formed pointwise, as in the statements of Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers and Continuity of Sums and Products of Real-Valued Functions on a Metric Space; those items state their hypotheses for a pair of functions, and where only one function is named below the second is taken to be that same function. Every point of $\mathbb{R}$ is an interior point of the interval $\mathbb{R}$ by Basic Facts about Intervals of the Real Line (i). Multiplication in the field $\mathbb{R}$ is commutative, and claim 2 of Zero Products and Elementary Identities in a Field gives $(-s)r=-(sr)$ for all $s,r\in\mathbb{R}$; both are used below without further comment in rearranging finite sums of products.

Fix $a\in\mathbb{R}$. Let $\tau:\mathbb{R}\to\mathbb{R}$ be given by $\tau(t)=a+t$, and let $f,g:\mathbb{R}\to\mathbb{R}$ be given by

$$f(t)=\cos(a+t)-\bigl(\cos a\cos t-\sin a\sin t\bigr), \qquad g(t)=\sin(a+t)-\bigl(\sin a\cos t+\cos a\sin t\bigr).$$

The two clauses to be proved say exactly that $f(x)=0$ and $g(x)=0$ for every $x\in\mathbb{R}$.

Claim 1 (the derivative of $\tau$). For every $t\in\mathbb{R}$, $\tau$ is differentiable at $t$ with derivative $1$.

By claim 1 of Properties of Natural Number Powers in a Field one has $s^{1}=s$ for every $s\in\mathbb{R}$, so the identity function of $\mathbb{R}$ is the map $s\mapsto s^{1}$, and claim 1 of Derivative of a Polynomial Function on the Real Line, applied with $I=\mathbb{R}$, gives that it is differentiable at $t$ with derivative $1$. Since $\tau$ is the sum of the function with constant value $a$ and the identity function, claims 1 and 2 of Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers give that $\tau$ is differentiable at $t$ with derivative $0+1=1$.

Claim 2 ($f'=-g$ and $g'=f$). For every $t\in\mathbb{R}$, $f$ is differentiable at $t$ with derivative $-g(t)$, and $g$ is differentiable at $t$ with derivative $f(t)$.

By Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine (v), $\cos$ is differentiable at every $s\in\mathbb{R}$ with derivative $-\sin s$, and $\sin$ is differentiable at $s$ with derivative $\cos s$. Every value of $\tau$ lies in $\mathbb{R}$, and $t$ and $\tau(t)$ are interior points of $\mathbb{R}$, so Chain Rule for Real Functions on Intervals, applied with $I=J=\mathbb{R}$, inner function $\tau$ and outer function $\cos$, gives that $\cos\circ\tau$ is differentiable at $t$ with derivative $(-\sin(a+t))\cdot1=-\sin(a+t)$; with outer function $\sin$ it gives that $\sin\circ\tau$ is differentiable at $t$ with derivative $\cos(a+t)$.

The function $t\mapsto\cos a\cos t-\sin a\sin t$ is the sum of the constant multiple of $\cos$ by $\cos a$ and the constant multiple of $\sin$ by $-\sin a$, so claim 2 of Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers gives that it is differentiable at $t$ with derivative

$$\cos a(-\sin t)+(-\sin a)\cos t=-\bigl(\sin a\cos t+\cos a\sin t\bigr).$$

Since $f$ is the sum of $\cos\circ\tau$ and the constant multiple of that function by $-1$, claim 2 of Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers gives that $f$ is differentiable at $t$ with derivative

$$-\sin(a+t)+\bigl(\sin a\cos t+\cos a\sin t\bigr)=-g(t).$$

In the same way $t\mapsto\sin a\cos t+\cos a\sin t$ is differentiable at $t$ with derivative $\sin a(-\sin t)+\cos a\cos t=\cos a\cos t-\sin a\sin t$, so $g$ is differentiable at $t$ with derivative

$$\cos(a+t)-\bigl(\cos a\cos t-\sin a\sin t\bigr)=f(t).$$

Claim 3 (the sum of squares). Let $h:\mathbb{R}\to\mathbb{R}$ be the function $h=ff+gg$, that is, $h(t)=f(t)f(t)+g(t)g(t)$. Then $h$ is continuous on $\mathbb{R}$ and differentiable at every $t\in\mathbb{R}$ with derivative $0$.

By Claim 2 and claim 3 of Derivatives of Constants, the Identity, Sums, Scalar Multiples, Products, Reciprocals, Quotients and Powers, applied at $t$ with both functions taken to be $f$, the function $ff$ is differentiable at $t$ with derivative $(-g(t))f(t)+f(t)(-g(t))$; with both taken to be $g$, the function $gg$ is differentiable at $t$ with derivative $f(t)g(t)+g(t)f(t)$. Claim 2 of that lemma gives that $h$ is differentiable at $t$ with derivative the sum of these four terms, each of the first two being $-(f(t)g(t))$ and each of the last two being $f(t)g(t)$; by the additive inverse axiom of $\mathbb{R}$ they cancel in pairs, so the derivative is $0$.

By Claim 2 and The Increment Form of the Derivative, and Differentiability Implies Continuity, applied with $I=\mathbb{R}$, the functions $f$ and $g$ are continuous at every point of $\mathbb{R}$ relative to $\mathbb{R}$, hence continuous on $\mathbb{R}$; claim 5 of Continuity of Sums and Products of Real-Valued Functions on a Metric Space, applied with $(X,d)=(\mathbb{R},d_{\mathbb{R}})$ and $A=\mathbb{R}$ — first to the pair $f,f$, then to the pair $g,g$, then to the pair $ff,gg$ — then gives in turn that $ff$, $gg$ and their sum $h$ are continuous on $\mathbb{R}$.

Claim 4 ($h$ vanishes identically). Let $x\in\mathbb{R}$ and put $R=1+|x|$. By claim 1 of Properties of the Absolute Value in an Ordered Field one has $0\le|x|$, and $0<1$ by claim 6 of Elementary Order Arithmetic in an Ordered Field. Claim 3 of the latter, applied with $0<1$ and $|x|\le|x|$, gives $|x|=0+|x|<1+|x|=R$; applied with $0<1$ and $0\le|x|$ it gives $0=0+0<R$. By claim 9 of Properties of the Absolute Value in an Ordered Field these mean $-R<x<R$ and $-R<0<R$, so $x$ and $0$ both lie in the closed interval $[-R,R]$, which by Basic Facts about Intervals of the Real Line (v) is an interval every point of which strictly between $-R$ and $R$ is an interior point of it.

By Claim 3 and the two claims of Restriction Stability of Continuity and of the Derivative, the restriction $h|_{[-R,R]}$ is continuous on $[-R,R]$ and differentiable with derivative $0$ at every $t$ with $-R<t<R$. Hence A Continuous Function with Vanishing Derivative is Constant, applied with $a=-R$ and $b=R$, gives $h(t)=h(-R)$ for every $t\in[-R,R]$, so $h(x)=h(-R)=h(0)$.

Now $a+0=a$ by the additive identity of $\mathbb{R}$, and $\cos0=1$, $\sin0=0$ by Uniform Convergence, Continuity, Parity and Derivatives of Sine and Cosine (iii); so, by the multiplicative identity and claim 1 of Zero Products and Elementary Identities in a Field,

$$f(0)=\cos a-\bigl(\cos a\cdot1-\sin a\cdot0\bigr)=\cos a-\cos a=0, \qquad g(0)=\sin a-\bigl(\sin a\cdot1+\cos a\cdot0\bigr)=\sin a-\sin a=0 .$$

Hence $h(0)=0\cdot0+0\cdot0=0$ by claim 1 of Zero Products and Elementary Identities in a Field, and therefore $h(x)=0$.

Claim 5 (the two clauses). Let $x\in\mathbb{R}$. By Claim 4, $f(x)f(x)+g(x)g(x)=0$, and both summands are nonnegative by claim 2 of Nonnegativity of Squares in an Ordered Field. Let $a_{1}=f(x)f(x)$ and $a_{2}=g(x)g(x)$, a family indexed by the initial segment of $2=S(1)$; claim 1 of Properties of Finite Sums gives $\sum_{k=1}^{2}a_{k}=a_{1}+a_{2}$, which is therefore $0$, so claim 5 of that lemma gives $a_{1}=0$ and $a_{2}=0$. By claim 3 of Zero Products and Elementary Identities in a Field, $f(x)=0$ and $g(x)=0$.

Unwinding the definitions of $f$ and $g$, this says

$$\cos(a+x)=\cos a\cos x-\sin a\sin x, \qquad \sin(a+x)=\sin a\cos x+\cos a\sin x .$$

As $a\in\mathbb{R}$ was fixed arbitrarily at the outset and $x\in\mathbb{R}$ was arbitrary, both clauses hold for all $a,x\in\mathbb{R}$.