Proof of Kit for def:tangent

Facts about maps, predicative formulas and the arithmetic and order of $\mathbb{R}$ 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, $\cdot$ is the multiplication of $\mathbb{R}$, and $J=(-\pi/2,\pi/2)$ is the open interval. Throughout, the values of the parameters, and $J$, 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}$, the unit $1$ and the imaginary unit of $\mathbb{C}$, and $0,\pi\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), The Number Pi (i), Classes, Membership, Sets and Proper Classes (i)); the map $\mathbb{R}\to\mathbb{C}$, the addition of $\mathbb{N}_{0}$, the sum and product operations of $\mathbb{C}$, $+$, $\cdot$ 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)); $\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)); and $J$ as a subclass of $\mathbb{R}$ (Intervals of the Real Line (ii)), these by 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,C,S$ for the distinct set variables $x_{0},x_{1},x_{2}$ 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 a predicative formula in $F$ alone and move it to the position $i$ at the end. The letters $t,y,c,s,g,h,u,v$ denote further pairwise distinct set variables, distinct from $x_{0},x_{1},x_{2}$. The parameters are set variables other than $x_{0},\dots,x_{n-1}$, other than $x_{0},x_{1},x_{2}$, and other than these letters and all other bound variables used below.

The tangent. By The Tangent Function on $(-\pi/2,\pi/2)$ (i), $\tan$ is a map $J\to\mathbb{R}$ with $\tan t=\sin t/\cos t$ for every $t\in J$, where $\sin,\cos:\mathbb{R}\to\mathbb{R}$ are the sine and the cosine. For $t\in J$ we have $\cos t>0$ by The Cosine Is Positive on $(-\pi/2,\pi/2)$ (i), so $\cos t\neq0$, and hence, for every $y\in\mathbb{R}$,

$$y\cdot\cos t=\sin t\iff y=\frac{\sin t}{\cos t}=\tan t .$$

The function $\tan$ is a set: as a map $J\to\mathbb{R}$ it lies in the class $\mathbb{R}^{J}$ of functions from $J$ to $\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $J$ and $\mathbb{R}$ being sets, and elements of classes are sets.

Reading rules. (a) For a map $G:A\to\mathbb{R}$, with $A$ equal to $J$ or $\mathbb{R}$, and all sets $u$ and $v$: $(u,v)\in G$ if and only if $u\in A$ and $v=G(u)$, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii). (b) For $u,v\in\mathbb{R}$ and every set $g$: $((u,v),g)\in{+}$ if and only if $g=u+v$, and $((u,v),g)\in{\cdot}$ if and only if $g=u\cdot v$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi) for the binary operations of $\mathbb{R}$ (The Real Numbers (iii)); and for real $u$ and $v$, $(u,v)\in{<}$ says $u<v$ (Partial and Total Orders on a Set and the Associated Strict Relation (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 values of $0$ and $\pi$ are sets, as noted at the start. Each formula below is built from such formulas, from membership in the parameter $\mathbb{R}$ 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 cosine and the sine. Kit for def:sine-cosine-real (i) and Kit for def:sine-cosine-real (ii), for one variable and the position $0$, give predicative formulas in $x_{0}$ expressing that $x_{0}$ is the cosine function and that $x_{0}$ is the sine function; their parameters are among those of the statement. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$, $n=3$ and $\sigma(0)=1$, respectively $\sigma(0)=2$, they become predicative formulas $\gamma_{\cos}(C)$ and $\gamma_{\sin}(S)$ in $x_{0},x_{1},x_{2}$, with bound variables renamed to differ from the letters above, that hold exactly when $C$ is the cosine function and when $S$ is the sine function, respectively. The functions $\cos$ and $\sin$ are sets: as maps $\mathbb{R}\to\mathbb{R}$ they lie 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). Hence $\cos$ is the only set $C$ with $\gamma_{\cos}(C)$, and $\sin$ is the only set $S$ with $\gamma_{\sin}(S)$.

The interval. Let

$$\delta(t)=t\in\mathbb{R}\wedge\exists g\,\exists h\,\bigl(((t,t),g)\in{+}\wedge(g,\pi)\in{<}\wedge((g,\pi),h)\in{+}\wedge(0,h)\in{<}\bigr).$$

Assign a set to $t$; as $\delta(t)$ requires $t\in\mathbb{R}$, and $J\subseteq\mathbb{R}$, let $t\in\mathbb{R}$. By (b), the conjuncts inside the quantifiers say that $g=t+t$, $g<\pi$, $h=(t+t)+\pi$ and $0<h$; such $g$ and $h$ exist and are sets, as elements of $\mathbb{R}$. So $\delta(t)$ holds if and only if $t\in\mathbb{R}$, $t+t<\pi$ and $0<(t+t)+\pi$, that is, $-\pi<2t<\pi$, or equivalently $-\pi/2<t<\pi/2$. By Intervals of the Real Line (ii), for every set $t$, $\delta(t)$ holds if and only if $t\in J$.

Maps on the interval. Let $\Phi(F)$ 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 (vi), with bound variables distinct from those above, which holds exactly when $F$ is a function, and let

$$\mu_{J}(F)=\Phi(F)\wedge\forall u\,\bigl(\delta(u)\Leftrightarrow\exists v\,((u,v)\in F)\bigr)\wedge\forall u\,\forall v\,\bigl((u,v)\in F\Rightarrow v\in\mathbb{R}\bigr).$$

As $\delta(u)$ holds for a set $u$ exactly when $u\in J$, $\mu_{J}(F)$ holds if and only if the formula $\mu(F,A,B)$ 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) holds with $J$ and $\mathbb{R}$ assigned to $A$ and $B$, that is, if and only if $F$ is a map $F:J\to\mathbb{R}$.

