Proof of Kit for def:sine-cosine-real

Facts about maps and predicative formulas carried by Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (vi) are used without comment. The parameters are those of the statement, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); in formulas, $\oplus$ and $\odot$ denote the sum and product operations of $\mathbb{C}$, $\jmath$ its imaginary unit, and $\iota:\mathbb{R}\to\mathbb{C}$ the map of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi). Throughout, the values of the parameters are sets: $\mathbb{N}$, $\mathbb{R}$ and $\mathbb{C}$ (The Set of Natural Numbers and the Number One (i), The Real Numbers (i), The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii)); the constants $1\in\mathbb{N}$, $1,\jmath\in\mathbb{C}$ and $0\in\mathbb{R}$ as elements of sets (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v), The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iv), The Real Numbers (iv), Classes, Membership, Sets and Proper Classes (i)); $\iota$, the addition of $\mathbb{N}_{0}$, $\oplus$, $\odot$, $+$ and $d_{\mathbb{C}}$ as maps between sets, hence elements of classes $B^{A}$ of functions from $A$ to $B$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi), Addition on Omega (i), The Real Numbers (iii), The Distance on the Complex Numbers (i), Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)); and $\le$ and its strict order $<$ as subclasses of the set $\mathbb{R}\times\mathbb{R}$ (Partial and Total Orders on a Set and the Associated Strict Relation (i), Relations, Domain, Range, Inverse and Composition (vi), Partial and Total Orders on a Set and the Associated Strict Relation (iii), Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). We write $F,E$ for the distinct set variables $x_{0},x_{1}$ of Renaming and Substituting Variables in Predicative Formulas, the given $x_{0},\dots,x_{n-1}$ being the first of the variables $x_{0},x_{1},\dots$ there; we build predicative formulas in $F$ alone and move them to the position $i$ at the end. The letters $t,a,p,v,w,b,q,r,s$ denote further pairwise distinct set variables, distinct from $x_{0}$ and $x_{1}$. The parameters are set variables other than $x_{0},\dots,x_{n-1}$, other than $x_{0},x_{1}$, and other than these letters and all other bound variables used below.

The defining identities. The Real Sine and Cosine Functions (i) and The Real Sine and Cosine Functions (ii) adopt Complex Analysis: Standing Notation, in which a real number $t$ stands for $\iota(t)$ wherever a complex number is required (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (v)). So $\cos$ and $\sin$ are maps $\mathbb{R}\to\mathbb{R}$ with

$$\cos t=\operatorname{Re}\exp\bigl(\jmath\,\iota(t)\bigr),\qquad \sin t=\operatorname{Im}\exp\bigl(\jmath\,\iota(t)\bigr)\qquad\text{for every }t\in\mathbb{R}.$$

The real and imaginary parts there are those of Real and Imaginary Parts of a Complex Number (i): for $w\in\mathbb{C}$, $\operatorname{Re}w$ and $\operatorname{Im}w$ are the real numbers $a$ and $b$ with $w=\iota(a)+\iota(b)\,\jmath$, which exist and are unique by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (vii). Hence, for $w\in\mathbb{C}$ and $a\in\mathbb{R}$,

$$\operatorname{Re}w=a\iff w=\iota(a)+\iota(b)\,\jmath\ \text{for some }b\in\mathbb{R},\qquad \operatorname{Im}w=a\iff w=\iota(b)+\iota(a)\,\jmath\ \text{for some }b\in\mathbb{R}.$$

Reading rules. (a) For all sets $u$ and $y$: $(u,y)\in\iota$ if and only if $u\in\mathbb{R}$ and $y=\iota(u)$; $(u,y)\in\exp$ if and only if $u\in\mathbb{C}$ and $y=\exp u$; and, for a map $G:\mathbb{R}\to\mathbb{R}$, $(u,y)\in G$ if and only if $u\in\mathbb{R}$ and $y=G(u)$. These are Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii), $\exp$ being a map $\mathbb{C}\to\mathbb{C}$ (The Complex Exponential Function (i)). (b) For $u,y\in\mathbb{C}$ and every set $g$: $((u,y),g)\in{\oplus}$ if and only if $g=u+y$, and $((u,y),g)\in{\odot}$ if and only if $g=uy$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi) for the binary operations of $\mathbb{C}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii)). (c) By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), each formula of the form $(\cdot,\cdot)\in\cdot$ or $((\cdot,\cdot),\cdot)\in\cdot$ written below is predicative and, when sets are assigned to the variables inside the pairs, holds if and only if the corresponding membership of ordered pairs holds; the value of $\jmath$ is a set, as noted at the start. Each formula below is built from such formulas and from formulas already shown predicative by connectives and quantifiers over set variables, with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi); so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

The exponential. Kit for def:complex-exponential (i), for one variable and the position $0$, gives a predicative formula in $x_{0}$ expressing that $x_{0}$ is the complex exponential function; its parameters are among those of the statement. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$, $n=2$ and $\sigma(0)=1$, it becomes a predicative formula $\varepsilon(E)$ in $x_{0},x_{1}$, with bound variables renamed to differ from the letters above, that holds exactly when $E$ is the complex exponential function. The function $\exp$ is a set: as a map $\mathbb{C}\to\mathbb{C}$ it lies in the class $\mathbb{C}^{\mathbb{C}}$ of functions from $\mathbb{C}$ to $\mathbb{C}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $\mathbb{C}$ being a set (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii)), and elements of classes are sets. Hence $\exp$ is the only set $E$ with $\varepsilon(E)$.

