The Real Sine and Cosine Functions

In the setting of The Real Numbers: Standing Notation and Background, let $x$ be a real number, let $k!$ denote the factorial of $k\in\mathbb{N}$, and let $c^{n}$ denote the $n$th power of a real number $c$. Convergence of a series of real numbers and its sum are as defined there. For $k\in\mathbb{N}$ the natural numbers $2k$ and $2k+1$ are the abbreviations of Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials §powers. Every exponent occurring below is therefore a natural number, and every factorial is the factorial of a natural number, so neither a zeroth power nor a factorial of zero is formed.

1. (Cosine)¶ The series $\sum_{k=1}^{\infty}\dfrac{(-1)^{k}x^{2k}}{(2k)!}$ converges, and the cosine of $x$ is the real number

2. (Sine)¶ The series $\sum_{k=1}^{\infty}\dfrac{(-1)^{k}x^{2k+1}}{(2k+1)!}$ converges, and the sine of $x$ is the real number

Both convergence assertions hold for the following reason. Write $A=|x|$ for the absolute value of $x$, so that $0\le A$. Since $0\le1$ by claim 1 of Elementary Arithmetic in an Ordered Field, that definition gives $|1|=1$, and claim 2 of Properties of the Absolute Value in an Ordered Field gives $|-1|=1$; hence $|(-1)^{k}|=|-1|^{k}=1^{k}=1$ for every $k\in\mathbb{N}$, by Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials §powers and claim 2 of Properties of Natural Number Powers in a Field. The factorials $(2k)!$ and $(2k+1)!$ are positive by Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials §factorial, so each equals its own absolute value; moreover, for a positive real $w$, claim 4 of Properties of the Absolute Value in an Ordered Field gives $|w|\,|w^{-1}|=|w\,w^{-1}|=|1|=1$, so $|w^{-1}|=|w|^{-1}$. Therefore that same claim 4, together with $|x^{n}|=|x|^{n}$ from Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials §powers, gives

for every $k\in\mathbb{N}$. These are the terms of the two series shown convergent in Iterated Powers, Factorials, and Convergence of the Series of Powers over Factorials §trigonometric, so the domination clause An Absolutely Convergent Series of Real Numbers Converges §dominated shows that each of the two series above converges absolutely, and An Absolutely Convergent Series of Real Numbers Converges §convergence then shows that each converges. This makes $\cos$ and $\sin$ functions from $\mathbb{R}$ to $\mathbb{R}$.