The tangent as a formula. Let

$$\varphi=\mu_{J}(F)\wedge\exists C\,\exists S\,\Bigl(\gamma_{\cos}(C)\wedge\gamma_{\sin}(S)\wedge\forall t\,\forall y\,\forall c\,\forall s\,\bigl(((t,y)\in F\wedge(t,c)\in C\wedge(t,s)\in S)\Rightarrow((y,c),s)\in{\cdot}\bigr)\Bigr).$$

Assign to $F$ a map $J\to\mathbb{R}$. As $\cos$ and $\sin$ are the only sets with $\gamma_{\cos}$ and $\gamma_{\sin}$, the existential conjunct of $\varphi$ holds if and only if its universal formula holds with $C$ assigned $\cos$ and $S$ assigned $\sin$. Then, by (a), the premises of the implication say that $t\in J$, $y=F(t)$, $c=\cos t$ and $s=\sin t$, as $J\subseteq\mathbb{R}$; these exist for every $t\in J$ and are sets, as elements of $\mathbb{R}$. By (b) the conclusion then says $\sin t=F(t)\cdot\cos t$, as $F(t)$ and $\cos t$ are real numbers. So $\varphi$ holds if and only if $F$ is a map $J\to\mathbb{R}$ with

$$F(t)\cdot\cos t=\sin t\qquad\text{for every }t\in J,$$

that is, by the paragraph on the tangent, with $F(t)=\tan t$ for every $t\in J$. As $\tan$ is such a map, this holds if and only if $F=\tan$, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii). Thus $\varphi$, whose only free variable other than parameters is $F$, that is $x_{0}$, is a predicative formula in $x_{0}$ in the sense of Renaming and Substituting Variables in Predicative Formulas, and it holds exactly when $x_{0}$ is the tangent function.

Any position. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, the formula $\varphi(x_{i})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{i}$ is the tangent function. This proves (i).

The class. The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi$ with $x_{0}$ as its single variable and the parameters of the statement as its parameters, gives a class $T$ whose set elements are exactly the sets that are the tangent function (the one-entry tuple $\langle a\rangle$ is $a$, The Ordered Pair of Two Sets and Nested Tuples (ii)). It serves as the $T$ of (ii), since every element of a class is a set (Classes, Membership, Sets and Proper Classes (i)), and so is $\tan$, as shown in the paragraph on the tangent.