Real and imaginary parts as formulas. Let

$$\rho_{\cos}=\exists b\,\exists q\,\exists r\,\exists s\,\bigl((a,q)\in\iota\wedge(b,r)\in\iota\wedge((r,\jmath),s)\in{\odot}\wedge((q,s),w)\in{\oplus}\bigr),$$ $$\rho_{\sin}=\exists b\,\exists q\,\exists r\,\exists s\,\bigl((b,q)\in\iota\wedge(a,r)\in\iota\wedge((r,\jmath),s)\in{\odot}\wedge((q,s),w)\in{\oplus}\bigr).$$

Assign to $a$ a real number and to $w$ a complex number. By Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), the conjuncts of $\rho_{\cos}$ hold exactly when the corresponding memberships of ordered pairs hold, and by (a), from Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii), and (b) these say that $b\in\mathbb{R}$, $q=\iota(a)$, $r=\iota(b)$, $s=\iota(b)\,\jmath$ and $w=\iota(a)+\iota(b)\,\jmath$; for every $b\in\mathbb{R}$ such $q$, $r$ and $s$ exist and are sets, as elements of $\mathbb{C}$. So $\rho_{\cos}$ holds if and only if $w=\iota(a)+\iota(b)\,\jmath$ for some $b\in\mathbb{R}$, that is, $\operatorname{Re}w=a$, by the paragraph on the defining identities. In the same way, $\rho_{\sin}$ holds if and only if $w=\iota(b)+\iota(a)\,\jmath$ for some $b\in\mathbb{R}$, that is, $\operatorname{Im}w=a$.

The cosine and the sine. Let $\mu(F,\mathbb{R},\mathbb{R})$ be the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), with bound variables distinct from those above, which holds exactly when $F$ is a map $F:\mathbb{R}\to\mathbb{R}$. Let

$$\chi=(t,a)\in F\wedge(t,p)\in\iota\wedge((\jmath,p),v)\in{\odot}\wedge(v,w)\in E,$$ $$\varphi_{\cos}=\mu(F,\mathbb{R},\mathbb{R})\wedge\exists E\,\bigl(\varepsilon(E)\wedge\forall t\,\forall a\,\forall p\,\forall v\,\forall w\,(\chi\Rightarrow\rho_{\cos})\bigr),$$

and let $\varphi_{\sin}$ be the same formula with $\rho_{\sin}$ in place of $\rho_{\cos}$. Assign to $F$ a map $\mathbb{R}\to\mathbb{R}$. As $\exp$ is the only set with $\varepsilon$, the existential conjunct of $\varphi_{\cos}$ holds if and only if its universal formula holds with $E$ assigned $\exp$. Then, by (a) and (b), $\chi$ says that $t\in\mathbb{R}$, $a=F(t)$, $p=\iota(t)$, $v=\jmath\,\iota(t)$ and $w=\exp(\jmath\,\iota(t))$; these exist for every $t\in\mathbb{R}$ and are sets, $F(t)$ as an element of $\mathbb{R}$ and the others as elements of $\mathbb{C}$. Since $F(t)$ is real and $\exp(\jmath\,\iota(t))$ is complex, the previous paragraph shows that $\varphi_{\cos}$ holds if and only if $F$ is a map $\mathbb{R}\to\mathbb{R}$ with

$$F(t)=\operatorname{Re}\exp\bigl(\jmath\,\iota(t)\bigr)\qquad\text{for every }t\in\mathbb{R}.$$

As $\cos$ is such a map, this holds if and only if $F=\cos$, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii). In the same way, $\varphi_{\sin}$ holds if and only if $F$ is a map $\mathbb{R}\to\mathbb{R}$ with $F(t)=\operatorname{Im}\exp(\jmath\,\iota(t))$ for every $t\in\mathbb{R}$, that is, $F=\sin$. Thus $\varphi_{\cos}$ and $\varphi_{\sin}$, whose only free variable other than parameters is $F$, that is $x_{0}$, are predicative formulas in $x_{0}$ in the sense of Renaming and Substituting Variables in Predicative Formulas, holding exactly when $x_{0}$ is the cosine function and the sine function, respectively.

Any position. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, the formulas $\varphi_{\cos}(x_{i})$ and $\varphi_{\sin}(x_{i})$ are predicative formulas in $x_{0},\dots,x_{n-1}$ that hold, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{i}$ is the cosine function and the sine function, respectively. This proves (i) and (ii).

The classes. The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi_{\cos}$ with $x_{0}$ as its single variable and the parameters of the statement as its parameters, gives a class $C$ whose set elements are exactly the sets that are the cosine function (the one-entry tuple $\langle a\rangle$ is $a$, The Ordered Pair of Two Sets and Nested Tuples (ii)). It serves as the $C$ of (iii), since every element of a class is a set (Classes, Membership, Sets and Proper Classes (i)), and so is $\cos$: as a map $\mathbb{R}\to\mathbb{R}$ it lies in the class $\mathbb{R}^{\mathbb{R}}$ of functions from $\mathbb{R}$ to $\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $\mathbb{R}$ being a set, as noted at the start. In the same way, $\varphi_{\sin}$ gives a class $S$ as in (iv).