# The best possible constants approach for Wilker-Cusa-Huygens inequalities via stratification

Bojan Banjac, Branko Malešević, Miloš Mićović, Bojana Mihailović, Milica Savatović

► To cite this version:

Bojan Banjac, Branko Malešević, Miloš Mićović, Bojana Mihailović, Milica Savatović. The best possible constants approach for Wilker-Cusa-Huygens inequalities via stratification. Applicable Analysis and Discrete Mathematics, 2024, 18 (1), 10.2298/AADM240308012B. hal-04515800v2

HAL Id: hal-04515800

https://hal.science/hal-04515800v2

Submitted on 26 Apr 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# The best possible constants approach for Wilker-Cusa-Huygens inequalities via stratification

Bojan Banjac, Branko Malešević, Miloš Mićović, Bojana Mihailović, Milica Savatović

► To cite this version:

Bojan Banjac, Branko Malešević, Miloš Mićović, Bojana Mihailović, Milica Savatović. The best possible constants approach for Wilker-Cusa-Huygens inequalities via stratification. Applicable Analysis and Discrete Mathematics, 2024, 18 (1), 10.2298/AADM240308012B. hal-04515800v2

HAL Id: hal-04515800

https://hal.science/hal-04515800v2

Submitted on 26 Apr 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
THE BEST POSSIBLE CONSTANTS APPROACH
FOR WILKER-CUSA-HUYGENS INEQUALITIES
VIA STRATIFICATION

Bojan Banjac, Branko Malešević, Miloš Mićović*,
Bojana Mihailović and Milica Savatović

In this paper, we generalize Cristinel Mortici's results on Wilker-Cusa-Huygens inequalities using stratified families of functions and SimTheP – a system for automated proving of MTP inequalities.

# 1. INTRODUCTION

The basis of this research is well-known C. Mortici's paper [1] in which the
following theorems were proved:

**Theorem 1.** For every $x \in (0, \pi/2)$, we have:

$$-\frac{1}{15}x^4 < \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + \frac{23}{1890}x^6.$$

**Theorem 2.** For every $x \in (0, \pi/2)$, we have:

$$-\frac{1}{180}x^4 < \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + \frac{1}{3780}x^6.$$

**Theorem 3.** For every $x \in (0, \pi/2)$, we have:

$$3 + \left(\frac{3}{20}x^4 - \frac{3}{140}x^6\right) \frac{1}{\cos x} < 2\frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20 \cos x}x^4.$$

<footnote>*Corresponding author. Miloš Mićović</footnote>

<footnote n="2020">2020 Mathematics Subject Classification. 68V15, 41A44, 26D05.</footnote>

<footnote>Keywords and Phrases. Wilker-Cusa-Huygens inequalities, Stratified families of functions, A mini-max approximant, Automated proving of MTP inequalities, SimTheP.</footnote>
THE BEST POSSIBLE CONSTANTS APPROACH FOR WILKER-CUSA-HUYGENS INEQUALITIES VIA STRATIFICATION

Bojan Banjac, Branko Malešević, Miloš Mićović*,
Bojana Mihailović and Milica Savatović

In this paper, we generalize Cristinel Mortici's results on Wilker-Cusa-Huygens inequalities using stratified families of functions and SimTheP – a system for automated proving of MTP inequalities.

# 1. INTRODUCTION

The basis of this research is well-known C. Mortici's paper [1] in which the following theorems were proved:

**Theorem 1.** For every $x \in (0, \pi/2)$, we have:

$$-\frac{1}{15}x^4 < \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + \frac{23}{1890}x^6.$$

**Theorem 2.** For every $x \in (0, \pi/2)$, we have:

$$-\frac{1}{180}x^4 < \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + \frac{1}{3780}x^6.$$

**Theorem 3.** For every $x \in (0, \pi/2)$, we have:

$$3 + \left(\frac{3}{20}x^4 - \frac{3}{140}x^6\right) \frac{1}{\cos x} < 2\frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20 \cos x}x^4.$$

<footnote>*Corresponding author. Miloš Mićović</footnote>

<footnote n="2020">2020 Mathematics Subject Classification. 68V15, 41A44, 26D05.</footnote>

<footnote>Keywords and Phrases. Wilker-Cusa-Huygens inequalities, Stratified families of functions, A mini-max approximant, Automated proving of MTP inequalities, SimTheP.</footnote>
**Theorem 4.** For every $x \in (0, \pi/2)$, we have:

$$2 + \left( \frac{8}{45}x^4 - \frac{4}{105}x^6 \right) \frac{1}{\cos x} < \left( \frac{\sin x}{x} \right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45 \cos x} x^4.$$

**Theorem 5.** For every $x \in (0, \pi/2)$, we have:

$$\left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} > 2 + \frac{2}{45}x^4.$$

**Theorem 6.** For every $x \in (0, \pi/2)$, we have:

$$3\frac{x}{\sin x} + \cos x > 4 + \frac{1}{10}x^4 + \frac{1}{210}x^6.$$

Using a method based on the stratified families of functions described in the paper [2], we show that it is possible to enhance inequalities presented in Theorems 1-6 up to the level of the best possible constants. Also, we show that from some of the introduced families of functions, it is possible to single out corresponding minimax approximations.

In Section 2, preliminaries on stratified families of functions and a method for proving MTP inequalities are presented. This method for proving MTP inequalities forms the basis of SimTheP – automated theorem prover for MTP inequalities. The main results of the paper are provided in Section 3. Section 4 presents the conclusion. At the end of the paper, an Appendix is included, which contains proofs obtained using SimTheP.

## 2. PRELIMINARIES

In this section, we present assertions from the paper [2] and a method from the paper [3] on the basis of which our main results will be obtained.

### 2.1. STRATIFIED FAMILIES OF FUNCTIONS

Let

$$\varphi_p(x) : (a, b) \to \mathbb{R}$$

be a family of functions with a variable $x \in (a, b)$ and a parameter $p \in \mathbb{R}^+$.

A family of functions $\varphi_p(x)$ is *increasingly stratified* if

$$(\forall p_1, p_2 \in \mathbb{R}^+) \ p_1 < p_2 \iff \varphi_{p_1}(x) < \varphi_{p_2}(x)$$

holds for any $x \in (a, b)$ and, conversely, it is *decreasingly stratified* if

$$(\forall p_1, p_2 \in \mathbb{R}^+) \ p_1 < p_2 \iff \varphi_{p_1}(x) > \varphi_{p_2}(x)$$

holds for any $x \in (a, b)$.
**Theorem 4.** For every $x \in (0, \pi/2)$, we have:

$$2 + \left( \frac{8}{45}x^4 - \frac{4}{105}x^6 \right) \frac{1}{\cos x} < \left( \frac{\sin x}{x} \right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45 \cos x} x^4.$$

**Theorem 5.** For every $x \in (0, \pi/2)$, we have:

$$\left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} > 2 + \frac{2}{45}x^4.$$

**Theorem 6.** For every $x \in (0, \pi/2)$, we have:

$$3\frac{x}{\sin x} + \cos x > 4 + \frac{1}{10}x^4 + \frac{1}{210}x^6.$$

Using a method based on the stratified families of functions described in the paper [2], we show that it is possible to enhance inequalities presented in Theorems 1-6 up to the level of the best possible constants. Also, we show that from some of the introduced families of functions, it is possible to single out corresponding minimax approximations.

In Section 2, preliminaries on stratified families of functions and a method for proving MTP inequalities are presented. This method for proving MTP inequalities forms the basis of SimTheP – automated theorem prover for MTP inequalities. The main results of the paper are provided in Section 3. Section 4 presents the conclusion. At the end of the paper, an Appendix is included, which contains proofs obtained using SimTheP.

## 2. PRELIMINARIES

In this section, we present assertions from the paper [2] and a method from the paper [3] on the basis of which our main results will be obtained.

### 2.1. STRATIFIED FAMILIES OF FUNCTIONS

Let

$$\varphi_p(x) : (a, b) \to \mathbb{R}$$

be a family of functions with a variable $x \in (a, b)$ and a parameter $p \in \mathbb{R}^+$.

A family of functions $\varphi_p(x)$ is *increasingly stratified* if

$$(\forall p_1, p_2 \in \mathbb{R}^+) \ p_1 < p_2 \iff \varphi_{p_1}(x) < \varphi_{p_2}(x)$$

holds for any $x \in (a, b)$ and, conversely, it is *decreasingly stratified* if

$$(\forall p_1, p_2 \in \mathbb{R}^+) \ p_1 < p_2 \iff \varphi_{p_1}(x) > \varphi_{p_2}(x)$$

holds for any $x \in (a, b)$.
In this paper, we call $\sup_{x \in (a,b)} |\varphi_p(x)|$ an error and denote it by $d^{(p)}$.

In [2], the conditions for the existence of a unique value $p_0$ of the parameter $p \in \mathbb{R}^+$, for which an infimum of the error is attained, are considered. Such infimum is denoted by

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (a,b)} |\varphi_p(x)|.$$

For such a value $p_0$, the function $\varphi_{p_0}(x)$ is called the minimax approximant on $(a, b)$.

**Theorem 7.** (Theorem 1 [2]) Let $\varphi_p(x)$ be a family of functions that are continuous with respect to $x \in (a, b)$ for each $p \in \mathbb{R}^+$ and increasingly stratified for $p \in \mathbb{R}^+$, and let $c, d$ be in $\mathbb{R}^+$ such that $c < d$. If:

(a) $\varphi_c(x) < 0$ and $\varphi_d(x) > 0$ for all $x \in (a, b)$, and at the endpoints $\varphi_c(a+) = \varphi_c(b-) = \varphi_d(a+) = 0$ and $\varphi_d(b-) \in \mathbb{R}^+$ hold;

(b) the functions $\varphi_p(x)$ are continuous with respect to $p \in (c, d)$ for each $x \in (a, b)$ and $\varphi_p(b-)$ is continuous with respect to $p \in (c, d)$ too;

(c) for all $p \in (c, d)$, there exists a right neighbourhood of the point $a$ in which $\varphi_p(x) < 0$ holds;

(d) for all $p \in (c, d)$ the function $\varphi_p(x)$ has exactly one extremum $t^{(p)}$ on $(a, b)$, which is minimum;

then there exists exactly one solution $p_0$, for $p \in \mathbb{R}^+$, of the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p(b-)$$

and for $d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}(b-)$ we have

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (a,b)} |\varphi_p(x)|.$$

The analogous theorem can be stated for decreasingly stratified families of functions.

**Theorem 7'** (Theorem 1' [2]) Let $\varphi_p(x)$ be a family of functions that are continuous with respect to $x \in (a, b)$ for each $p \in \mathbb{R}^+$ and decreasingly stratified for $p \in \mathbb{R}^+$, and let $c, d$ be in $\mathbb{R}^+$ such that $c < d$. If:

(a) $\varphi_c(x) > 0$ and $\varphi_d(x) < 0$ for all $x \in (a, b)$, and at the endpoints $\varphi_c(a+) = \varphi_c(b-) = \varphi_d(a+) = 0$ and $\varphi_c(b-) \in \mathbb{R}^+$ hold;

(b) the functions $\varphi_p(x)$ are continuous with respect to $p \in (c, d)$ for each $x \in (a, b)$ and $\varphi_p(b-)$ is continuous with respect to $p \in (c, d)$ too;

(c) for all $p \in (c, d)$, there exists a right neighbourhood of the point $a$ in which $\varphi_p(x) < 0$ holds;
In this paper, we call $\sup_{x \in (a,b)} |\varphi_p(x)|$ an error and denote it by $d^{(p)}$.

In [2], the conditions for the existence of a unique value $p_0$ of the parameter $p \in \mathbb{R}^+$, for which an infimum of the error is attained, are considered. Such infimum is denoted by

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (a,b)} |\varphi_p(x)|.$$

For such a value $p_0$, the function $\varphi_{p_0}(x)$ is called the minimax approximant on $(a, b)$.

**Theorem 7.** (Theorem 1 [2]) Let $\varphi_p(x)$ be a family of functions that are continuous with respect to $x \in (a, b)$ for each $p \in \mathbb{R}^+$ and increasingly stratified for $p \in \mathbb{R}^+$, and let $c, d$ be in $\mathbb{R}^+$ such that $c < d$. If:

(a) $\varphi_c(x) < 0$ and $\varphi_d(x) > 0$ for all $x \in (a, b)$, and at the endpoints $\varphi_c(a+) = \varphi_c(b-) = \varphi_d(a+) = 0$ and $\varphi_d(b-) \in \mathbb{R}^+$ hold;

(b) the functions $\varphi_p(x)$ are continuous with respect to $p \in (c, d)$ for each $x \in (a, b)$ and $\varphi_p(b-)$ is continuous with respect to $p \in (c, d)$ too;

(c) for all $p \in (c, d)$, there exists a right neighbourhood of the point $a$ in which $\varphi_p(x) < 0$ holds;

(d) for all $p \in (c, d)$ the function $\varphi_p(x)$ has exactly one extremum $t^{(p)}$ on $(a, b)$, which is minimum;

then there exists exactly one solution $p_0$, for $p \in \mathbb{R}^+$, of the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p(b-)$$

and for $d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}(b-)$ we have

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (a,b)} |\varphi_p(x)|.$$

The analogous theorem can be stated for decreasingly stratified families of functions.

**Theorem 7'** (Theorem 1' [2]) Let $\varphi_p(x)$ be a family of functions that are continuous with respect to $x \in (a, b)$ for each $p \in \mathbb{R}^+$ and decreasingly stratified for $p \in \mathbb{R}^+$, and let $c, d$ be in $\mathbb{R}^+$ such that $c < d$. If:

(a) $\varphi_c(x) > 0$ and $\varphi_d(x) < 0$ for all $x \in (a, b)$, and at the endpoints $\varphi_c(a+) = \varphi_c(b-) = \varphi_d(a+) = 0$ and $\varphi_c(b-) \in \mathbb{R}^+$ hold;

(b) the functions $\varphi_p(x)$ are continuous with respect to $p \in (c, d)$ for each $x \in (a, b)$ and $\varphi_p(b-)$ is continuous with respect to $p \in (c, d)$ too;

(c) for all $p \in (c, d)$, there exists a right neighbourhood of the point $a$ in which $\varphi_p(x) < 0$ holds;
(d) for all $p \in (c, d)$ the function $\varphi_p(x)$ has exactly one extremum $t^{(p)}$ on $(a, b)$, which is minimum;

then there exists exactly one solution $p_0$, for $p \in \mathbb{R}^+$, of the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p(b^-)$$

and for $d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}(b^-)$ we have

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (a, b)} |\varphi_p(x)|.$$

**Theorem 8.** (Nike theorem, Theorem 3 [2], Theorem 2.1. [4]) Let $f: (0, c) \to \mathbb{R}$ be $m$ times differentiable function (for some $m \ge 2$, $m \in \mathbb{N}$) satisfying the following conditions:

(a) $f^{(m)}(x) > 0$ for $x \in (0, c)$;

(b) there is a right neighbourhood of zero in which the following inequalities are true:

$$f < 0, f' < 0, \dots, f^{(m-1)} < 0;$$

(c) there is a left neighbourhood of $c$ in which the following inequalities are true:

$$f > 0, f' > 0, \dots, f^{(m-1)} > 0.$$

Then the function $f$ has exactly one zero $x_0 \in (0, c)$, and $f(x) < 0$ for $x \in (0, x_0)$ and $f(x) > 0$ for $x \in (x_0, c)$. Also, the function $f$ has exactly one local minimum on the interval $(0, c)$. More precisely, there is exactly one point $t \in (0, c)$ (in fact $t \in (0, x_0)$) such that $f(t) < 0$ is the smallest value of the function $f$ on the interval $(0, c)$ and particularly on $(0, x_0)$.

In a case when it is not possible to apply the Nike theorem, the following theorem is applied, which gives sufficient conditions that the function on the interval has exactly one zero and exactly one minimum (see section 3).

**Theorem 9.** (The Second Nike theorem, Theorem 4 [2]) Let $f: (0, c) \to \mathbb{R}$ be $m$ times differentiable function (for some $m \ge 2$, $m \in \mathbb{N}$) satisfying the following conditions:

(a) $f^{(m)}$ has exactly one zero $x_m$ on $(0, c)$ such that $f^{(m)} > 0$ on $(0, x_m)$ and $f^{(m)} < 0$ on $(x_m, c)$;

(b) there is a right neighbourhood of zero in which the following inequalities are true:

$$f < 0, f' < 0, \dots, f^{(m-1)} < 0;$$

(c) there is a left neighbourhood of $c$ in which the following inequalities are true:

$$f > 0, f' > 0, \dots, f^{(m-1)} > 0.$$
(d) for all $p \in (c, d)$ the function $\varphi_p(x)$ has exactly one extremum $t^{(p)}$ on $(a, b)$, which is minimum;

then there exists exactly one solution $p_0$, for $p \in \mathbb{R}^+$, of the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p(b^-)$$

and for $d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}(b^-)$ we have

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (a, b)} |\varphi_p(x)|.$$

**Theorem 8.** (Nike theorem, Theorem 3 [2], Theorem 2.1. [4]) Let $f : (0, c) \to \mathbb{R}$ be $m$ times differentiable function (for some $m \ge 2$, $m \in \mathbb{N}$) satisfying the following conditions:

(a) $f^{(m)}(x) > 0$ for $x \in (0, c)$;

(b) there is a right neighbourhood of zero in which the following inequalities are true:

$$f < 0, f' < 0, \dots, f^{(m-1)} < 0;$$

(c) there is a left neighbourhood of $c$ in which the following inequalities are true:

$$f > 0, f' > 0, \dots, f^{(m-1)} > 0.$$

Then the function $f$ has exactly one zero $x_0 \in (0, c)$, and $f(x) < 0$ for $x \in (0, x_0)$ and $f(x) > 0$ for $x \in (x_0, c)$. Also, the function $f$ has exactly one local minimum on the interval $(0, c)$. More precisely, there is exactly one point $t \in (0, c)$ (in fact $t \in (0, x_0)$) such that $f(t) < 0$ is the smallest value of the function $f$ on the interval $(0, c)$ and particularly on $(0, x_0)$.

In a case when it is not possible to apply the Nike theorem, the following theorem is applied, which gives sufficient conditions that the function on the interval has exactly one zero and exactly one minimum (see section 3).

**Theorem 9.** (The Second Nike theorem, Theorem 4 [2]) Let $f : (0, c) \to \mathbb{R}$ be $m$ times differentiable function (for some $m \ge 2$, $m \in \mathbb{N}$) satisfying the following conditions:

(a) $f^{(m)}$ has exactly one zero $x_m$ on $(0, c)$ such that $f^{(m)} > 0$ on $(0, x_m)$ and $f^{(m)} < 0$ on $(x_m, c)$;

(b) there is a right neighbourhood of zero in which the following inequalities are true:

$$f < 0, f' < 0, \dots, f^{(m-1)} < 0;$$

(c) there is a left neighbourhood of $c$ in which the following inequalities are true:

$$f > 0, f' > 0, \dots, f^{(m-1)} > 0.$$
Then the function $f$ has exactly one zero $x_0 \in (0, c)$ and $f(x) < 0$ for $x \in (0, x_0)$ and $f(x) > 0$ for $x \in (x_0, c)$. The function $f$ has exactly one minimum on the interval $(0, c)$, i.e. there is exactly one point $t \in (0, c)$ (in fact $t \in (0, x_0)$) such that $f(t) < 0$ is the smallest value of the function $f$ on the interval $(0, c)$ and particularly on $(0, x_0)$.

**Remark 1.** Let us emphasize that the previous two forms of the Nike theorem ensure the existence of a minimax approximant. Also, these two theorems claim that the local minimum at $t$ is the only extremum of the function $f$ on $(0, c)$, which is shown in their proofs (see [2]).

The topic of stratification appears in the recently published papers [5]-[8].

## 2.2. A METHOD FOR PROVING MTP INEQUALITIES

MTP – Mixed Trigonometric Polynomial function is determined by:

$$f(x) = \sum_{i=1}^{n} \alpha_{i} x^{p_{i}} \cos^{q_{i}} x \sin^{r_{i}} x,$$

where $x \in \mathbb{S} \subseteq \mathbb{R}$ ($\mathbb{S}$ is an open or closed interval), $\alpha_i \in \mathbb{R} \setminus \{0\}$, $p_i, q_i, r_i \in \mathbb{N}_0$ and $n \in \mathbb{N}$. The corresponding inequality

$$f(x) > 0,$$

where $x \in \mathbb{S}$, is called an MTP inequality.

MTP functions were originally considered through MTP systems of such functions involving multiple variables, see [9]. In the article [3], the previous definitions of MTP function and MTP inequality were introduced. Moreover, in that article, a method for proving MTP inequalities on the base interval $(0, \pi/2)$ was presented. The method is based on Maclaurin approximations of the sine and cosine functions. Let us emphasize that in [10], a method for proving MTP inequalities on the base interval, based on the universal trigonometric substitution and Maclaurin approximations, was presented, see also [11]. It is noteworthy that both methods have been applied earlier in numerous papers and monographs, see, for example, [1], [12], [13]. The topic of MTP functions and stratified families of functions has been the subject of recently defended doctoral dissertations [14], [15], [16].

In further consideration, let $f(x)$ be an MTP function with rational coefficients. The method for proving MTP inequalities from the paper [3] has been computationally implemented through the doctoral dissertation [15]. For methods for proving inequalities by computer, see also the papers [17] and [18]. The computer implementation from [15], called SimTheP, proves MTP inequalities on the interval $\mathbb{S} \subseteq [0, \pi/2]$, providing users with the proof in four stages. Therefore, we will outline the method through a brief description of each of these stages based on the papers [3], [7], [19].
Then the function $f$ has exactly one zero $x_0 \in (0, c)$ and $f(x) < 0$ for $x \in (0, x_0)$ and $f(x) > 0$ for $x \in (x_0, c)$. The function $f$ has exactly one minimum on the interval $(0, c)$, i.e. there is exactly one point $t \in (0, c)$ (in fact $t \in (0, x_0)$) such that $f(t) < 0$ is the smallest value of the function $f$ on the interval $(0, c)$ and particularly on $(0, x_0)$.

**Remark 1.** Let us emphasize that the previous two forms of the Nike theorem ensure the existence of a minimax approximant. Also, these two theorems claim that the local minimum at $t$ is the only extremum of the function $f$ on $(0, c)$, which is shown in their proofs (see [2]).

The topic of stratification appears in the recently published papers [5]-[8].

## 2.2. A METHOD FOR PROVING MTP INEQUALITIES

MTP – Mixed Trigonometric Polynomial function is determined by:

$$f(x) = \sum_{i=1}^{n} \alpha_{i} x^{p_{i}} \cos^{q_{i}} x \sin^{r_{i}} x,$$

where $x \in \mathbb{S} \subseteq \mathbb{R}$ ($\mathbb{S}$ is an open or closed interval), $\alpha_i \in \mathbb{R} \setminus \{0\}$, $p_i, q_i, r_i \in \mathbb{N}_0$ and $n \in \mathbb{N}$. The corresponding inequality

$$f(x) > 0,$$

where $x \in \mathbb{S}$, is called an MTP inequality.

MTP functions were originally considered through MTP systems of such functions involving multiple variables, see [9]. In the article [3], the previous definitions of MTP function and MTP inequality were introduced. Moreover, in that article, a method for proving MTP inequalities on the base interval $(0, \pi/2)$ was presented. The method is based on Maclaurin approximations of the sine and cosine functions. Let us emphasize that in [10], a method for proving MTP inequalities on the base interval, based on the universal trigonometric substitution and Maclaurin approximations, was presented, see also [11]. It is noteworthy that both methods have been applied earlier in numerous papers and monographs, see, for example, [1], [12], [13]. The topic of MTP functions and stratified families of functions has been the subject of recently defended doctoral dissertations [14], [15], [16].

In further consideration, let $f(x)$ be an MTP function with rational coefficients. The method for proving MTP inequalities from the paper [3] has been computationally implemented through the doctoral dissertation [15]. For methods for proving inequalities by computer, see also the papers [17] and [18]. The computer implementation from [15], called SimTheP, proves MTP inequalities on the interval $\mathbb{S} \subseteq [0, \pi/2]$, providing users with the proof in four stages. Therefore, we will outline the method through a brief description of each of these stages based on the papers [3], [7], [19].
# I Recognition of possible case

In the first phase, the hypothesis $f(x) > 0$ on $\mathbb{S}$ is tested based on the values of the function at the boundary points of the interval.

# II Transformation of angles

In this phase, each addend of the MTP function $f(x)$ undergoes the substitution of the expression $\cos^n x \sin^m x$ ($n, m \in \mathbb{N}_0$) into a sum of sine and cosine functions of multiple angles according to Table 1. These substitutions were proven in the paper [3].

<table><caption>Table 1: Substitutions of terms $x^{p_i} \cos^{q_i} x \sin^{r_i} x$, see Table 1 from [19]</caption><thead><tr><th colspan="2">cos<sup>n</sup>x sin<sup>m</sup>x</th><th>Substitution</th></tr><tr><th>n = q<sub>i</sub></th><th>m = r<sub>i</sub></th><th></th></tr></thead><tbody><tr><td>even</td><td>even</td><td><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">&sum;<sub>k=0</sub><sup>n/2+m/2-1</sup></td></tr><tr><td style="padding: 0 0.2em;">&sum;<sub>j=0</sub><sup>k</sup></td></tr></tbody></table> <table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">(-1)<sup>m/2+k+j</sup> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">n</td></tr><tr><td style="padding: 0 0.2em;">j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">m</td></tr><tr><td style="padding: 0 0.2em;">k-j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> cos((n+m-2k)x)</td></tr><tr><td>odd</td><td>even</td><td><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">&sum;<sub>k=0</sub><sup>n/2+m/2-1/2</sup></td></tr><tr><td style="padding: 0 0.2em;">&sum;<sub>j=0</sub><sup>k</sup></td></tr></tbody></table> <table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">(-1)<sup>m/2+k+j</sup> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">n</td></tr><tr><td style="padding: 0 0.2em;">j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">m</td></tr><tr><td style="padding: 0 0.2em;">k-j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> cos((n+m-2k)x)</td></tr><tr><td>even</td><td>odd</td><td><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">&sum;<sub>k=0</sub><sup>n/2+m/2-1/2</sup></td></tr><tr><td style="padding: 0 0.2em;">&sum;<sub>j=0</sub><sup>k</sup></td></tr></tbody></table> <table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">(-1)<sup>m/2+k+j-1/2</sup> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">n</td></tr><tr><td style="padding: 0 0.2em;">j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">m</td></tr><tr><td style="padding: 0 0.2em;">k-j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> sin((n+m-2k)x)</td></tr><tr><td>odd</td><td>odd</td><td><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">&sum;<sub>k=0</sub><sup>n/2+m/2-1</sup></td></tr><tr><td style="padding: 0 0.2em;">&sum;<sub>j=0</sub><sup>k</sup></td></tr></tbody></table> <table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">(-1)<sup>m/2+k+j-1/2</sup> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">n</td></tr><tr><td style="padding: 0 0.2em;">j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> <span style="font-size: 2.5em; vertical-align: middle;">(</span><table style="display: inline-block; vertical-align: middle; border: 0; text-align: center;"><tbody><tr><td style="border-bottom: 1px solid black; padding: 0 0.2em;">m</td></tr><tr><td style="padding: 0 0.2em;">k-j</td></tr></tbody></table><span style="font-size: 2.5em; vertical-align: middle;">)</span> sin((n+m-2k)x)</td></tr></tbody></table></td></tr></tbody></table>

The initial MTP function is transformed into the equivalent form:

$$ (1) \qquad f(x) = \sum_{i=1}^{n} \alpha_i x^{p_i} \left( \sum_{k=0}^{m_i} \theta_k \operatorname{trig}_k^{(q_i, r_i)} \left( \underbrace{(q_i - r_i - 2k)}_{(=t)} x \right) \right), $$

where

$$ \operatorname{trig}_k^{(q_i, r_i)} = \begin{cases} \cos : q_i\text{-odd}, r_i\text{-even} \text{ or } q_i\text{-even}, r_i\text{-even} \\ \sin : q_i\text{-odd}, r_i\text{-odd} \text{ or } q_i\text{-even}, r_i\text{-odd} \end{cases} $$

and

$$ m_i = m_i(q_i, r_i) = \left\lfloor \frac{q_i + r_i}{2} \right\rfloor - 1. $$
## I Recognition of possible case

In the first phase, the hypothesis $f(x) > 0$ on $\mathbb{S}$ is tested based on the values of the function at the boundary points of the interval.

## II Transformation of angles

In this phase, each addend of the MTP function $f(x)$ undergoes the substitution of the expression $\cos^n x \sin^m x$ ($n, m \in \mathbb{N}_0$) into a sum of sine and cosine functions of multiple angles according to Table 1. These substitutions were proven in the paper [3].

<table><caption>Table 1: Substitutions of terms $x^{p_i} \cos^{q_i} x \sin^{r_i} x$, see Table 1 from [19]</caption><thead><tr><th colspan="2">cos<sup>n</sup>x sin<sup>m</sup>x</th><th>Substitution</th></tr><tr><th>n = q<sub>i</sub></th><th>m = r<sub>i</sub></th><th></th></tr></thead><tbody><tr><td>even</td><td>even</td><td><table style="display: inline-table; vertical-align: middle; border-collapse: collapse; margin-left: 5px; text-align: center;"><tbody><tr><td style="border: none; padding: 0 5px; border-bottom: 1px solid black;">&sum;<sub>k=0</sub><sup>n/2 + m/2 - 1</sup> &sum;<sub>j=0</sub><sup>k</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m/2 + k + j</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div><div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-top: 1px solid black; padding: 0 5px;">2<sup>n+m-1</sup></div></td></tr><tr><td></td><td></td><td style="border-top: 1px solid black; padding: 0 5px;">+ &sum;<sub>j=0</sub><sup>n/2 + m/2 - 1</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m + n/2 + j</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m/2 + m/2 - j</span><span style="font-size: 0.8em;">)</span></div></td></tr><tr><td>odd</td><td>even</td><td><table style="display: inline-table; vertical-align: middle; border-collapse: collapse; margin-left: 5px; text-align: center;"><tbody><tr><td style="border: none; padding: 0 5px; border-bottom: 1px solid black;">&sum;<sub>k=0</sub><sup>n/2 + m/2 - 1</sup> &sum;<sub>j=0</sub><sup>k</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m/2 + k + j</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div><div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-top: 1px solid black; padding: 0 5px;">2<sup>n+m-1</sup></div></td></tr><tr><td></td><td></td><td style="border-top: 1px solid black; padding: 0 5px;">+ &sum;<sub>j=0</sub><sup>n/2 + m/2 - 1</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m + n/2 + j - 1/2</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div></td></tr><tr><td>even</td><td>odd</td><td><table style="display: inline-table; vertical-align: middle; border-collapse: collapse; margin-left: 5px; text-align: center;"><tbody><tr><td style="border: none; padding: 0 5px; border-bottom: 1px solid black;">&sum;<sub>k=0</sub><sup>n/2 + m/2 - 1</sup> &sum;<sub>j=0</sub><sup>k</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m/2 + k + j - 1/2</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div><div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-top: 1px solid black; padding: 0 5px;">2<sup>n+m-1</sup></div></td></tr><tr><td></td><td></td><td style="border-top: 1px solid black; padding: 0 5px;">+ &sum;<sub>j=0</sub><sup>n/2 + m/2 - 1</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m + n/2 + k + j - 1/2</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div></td></tr><tr><td>odd</td><td>odd</td><td><table style="display: inline-table; vertical-align: middle; border-collapse: collapse; margin-left: 5px; text-align: center;"><tbody><tr><td style="border: none; padding: 0 5px; border-bottom: 1px solid black;">&sum;<sub>k=0</sub><sup>n/2 + m/2 - 1</sup> &sum;<sub>j=0</sub><sup>k</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m/2 + k + j - 1/2</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div><div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-top: 1px solid black; padding: 0 5px;">2<sup>n+m-1</sup></div></td></tr><tr><td></td><td></td><td style="border-top: 1px solid black; padding: 0 5px;">+ &sum;<sub>j=0</sub><sup>n/2 + m/2 - 1</sup> <div style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;"><div style="border-bottom: 1px solid black; padding: 0 5px;">(-1)<sup>m + n/2 + k + j - 1/2</sup> <span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">n</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">j</span><span style="font-size: 0.8em;">)</span><span style="font-size: 0.8em;">(</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">m</span><span style="display: inline-block; vertical-align: middle; text-align: center; line-height: 1.2em;">k-j</span><span style="font-size: 0.8em;">)</span></div></td></tr></tbody></table></td></tr></tbody></table>

The initial MTP function is transformed into the equivalent form:

$$ (1) \qquad f(x) = \sum_{i=1}^{n} \alpha_i x^{p_i} \left( \sum_{k=0}^{m_i} \theta_k \operatorname{trig}_k^{(q_i, r_i)} \left( \underbrace{(q_i - r_i - 2k)}_{(=t)} x \right) \right), $$

where

$$ \operatorname{trig}_k^{(q_i, r_i)} = \begin{cases} \cos : q_i\text{-odd}, r_i\text{-even} \text{ or } q_i\text{-even}, r_i\text{-even} \\ \sin : q_i\text{-odd}, r_i\text{-odd} \text{ or } q_i\text{-even}, r_i\text{-odd} \end{cases} $$

and

$$ m_i = m_i(q_i, r_i) = \left\lfloor \frac{q_i + r_i}{2} \right\rfloor - 1. $$
### III Determination of downward rational polynomial approximation

During this phase, it is necessary to determine a downward polynomial approximation with rational coefficients of the MTP function (1).

Let us specify the general concept of downward/upward polynomial approximation of a function. Let $\phi(x) : A \to \mathbb{R}$ be any function defined over $A \subseteq \mathbb{R}$. The downward polynomial approximation of the function $\phi(x)$ over $B \subseteq A$ is a polynomial $P(x)$ such that

$$ (\forall x \in \mathbb{B}) \phi(x) \geq P(x), $$

denoted by $\underline{P}(x)$. Similarly, the upward polynomial approximation of the function $\phi(x)$ over $\mathbb{B} \subseteq A$ is a polynomial $P(x)$ such that

$$ (\forall x \in \mathbb{B}) \phi(x) \leq P(x), $$

denoted by $\overline{P}(x)$.

In the following Lemma from the paper [7], we provide some upward and downward polynomial approximations of the sine and cosine functions. These assumptions were proven in the paper [3].

**Lemma 1.** (Lemma 1 [7]) It holds:

(a) For the polynomial

$$ T_n(t) = \sum_{i=0}^{(n-1)/2} \frac{(-1)^i t^{2i+1}}{(2i+1)!}, $$

where $n = 4k + 1, k \in \mathbb{N}_0$, it holds:

$$ (\forall t \in [0, \sqrt{(n+3)(n+4)}]) \bar{T}_n(t) \geq \bar{T}_{n+4}(t) \geq \sin t, $$

$$ (\forall t \in [-\sqrt{(n+3)(n+4)}, 0]) \underline{T}_n(t) \leq \underline{T}_{n+4}(t) \leq \sin t. $$

For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equalities $\bar{T}_n(t) = \bar{T}_{n+4}(t)$ and $\underline{T}_n(t) = \underline{T}_{n+4}(t)$ hold, respectively.

(b) For the polynomial

$$ T_n(t) = \sum_{i=0}^{(n-1)/2} \frac{(-1)^i t^{2i+1}}{(2i+1)!}, $$

where $n = 4k + 3, k \in \mathbb{N}_0$, it holds:

$$ (\forall t \in [0, \sqrt{(n+3)(n+4)}]) \underline{T}_n(t) \leq \underline{T}_{n+4}(t) \leq \sin t, $$

$$ (\forall t \in [-\sqrt{(n+3)(n+4)}, 0]) \bar{T}_n(t) \geq \bar{T}_{n+4}(t) \geq \sin t. $$
### III Determination of downward rational polynomial approximation

During this phase, it is necessary to determine a downward polynomial approximation with rational coefficients of the MTP function (1).

Let us specify the general concept of downward/upward polynomial approximation of a function. Let $\phi(x) : A \to \mathbb{R}$ be any function defined over $A \subseteq \mathbb{R}$. The downward polynomial approximation of the function $\phi(x)$ over $B \subseteq A$ is a polynomial $P(x)$ such that

$$ (\forall x \in \mathbb{B}) \phi(x) \geq P(x), $$

denoted by $\underline{P}(x)$. Similarly, the upward polynomial approximation of the function $\phi(x)$ over $\mathbb{B} \subseteq A$ is a polynomial $P(x)$ such that

$$ (\forall x \in \mathbb{B}) \phi(x) \leq P(x), $$

denoted by $\overline{P}(x)$.

In the following Lemma from the paper [7], we provide some upward and downward polynomial approximations of the sine and cosine functions. These assumptions were proven in the paper [3].

**Lemma 1.** (Lemma 1 [7]) It holds:

(a) For the polynomial

$$ T_n(t) = \sum_{i=0}^{(n-1)/2} \frac{(-1)^i t^{2i+1}}{(2i+1)!}, $$

where $n = 4k + 1, k \in \mathbb{N}_0$, it holds:

$$ (\forall t \in [0, \sqrt{(n+3)(n+4)}]) \bar{T}_n(t) \geq \bar{T}_{n+4}(t) \geq \sin t, $$

$$ (\forall t \in [-\sqrt{(n+3)(n+4)}, 0]) \underline{T}_n(t) \leq \underline{T}_{n+4}(t) \leq \sin t. $$

For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equalities $\bar{T}_n(t) = \bar{T}_{n+4}(t)$ and $\underline{T}_n(t) = \underline{T}_{n+4}(t)$ hold, respectively.

(b) For the polynomial

$$ T_n(t) = \sum_{i=0}^{(n-1)/2} \frac{(-1)^i t^{2i+1}}{(2i+1)!}, $$

where $n = 4k + 3, k \in \mathbb{N}_0$, it holds:

$$ (\forall t \in [0, \sqrt{(n+3)(n+4)}]) \underline{T}_n(t) \leq \underline{T}_{n+4}(t) \leq \sin t, $$

$$ (\forall t \in [-\sqrt{(n+3)(n+4)}, 0]) \bar{T}_n(t) \geq \bar{T}_{n+4}(t) \geq \sin t. $$
For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equalities $\underline{T}_n(t) = \overline{T}_{n+4}(t)$ and $\overline{T}_n(t) = \underline{T}_{n+4}(t)$ hold, respectively.

(c) For the polynomial

$$T_n(t) = \sum_{i=0}^{n/2} \frac{(-1)^i t^{2i}}{(2i)!},$$

where $n = 4k, k \in \mathbb{N}_0$, it holds:

$$(\forall t \in [-\sqrt{(n+3)(n+4)}, \sqrt{(n+3)(n+4)}]) \underline{T}_n(t) \ge \overline{T}_{n+4}(t) \ge \cos t.$$

For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equality $\underline{T}_n(t) = \overline{T}_{n+4}(t)$ holds.

(d) For the polynomial

$$T_n(t) = \sum_{i=0}^{n/2} \frac{(-1)^i t^{2i}}{(2i)!},$$

where $n = 4k + 2, k \in \mathbb{N}_0$, it holds:

$$(\forall t \in [-\sqrt{(n+3)(n+4)}, \sqrt{(n+3)(n+4)}]) \underline{T}_n(t) \le \overline{T}_{n+4}(t) \le \cos t.$$

For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equality $\underline{T}_n(t) = \overline{T}_{n+4}(t)$ holds.

Let $T_n^{\phi,a}(x)$ denote the Taylor expansion of order $n$ of some analytic function $\phi$ in the neighbourhood of some point $a$.

With the aim of obtaining a downward polynomial approximation $P(x)$ of the MTP function $f(x)$, we approximate each addend of the function (1) by a Maclaurin polynomial using the following estimates:

$$ (*) \qquad \left\{ \begin{array}{ll} \alpha_i \theta_k > 0 : & \mathbf{cos} t > T_{4\ell_1+2}^{\cos,0}(x), \\ \alpha_i \theta_k < 0 : & \mathbf{cos} t < T_{4\ell_2}^{\cos,0}(x), \\ \alpha_i \theta_k > 0 : & \mathbf{sin} t > T_{4\ell_3+3}^{\sin,0}(x), \\ \alpha_i \theta_k < 0 : & \mathbf{sin} t < T_{4\ell_4+1}^{\sin,0}(x); \end{array} \right. $$

where $t = (q_i - r_i - 2k)x$ and $\ell_{1,2,3,4} \in \mathbb{N}_0$.

By applying $(*)$, we determine a polynomial $P(x)$ such that

$$f(x) > P(x)$$

for $x \in \mathbb{S}$. If there exists a polynomial $P(x)$ with rational coefficients such that

$$P(x) > 0$$

for $x \in \mathbb{S}$, then

$$f(x) > 0$$

for $x \in \mathbb{S}$.
For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equalities $\underline{T}_n(t) = \overline{T}_{n+4}(t)$ and $\overline{T}_n(t) = \underline{T}_{n+4}(t)$ hold, respectively.

(c) For the polynomial

$$T_n(t) = \sum_{i=0}^{n/2} \frac{(-1)^i t^{2i}}{(2i)!},$$

where $n = 4k, k \in \mathbb{N}_0$, it holds:

$$(\forall t \in [-\sqrt{(n+3)(n+4)}, \sqrt{(n+3)(n+4)}]) \underline{T}_n(t) \ge \overline{T}_{n+4}(t) \ge \cos t.$$

For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equality $\underline{T}_n(t) = \overline{T}_{n+4}(t)$ holds.

(d) For the polynomial

$$T_n(t) = \sum_{i=0}^{n/2} \frac{(-1)^i t^{2i}}{(2i)!},$$

where $n = 4k + 2, k \in \mathbb{N}_0$, it holds:

$$(\forall t \in [-\sqrt{(n+3)(n+4)}, \sqrt{(n+3)(n+4)}]) \underline{T}_n(t) \le \overline{T}_{n+4}(t) \le \cos t.$$

For $t = 0$, the inequalities turn into equalities. For $t = \pm\sqrt{(n+3)(n+4)}$, the equality $\underline{T}_n(t) = \overline{T}_{n+4}(t)$ holds.

Let $T_n^{\phi,a}(x)$ denote the Taylor expansion of order $n$ of some analytic function $\phi$ in the neighbourhood of some point $a$.

With the aim of obtaining a downward polynomial approximation $P(x)$ of the MTP function $f(x)$, we approximate each addend of the function (1) by a Maclaurin polynomial using the following estimates:

$$ (*) \qquad \left\{ \begin{array}{ll} \alpha_i \theta_k > 0 : & \mathbf{cos} t > T_{4\ell_1+2}^{\cos,0}(x), \\ \alpha_i \theta_k < 0 : & \mathbf{cos} t < T_{4\ell_2}^{\cos,0}(x), \\ \alpha_i \theta_k > 0 : & \mathbf{sin} t > T_{4\ell_3+3}^{\sin,0}(x), \\ \alpha_i \theta_k < 0 : & \mathbf{sin} t < T_{4\ell_4+1}^{\sin,0}(x); \end{array} \right. $$

where $t = (q_i - r_i - 2k)x$ and $\ell_{1,2,3,4} \in \mathbb{N}_0$.

By applying $(*)$, we determine a polynomial $P(x)$ such that

$$f(x) > P(x)$$

for $x \in \mathbb{S}$. If there exists a polynomial $P(x)$ with rational coefficients such that

$$P(x) > 0$$

for $x \in \mathbb{S}$, then

$$f(x) > 0$$

for $x \in \mathbb{S}$.
If the coefficients of the MTP function $f(x)$ are not rational numbers but computable real numbers, then we could determine a downward polynomial approximation with rational numbers, see the paper [20].

## IV The final part

For real polynomials defined over a segment with endpoints where the polynomial does not have zero, Sturm's theorem provides the number of roots on such a segment, see, for example, Theorem 4.1 [21] or originally [22]. It is particularly noteworthy that for polynomial functions with rational coefficients defined over a segment with rational endpoints, according to Theorem 4.2 [21], the problem of determining the number of roots over that segment is an algorithmically decidable problem. For such polynomial functions, if we obtain a proof of positivity using Sturm's theorem, we can consider it as an effective proof by finite procedures that can be manually verified.

In the third part, $P(x)$ is determined as a polynomial with rational coefficients. If $\mathbb{S}$ is not a segment with rational endpoints or the polynomial $P(x)$ has a root at the boundary points of the segment $\mathbb{S}$, we consider the polynomial over an extended segment with rational endpoints, see [23]. It is always possible to choose such a segment with rational endpoints that the polynomial $P(x)$ does not have a root at the boundary points of that segment. If the number of roots does not increase over such an extended segment, and we know whether the polynomial has a root at the boundary points of the segment $\mathbb{S}$, then we also have an effective proof of the polynomial inequality $P(x) > 0$ over $\mathbb{S}$ by applying Sturm's theorem.

Let us emphasize that proofs based on the Sturm algorithm are absolutely theoretically rigorous, as pointed out in the paper [24], see also [25]-[27].

In Appendix sections A1 and A4 - A7, we prove MTP inequalities $f(x) > 0$ over the base interval $(0, \pi/2)$, while in section A2, we prove MTP inequality over the interval $(0, 1]$ and in A3 over the interval $[1, \pi/2]$.

## 3. MAIN RESULTS

According to the paper [2], the following statements, which are improvements of Theorems 1–6 from the paper [1], are proved. Note that the automatic prover SimTheP was utilized for proving the MTP inequalities. The results obtained by this prover are provided in the Appendix.

### Improvement of Theorem 1

**Lemma 2.** *The family of functions*

$$ \varphi_p(x) = -\cos x + \left(\frac{\sin x}{x}\right)^3 - \frac{1}{15}x^4 + p x^6 \quad (\text{for } x \in (0, \frac{\pi}{2})) $$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.
If the coefficients of the MTP function $f(x)$ are not rational numbers but computable real numbers, then we could determine a downward polynomial approximation with rational numbers, see the paper [20].

## IV The final part

For real polynomials defined over a segment with endpoints where the polynomial does not have zero, Sturm's theorem provides the number of roots on such a segment, see, for example, Theorem 4.1 [21] or originally [22]. It is particularly noteworthy that for polynomial functions with rational coefficients defined over a segment with rational endpoints, according to Theorem 4.2 [21], the problem of determining the number of roots over that segment is an algorithmically decidable problem. For such polynomial functions, if we obtain a proof of positivity using Sturm's theorem, we can consider it as an effective proof by finite procedures that can be manually verified.

In the third part, $P(x)$ is determined as a polynomial with rational coefficients. If $\mathbb{S}$ is not a segment with rational endpoints or the polynomial $P(x)$ has a root at the boundary points of the segment $\mathbb{S}$, we consider the polynomial over an extended segment with rational endpoints, see [23]. It is always possible to choose such a segment with rational endpoints that the polynomial $P(x)$ does not have a root at the boundary points of that segment. If the number of roots does not increase over such an extended segment, and we know whether the polynomial has a root at the boundary points of the segment $\mathbb{S}$, then we also have an effective proof of the polynomial inequality $P(x) > 0$ over $\mathbb{S}$ by applying Sturm's theorem.

Let us emphasize that proofs based on the Sturm algorithm are absolutely theoretically rigorous, as pointed out in the paper [24], see also [25]-[27].

In Appendix sections A1 and A4 - A7, we prove MTP inequalities $f(x) > 0$ over the base interval $(0, \pi/2)$, while in section A2, we prove MTP inequality over the interval $(0, 1]$ and in A3 over the interval $[1, \pi/2]$.

## 3. MAIN RESULTS

According to the paper [2], the following statements, which are improvements of Theorems 1-6 from the paper [1], are proved. Note that the automatic prover SimTheP was utilized for proving the MTP inequalities. The results obtained by this prover are provided in the Appendix.

### Improvement of Theorem 1

**Lemma 2.** *The family of functions*

$$ \varphi_p(x) = -\cos x + \left(\frac{\sin x}{x}\right)^3 - \frac{1}{15}x^4 + px^6 \quad (\text{for } x \in (0, \frac{\pi}{2})) $$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.
Let us introduce the function $g(x)$ so that the equivalence

$$ \varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+ $$

holds. Then

$$ g(x) = \frac{x^7 + 15x^3 \cos x - 15 \sin^3 x}{15x^9}, \quad x \in (0, \frac{\pi}{2}). $$

Note that

$$ \varphi_p(x) = (p - g(x))x^6. $$

**Lemma 3.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$ g'(x) = \frac{45x \cos^3 x - 135 \cos^2 x \sin x - (90x^3 + 45x) \cos x - 15x^4 \sin x + 135 \sin x - 2x^7}{15x^{10}}. $$

It holds

$$ g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}), $$

where

$$ f(x) = 2x^7 - 45x \cos^3 x + 135 \cos^2 x \sin x + (90x^3 + 45x) \cos x + 15x^4 \sin x - 135 \sin x. $$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A1**. □

**Statement 1.** Let

$$ A = \frac{4\pi^7 - 7680}{15\pi^9} = 0.0098430\dots \quad \text{and} \quad B = \frac{23}{1890} = 0.012169\dots. $$

Then, it holds:

(i) If $p \in (0, A]$, then

$$ x \in (0, \frac{\pi}{2}) \implies -\frac{1}{15}x^4 + px^6 \le -\frac{1}{15}x^4 + Ax^6 < \cos x - \left(\frac{\sin x}{x}\right)^3. $$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$ x \in (0, x_0^{(p)}) \implies -\frac{1}{15}x^4 + px^6 < \cos x - \left(\frac{\sin x}{x}\right)^3 $$

and
Let us introduce the function $g(x)$ so that the equivalence

$$ \varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+ $$

holds. Then

$$ g(x) = \frac{x^7 + 15x^3 \cos x - 15 \sin^3 x}{15x^9}, \quad x \in (0, \frac{\pi}{2}). $$

Note that

$$ \varphi_p(x) = (p - g(x))x^6. $$

**Lemma 3.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$ g'(x) = \frac{45x \cos^3 x - 135 \cos^2 x \sin x - (90x^3 + 45x) \cos x - 15x^4 \sin x + 135 \sin x - 2x^7}{15x^{10}} $$

It holds

$$ g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}), $$

where

$$ f(x) = 2x^7 - 45x \cos^3 x + 135 \cos^2 x \sin x + (90x^3 + 45x) \cos x + 15x^4 \sin x - 135 \sin x. $$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A1**. □

**Statement 1.** Let

$$ A = \frac{4\pi^7 - 7680}{15\pi^9} = 0.0098430\dots \quad \text{and} \quad B = \frac{23}{1890} = 0.012169\dots. $$

Then, it holds:

(i) If $p \in (0, A]$, then

$$ x \in (0, \frac{\pi}{2}) \implies -\frac{1}{15}x^4 + px^6 \le -\frac{1}{15}x^4 + Ax^6 < \cos x - \left(\frac{\sin x}{x}\right)^3. $$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$ x \in (0, x_0^{(p)}) \implies -\frac{1}{15}x^4 + px^6 < \cos x - \left(\frac{\sin x}{x}\right)^3 $$

and
$$x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \implies \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + px^6$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in \left(0, \frac{\pi}{2}\right) \implies \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + Bx^6 \leq -\frac{1}{15}x^4 + px^6.$$

(iv) There is exactly one solution to the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p\left(\frac{\pi}{2}\right),$$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$p_0 = 0.010004...$$

For the value

$$d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}\left(\frac{\pi}{2}\right) = 0.0024209...,$$

the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.010004...$, the minimax approximant of the family is determined as

$$\varphi_{p_0}(x) = -\cos x + \left(\frac{\sin x}{x}\right)^3 - \frac{1}{15}x^4 + 0.010004...x^6$$

and it determines the corresponding minimax approximation

$$\cos x - \left(\frac{\sin x}{x}\right)^3 \approx -\frac{1}{15}x^4 + 0.010004...x^6.$$

*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2^{-}} g(x) \quad \text{and} \quad B = \lim_{x \to 0^{+}} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 3, strictly decreasing on $(0, \pi/2)$.
$$x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \Longrightarrow \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + px^6$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + Bx^6 \leq -\frac{1}{15}x^4 + px^6.$$

(iv) There is exactly one solution to the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p\left(\frac{\pi}{2}\right),$$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$p_0 = 0.010004...$$

For the value

$$d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}\left(\frac{\pi}{2}\right) = 0.0024209...,$$

the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.010004...$, the minimax approximant of the family is determined as

$$\varphi_{p_0}(x) = -\cos x + \left(\frac{\sin x}{x}\right)^3 - \frac{1}{15}x^4 + 0.010004...x^6$$

and it determines the corresponding minimax approximation

$$\cos x - \left(\frac{\sin x}{x}\right)^3 \approx -\frac{1}{15}x^4 + 0.010004...x^6.$$

*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2^{-}} g(x) \quad \text{and} \quad B = \lim_{x \to 0^{+}} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 3, strictly decreasing on $(0, \pi/2)$.
(i) If $p \in (0, A]$, then

$$g(x) > A \Leftrightarrow (A - g(x))x^6 < 0 \Leftrightarrow \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow -\frac{1}{15}x^4 + px^6 \leq -\frac{1}{15}x^4 + Ax^6 < \cos x - \left(\frac{\sin x}{x}\right)^3.$$

(ii) If $p \in (A, B)$, based on Lemma 3, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$\begin{align*} x \in (0, x_0^{(p)}) &\Longrightarrow g(x) > p \Longleftrightarrow \varphi_p(x) < 0 \\ &\Longleftrightarrow -\frac{1}{15}x^4 + px^6 < \cos x - \left(\frac{\sin x}{x}\right)^3 \end{align*}$$

and

$$\begin{align*} x \in (x_0^{(p)}, \frac{\pi}{2}) &\Longrightarrow g(x) < p \Longleftrightarrow \varphi_p(x) > 0 \\ &\Longleftrightarrow \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + px^6. \end{align*}$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \Leftrightarrow (B - g(x))x^6 > 0 \Leftrightarrow \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + Bx^6 \leq -\frac{1}{15}x^4 + px^6.$$

(iv), (v) Let $p \in (A, B)$. For the family $\varphi_p(x)$, the Taylor's expansions are:

$$(2) \qquad \varphi_p(x) = \left(-\frac{23}{1890} + p\right)x^6 + \frac{41}{37800}x^8 + o(x^8)$$
(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x))x^6 < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies -\frac{1}{15}x^4 + px^6 \le -\frac{1}{15}x^4 + Ax^6 < \cos x - \left(\frac{\sin x}{x}\right)^3.$$

(ii) If $p \in (A, B)$, based on Lemma 3, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$x \in (0, x_0^{(p)}) \implies g(x) > p \iff \varphi_p(x) < 0$$

$$\iff -\frac{1}{15}x^4 + px^6 < \cos x - \left(\frac{\sin x}{x}\right)^3$$

and

$$x \in (x_0^{(p)}, \frac{\pi}{2}) \implies g(x) < p \iff \varphi_p(x) > 0$$

$$\iff \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + px^6.$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x))x^6 > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + Bx^6 \le -\frac{1}{15}x^4 + px^6.$$

(iv), (v) Let $p \in (A, B)$. For the family $\varphi_p(x)$, the Taylor's expansions are:

$$(2) \qquad \varphi_p(x) = \left(-\frac{23}{1890} + p\right)x^6 + \frac{41}{37800}x^8 + o(x^8)$$
and

$$
\begin{equation}
\begin{aligned}
\varphi_p(x) = & \left( \frac{8}{\pi^3} - \frac{\pi^4}{240} + \frac{\pi^6}{64} p \right) + \\
& + \left( -\frac{48}{\pi^4} + 1 - \frac{\pi^3}{30} + \frac{3\pi^5}{16} p \right) \left( x - \frac{\pi}{2} \right) + \\
& + \left( \frac{192}{\pi^5} - \frac{12}{\pi^3} - \frac{\pi^2}{10} + \frac{15\pi^4}{16} p \right) \left( x - \frac{\pi}{2} \right)^2 + \\
& + \left( -\frac{640}{\pi^6} + \frac{72}{\pi^4} - \frac{1}{6} - \frac{2\pi}{15} + \frac{5\pi^3}{2} p \right) \left( x - \frac{\pi}{2} \right)^3 + \\
(3) \qquad & + \left( \frac{1920}{\pi^7} - \frac{288}{\pi^5} + \frac{7}{\pi^3} - \frac{1}{15} + \frac{15\pi^2}{4} p \right) \left( x - \frac{\pi}{2} \right)^4 + \\
& + \left( -\frac{5376}{\pi^8} + \frac{960}{\pi^6} - \frac{42}{\pi^4} + \frac{1}{120} + 3\pi p \right) \left( x - \frac{\pi}{2} \right)^5 + \\
& + \left( \frac{14336}{\pi^9} - \frac{2880}{\pi^7} + \frac{168}{\pi^5} - \frac{61}{30\pi^3} + p \right) \left( x - \frac{\pi}{2} \right)^6 + \\
& + \left( -\frac{36864}{\pi^{10}} + \frac{8064}{\pi^8} - \frac{560}{\pi^6} + \frac{61}{5\pi^4} - \frac{1}{5040} \right) \left( x - \frac{\pi}{2} \right)^7 + \\
& + o \left( \left( x - \frac{\pi}{2} \right)^7 \right).
\end{aligned}
\end{equation}
$$

For $p \in (A, B)$, functions $\varphi_p(x)$ don't satisfy all of the conditions of the Nike theorem. In consequence, we use the Second Nike theorem. Now we check the fulfillment of the Second Nike theorem:

(a) Let us observe the seventh derivative

$$
\begin{aligned}
\varphi_p^{(7)}(x) ={}& \frac{1}{x^{10}} \left( (2187 x^7 - 61236 x^5 + 340200 x^3 - 423360 x) \cos^3 x + \right. \\
& \qquad \left. + (-15309 x^6 + 170100 x^4 - 476280 x^2 + 181440) \sin x \cos^2 x + \right. \\
& \qquad \left. + (-1641 x^7 + 46116 x^5 - 264600 x^3 + 423360 x) \cos x + \right. \\
& \qquad \left. + (-x^{10} + 3843 x^6 - 44100 x^4 + 158760 x^2 - 181440) \sin x \right),
\end{aligned}
$$

for $x \in (0, \pi/2)$. Now we prove that function $\varphi_p^{(7)}(x)$ has exactly one zero $c$ on $(0, \pi/2)$ such that $\varphi_p^{(7)}(x) > 0$ for $x \in (0, c)$, and $\varphi_p^{(7)}(x) < 0$ for $x \in (c, \pi/2)$. Function $\varphi_p^{(7)}(x)$ is positive for $x \in [0, 1]$ because, according to [3], there exists proof that the numerator of $\varphi_p^{(7)}(x)$ is positive on $[0, 1]$. The proof is given in
and

$$
\begin{equation}
\begin{aligned}
\varphi_p(x) = & \left( \frac{8}{\pi^3} - \frac{\pi^4}{240} + \frac{\pi^6}{64} p \right) + \\
& + \left( -\frac{48}{\pi^4} + 1 - \frac{\pi^3}{30} + \frac{3\pi^5}{16} p \right) \left( x - \frac{\pi}{2} \right) + \\
& + \left( \frac{192}{\pi^5} - \frac{12}{\pi^3} - \frac{\pi^2}{10} + \frac{15\pi^4}{16} p \right) \left( x - \frac{\pi}{2} \right)^2 + \\
& + \left( -\frac{640}{\pi^6} + \frac{72}{\pi^4} - \frac{1}{6} - \frac{2\pi}{15} + \frac{5\pi^3}{2} p \right) \left( x - \frac{\pi}{2} \right)^3 + \\
(3) \qquad & + \left( \frac{1920}{\pi^7} - \frac{288}{\pi^5} + \frac{7}{\pi^3} - \frac{1}{15} + \frac{15\pi^2}{4} p \right) \left( x - \frac{\pi}{2} \right)^4 + \\
& + \left( -\frac{5376}{\pi^8} + \frac{960}{\pi^6} - \frac{42}{\pi^4} + \frac{1}{120} + 3\pi p \right) \left( x - \frac{\pi}{2} \right)^5 + \\
& + \left( \frac{14336}{\pi^9} - \frac{2880}{\pi^7} + \frac{168}{\pi^5} - \frac{61}{30\pi^3} + p \right) \left( x - \frac{\pi}{2} \right)^6 + \\
& + \left( -\frac{36864}{\pi^{10}} + \frac{8064}{\pi^8} - \frac{560}{\pi^6} + \frac{61}{5\pi^4} - \frac{1}{5040} \right) \left( x - \frac{\pi}{2} \right)^7 + \\
& + o \left( \left( x - \frac{\pi}{2} \right)^7 \right).
\end{aligned}
\end{equation}
$$

For $p \in (A, B)$, functions $\varphi_p(x)$ don't satisfy all of the conditions of the Nike theorem. In consequence, we use the Second Nike theorem. Now we check the fulfillment of the Second Nike theorem:

(a) Let us observe the seventh derivative

$$
\begin{aligned}
\varphi_p^{(7)}(x) ={}& \frac{1}{x^{10}} \left( (2187 x^7 - 61236 x^5 + 340200 x^3 - 423360 x) \cos^3 x + \right. \\
& \qquad \left. + (-15309 x^6 + 170100 x^4 - 476280 x^2 + 181440) \sin x \cos^2 x + \right. \\
& \qquad \left. + (-1641 x^7 + 46116 x^5 - 264600 x^3 + 423360 x) \cos x + \right. \\
& \qquad \left. + (-x^{10} + 3843 x^6 - 44100 x^4 + 158760 x^2 - 181440) \sin x \right),
\end{aligned}
$$

for $x \in (0, \pi/2)$. Now we prove that function $\varphi_p^{(7)}(x)$ has exactly one zero $c$ on $(0, \pi/2)$ such that $\varphi_p^{(7)}(x) > 0$ for $x \in (0, c)$, and $\varphi_p^{(7)}(x) < 0$ for $x \in (c, \pi/2)$. Function $\varphi_p^{(7)}(x)$ is positive for $x \in [0, 1]$ because, according to [3], there exists proof that the numerator of $\varphi_p^{(7)}(x)$ is positive on $[0, 1]$. The proof is given in
**Appendix A2.** Furthermore, let us observe the eighth derivative

$$ \varphi_p^{(8)}(x) = \frac{1}{x^{11}} \left( \begin{aligned} & (-52488x^7 + 816480x^5 - 3810240x^3 + 4354560x) \cos^3 x + \\ & \quad (-6561x^8 + 244944x^6 - 2041200x^4 + 5080320x^2 - 1814400) \sin x \cos^2 x + \\ & \quad (-x^{11} + 39384x^7 - 614880x^5 + 2963520x^3 - 4354560x) \cos x + \\ & \quad (1641x^8 - 61488x^6 + 529200x^4 - 1693440x^2 + 1814400) \sin x \end{aligned} \right), $$

for $x \in (0, \pi/2)$. According to [3], there exists proof that the numerator of $\varphi_p^{(8)}(x)$ is negative on $[1, \pi/2]$. It is enough to prove that $\varphi_p^{(8)}(x)$ is negative on $[1, \pi/2]$ using MacLaurin polynomials. The proof is given in **Appendix A3.** Finally,

$$ \varphi_p^{(7)}\left(\frac{\pi}{2}\right) = \frac{-\pi^{10} + 61488\pi^6 - 2822400\pi^4 + 40642560\pi^2 - 185794560}{\pi^{10}} = -6.14789\dots < 0. $$

Therefore, there exists exactly one zero $c \in (0, \pi/2)$ of function $\varphi_p^{(7)}(x)$ such that $\varphi_p^{(7)}(x) > 0$ for $x \in (0, c)$ and $\varphi_p^{(7)}(x) < 0$ for $x \in (c, \pi/2)$, where $c$ is numerically determined as $c = 1.40749\dots$. It is hereby shown that for $m = 7$, the first condition of the Second Nike theorem is satisfied.

(b) According to (2), there is a right neighbourhood $U_0$ of zero in which

$$ \varphi_p(x) < 0, \quad \varphi_p'(x) < 0, \quad \dots, \quad \varphi_p^{(6)}(x) < 0 \quad (x \in U_0) $$

hold.

(c) According to (3), there is a left neighbourhood $U_{\pi/2}$ of $\pi/2$ in which

$$ \varphi_p(x) > 0, \quad \varphi_p'(x) > 0, \quad \dots, \quad \varphi_p^{(6)}(x) > 0 \quad (x \in U_{\pi/2}) $$

hold. Then, for every function $\varphi_p(x)$, on the interval $(0, \pi/2)$, there exists exactly one extremum $t$, which is minimum, and there exists exactly one zero $x_0$. Hence, for the family of functions $\varphi_p(x)$, conditions of the Second Nike theorem are satisfied, as well as conditions of Theorem 7, which implies the existence of a minimax approximant. Minimax approximant and error can be numerically determined via Maple software in the following way: let $f(x, p) := \varphi_p(x)$ and $F(x, p) := \varphi'_p(x)$, then using the command

$$ \texttt{fsolve}(\{F(x,p) = 0, \text{abs}(f(x,p)) = f(\pi/2,p)\}, \{x = 0..\pi/2, p = A..B\}); $$

we get

$$ \{p = 0.01000418287, x = 1.299862713\} $$

and, for $p_0 = 0.010004\dots$, we get

$$ f(x, p_0) = -\cos x + \left(\frac{\sin x}{x}\right)^3 - \frac{1}{15}x^4 + 0.010004\dots x^6 $$
**Appendix A2.** Furthermore, let us observe the eighth derivative

$$ \varphi_p^{(8)}(x) = \frac{1}{x^{11}} \left( \begin{aligned} & (-52488x^7 + 816480x^5 - 3810240x^3 + 4354560x) \cos^3 x + \\ & \quad (-6561x^8 + 244944x^6 - 2041200x^4 + 5080320x^2 - 1814400) \sin x \cos^2 x + \\ & \quad (-x^{11} + 39384x^7 - 614880x^5 + 2963520x^3 - 4354560x) \cos x + \\ & \quad (1641x^8 - 61488x^6 + 529200x^4 - 1693440x^2 + 1814400) \sin x \end{aligned} \right), $$

for $x \in (0, \pi/2)$. According to [3], there exists proof that the numerator of $\varphi_p^{(8)}(x)$ is negative on $[1, \pi/2]$. It is enough to prove that $\varphi_p^{(8)}(x)$ is negative on $[1, \pi/2]$ using MacLaurin polynomials. The proof is given in **Appendix A3.** Finally,

$$ \varphi_p^{(7)}\left(\frac{\pi}{2}\right) = \frac{-\pi^{10} + 61488\pi^6 - 2822400\pi^4 + 40642560\pi^2 - 185794560}{\pi^{10}} = -6.14789\dots < 0. $$

Therefore, there exists exactly one zero $c \in (0, \pi/2)$ of function $\varphi_p^{(7)}(x)$ such that $\varphi_p^{(7)}(x) > 0$ for $x \in (0, c)$ and $\varphi_p^{(7)}(x) < 0$ for $x \in (c, \pi/2)$, where $c$ is numerically determined as $c = 1.40749\dots$. It is hereby shown that for $m = 7$, the first condition of the Second Nike theorem is satisfied.

(b) According to (2), there is a right neighbourhood $\mathcal{U}_0$ of zero in which

$$ \varphi_p(x) < 0, \quad \varphi_p'(x) < 0, \quad \dots, \quad \varphi_p^{(6)}(x) < 0 \quad (x \in \mathcal{U}_0) $$

hold.

(c) According to (3), there is a left neighbourhood $\mathcal{U}_{\pi/2}$ of $\pi/2$ in which

$$ \varphi_p(x) > 0, \quad \varphi_p'(x) > 0, \quad \dots, \quad \varphi_p^{(6)}(x) > 0 \quad (x \in \mathcal{U}_{\pi/2}) $$

hold. Then, for every function $\varphi_p(x)$, on the interval $(0, \pi/2)$, there exists exactly one extremum $t$, which is minimum, and there exists exactly one zero $x_0$. Hence, for the family of functions $\varphi_p(x)$, conditions of the Second Nike theorem are satisfied, as well as conditions of Theorem 7, which implies the existence of a minimax approximant. Minimax approximant and error can be numerically determined via Maple software in the following way: let $f(x, p) := \varphi_p(x)$ and $F(x, p) := \varphi'_p(x)$, then using the command

$$ \texttt{fsolve}(\{F(x,p) = 0, \text{abs}(f(x,p)) = f(\pi/2,p)\}, \{x = 0..\pi/2, p = A..B\}); $$

we get

$$ \{p = 0.01000418287, x = 1.299862713\} $$

and, for $p_0 = 0.010004\dots$, we get

$$ f(x, p_0) = -\cos x + \left(\frac{\sin x}{x}\right)^3 - \frac{1}{15}x^4 + 0.010004\dots x^6 $$
and

$$d_0 = f\left(\frac{\pi}{2}, p_0\right) = 0.0024209\dots$$

□

Based on the previous considerations, enhancement of Theorem 1 has been obtained in the following form:

**Proposition 1.** For every $0 < x < \pi/2$, the following inequalities hold

$$-\frac{1}{15}x^4 + \frac{4\pi^7 - 7680}{15\pi^9}x^6 < \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + \frac{23}{1890}x^6,$$

and the constants $A = \frac{4\pi^7 - 7680}{15\pi^9} = 0.0098430\dots$ and $B = \frac{23}{1890} = 0.012169\dots$ are the best possible.

**Improvement of Theorem 2**

**Lemma 4.** The family of functions

$$\varphi_p(x) = -\frac{\sin x}{x} + \frac{\cos x + 2}{3} - \frac{1}{180}x^4 + p x^6 \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

Let us introduce the function $g(x)$ so that the equivalence

$$\varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+$$

holds. Then

$$g(x) = \frac{x^5 - 60x \cos x + 180 \sin x - 120x}{180x^7}, \quad x \in (0, \frac{\pi}{2}).$$

Note that

$$\varphi_p(x) = (p - g(x))x^6.$$

**Lemma 5.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$g'(x) = \frac{270x \cos x + 30x^2 \sin x - 630 \sin x - x^5 + 360x}{90x^8}.$$

It holds

$$g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}),$$

where

$$f(x) = x^5 - 360x - 270x \cos x - 30x^2 \sin x + 630 \sin x.$$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A4**. □
and

$$d_0 = f\left(\frac{\pi}{2}, p_0\right) = 0.0024209\dots \quad \square$$

<figure><img src="image_2.png" /></figure>

Based on the previous considerations, enhancement of Theorem 1 has been obtained in the following form:

**Proposition 1.** For every $0 < x < \pi/2$, the following inequalities hold

$$-\frac{1}{15}x^4 + \frac{4\pi^7 - 7680}{15\pi^9}x^6 < \cos x - \left(\frac{\sin x}{x}\right)^3 < -\frac{1}{15}x^4 + \frac{23}{1890}x^6,$$

and the constants $A = \frac{4\pi^7 - 7680}{15\pi^9} = 0.0098430\dots$ and $B = \frac{23}{1890} = 0.012169\dots$ are the best possible.

**Improvement of Theorem 2**

**Lemma 4.** The family of functions

$$\varphi_p(x) = -\frac{\sin x}{x} + \frac{\cos x + 2}{3} - \frac{1}{180}x^4 + p x^6 \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

Let us introduce the function $g(x)$ so that the equivalence

$$\varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+$$

holds. Then

$$g(x) = \frac{x^5 - 60x \cos x + 180 \sin x - 120x}{180 x^7}, \quad x \in (0, \frac{\pi}{2}).$$

Note that

$$\varphi_p(x) = (p - g(x))x^6.$$

**Lemma 5.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$g'(x) = \frac{270 x \cos x + 30 x^2 \sin x - 630 \sin x - x^5 + 360 x}{90 x^8}.$$

It holds

$$g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}),$$

where

$$f(x) = x^5 - 360x - 270x \cos x - 30x^2 \sin x + 630 \sin x.$$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A4**. □

<figure><img src="image_3.png" /></figure>
**Statement 2.** Let

$$A = \frac{\pi^5 - 1920\pi + 5760}{45\pi^7} = 0.00025135... \quad \text{and} \quad B = \frac{1}{3780} = 0.00026455...$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow -\frac{1}{180}x^4 + px^6 \leq -\frac{1}{180}x^4 + Ax^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}.$$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in \left(0, x_0^{(p)}\right) \Longrightarrow -\frac{1}{180}x^4 + px^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}$$

and

$$x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \Longrightarrow \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + px^6$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + Bx^6 \leq -\frac{1}{180}x^4 + px^6.$$

(iv) There is exactly one solution to the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p\left(\frac{\pi}{2}\right),$$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$p_0 = 0.00025234...$$

For the value

$$d_0 = \left|\varphi_{p_0}(t^{(p_0)})\right| = \varphi_{p_0}\left(\frac{\pi}{2}\right) = 0.000014887...,$$

the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.00025234...$, the minimax approximation of the family is determined as

$$\varphi_{p_0}(x) = -\frac{\sin x}{x} + \frac{\cos x + 2}{3} - \frac{1}{180}x^4 + 0.00025234...x^6$$

and it determines the corresponding minimax approximation

$$\frac{\sin x}{x} - \frac{\cos x + 2}{3} \approx -\frac{1}{180}x^4 + 0.00025234...x^6.$$
**Statement 2.** Let

$$A = \frac{\pi^5 - 1920\pi + 5760}{45\pi^7} = 0.00025135... \quad \text{and} \quad B = \frac{1}{3780} = 0.00026455...$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow -\frac{1}{180}x^4 + px^6 \leq -\frac{1}{180}x^4 + Ax^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}.$$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in \left(0, x_0^{(p)}\right) \Longrightarrow -\frac{1}{180}x^4 + px^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}$$

and

$$x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \Longrightarrow \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + px^6$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + Bx^6 \leq -\frac{1}{180}x^4 + px^6.$$

(iv) There is exactly one solution to the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p\left(\frac{\pi}{2}\right),$$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$p_0 = 0.00025234...$$

For the value

$$d_0 = \left|\varphi_{p_0}(t^{(p_0)})\right| = \varphi_{p_0}\left(\frac{\pi}{2}\right) = 0.000014887...,$$

the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.00025234...$, the minimax approximation of the family is determined as

$$\varphi_{p_0}(x) = -\frac{\sin x}{x} + \frac{\cos x + 2}{3} - \frac{1}{180}x^4 + 0.00025234...x^6$$

and it determines the corresponding minimax approximation

$$\frac{\sin x}{x} - \frac{\cos x + 2}{3} \approx -\frac{1}{180}x^4 + 0.00025234...x^6.$$
*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2-} g(x) \quad \text{and} \quad B = \lim_{x \to 0+} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 5, strictly decreasing on $(0, \pi/2)$.

(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x))x^6 < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies -\frac{1}{180}x^4 + p x^6 \leq -\frac{1}{180}x^4 + Ax^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}.$$

(ii) If $p \in (A, B)$, based on Lemma 5, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$\begin{align*}
x \in (0, x_0^{(p)}) &\implies g(x) > p \iff \varphi_p(x) < 0 \\
&\iff -\frac{1}{180}x^4 + p x^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}
\end{align*}$$

and

$$\begin{align*}
x \in (x_0^{(p)}, \frac{\pi}{2}) &\implies g(x) < p \iff \varphi_p(x) > 0 \\
&\iff \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + p x^6.
\end{align*}$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x))x^6 > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + Bx^6 \leq -\frac{1}{180}x^4 + px^6.$$

(iv), (v) Let $p \in (A, B)$. For the family $\varphi_p(x)$, the Taylor's expansions are:

(4) $$\varphi_p(x) = \left(-\frac{1}{3780} + p\right)x^6 + \frac{1}{181440}x^8 + o(x^8)$$
*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2-} g(x) \quad \text{and} \quad B = \lim_{x \to 0+} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 5, strictly decreasing on $(0, \pi/2)$.

(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x))x^6 < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies -\frac{1}{180}x^4 + px^6 \leq -\frac{1}{180}x^4 + Ax^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}.$$

(ii) If $p \in (A, B)$, based on Lemma 5, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$\begin{align*}
x \in (0, x_0^{(p)}) &\implies g(x) > p \iff \varphi_p(x) < 0 \\
&\iff -\frac{1}{180}x^4 + px^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3}
\end{align*}$$

and

$$\begin{align*}
x \in (x_0^{(p)}, \frac{\pi}{2}) &\implies g(x) < p \iff \varphi_p(x) > 0 \\
&\iff \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + px^6.
\end{align*}$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x))x^6 > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + Bx^6 \leq -\frac{1}{180}x^4 + px^6.$$

(iv), (v) Let $p \in (A, B)$. For the family $\varphi_p(x)$, the Taylor's expansions are:

$$(4) \qquad \varphi_p(x) = \left(-\frac{1}{3780} + p\right)x^6 + \frac{1}{181440}x^8 + o(x^8)$$
and

$$
\begin{align}
\varphi_p(x) = & \left(-\frac{2}{\pi} + \frac{2}{3} - \frac{\pi^4}{2880} + \frac{\pi^6}{64} p\right) + \nonumber \\
& + \left(\frac{4}{\pi^2} - \frac{1}{3} - \frac{\pi^3}{360} + \frac{3\pi^5}{16} p\right) \left(x - \frac{\pi}{2}\right) + \nonumber \\
& + \left(-\frac{8}{\pi^3} + \frac{1}{\pi} - \frac{\pi^2}{120} + \frac{15\pi^4}{16} p\right) \left(x - \frac{\pi}{2}\right)^2 + \nonumber \\
& + \left(\frac{16}{\pi^4} - \frac{2}{\pi^2} + \frac{1}{18} - \frac{\pi}{90} + \frac{5\pi^3}{2} p\right) \left(x - \frac{\pi}{2}\right)^3 + \nonumber \\
(5) \qquad & + \left(-\frac{32}{\pi^5} + \frac{4}{\pi^3} - \frac{1}{12\pi} - \frac{1}{180} + \frac{15\pi^2}{4} p\right) \left(x - \frac{\pi}{2}\right)^4 + \nonumber \\
& + \left(\frac{64}{\pi^6} - \frac{8}{\pi^4} + \frac{1}{6\pi^2} - \frac{1}{360} + 3\pi p\right) \left(x - \frac{\pi}{2}\right)^5 + \nonumber \\
& + \left(-\frac{128}{\pi^7} + \frac{16}{\pi^5} - \frac{1}{3\pi^3} + \frac{1}{360\pi} + p\right) \left(x - \frac{\pi}{2}\right)^6 + \nonumber \\
& + \left(\frac{256}{\pi^8} - \frac{32}{\pi^6} + \frac{2}{3\pi^4} - \frac{1}{180\pi^2} + \frac{1}{15120}\right) \left(x - \frac{\pi}{2}\right)^7 + \nonumber \\
& + o\left(\left(x - \frac{\pi}{2}\right)^7\right). \nonumber
\end{align}
$$

For $p \in (A, B)$, functions $\varphi_p(x)$ satisfy all of the conditions of the Nike theorem.
Now we check the fulfillment of the Nike theorem:

(a) Let us observe the seventh derivative

$$
\varphi_p^{(7)}(x) = \frac{1}{3x^8} \left( \begin{aligned} & (x^8 - 21x^6 + 630x^4 - 7560x^2 + 15120) \sin x + \\ & + 3x(x^6 - 42x^4 + 840x^2 - 5040) \cos x \end{aligned} \right)
$$

for $x \in (0, \pi/2)$. According to [3], there exists proof that the numerator of $\varphi_p^{(7)}(x)$ is positive on $[0, \pi/2]$. The proof is given in **Appendix A5**. Thus, for $m = 7$, the first condition of the Nike theorem is satisfied.

(b) According to (4), there is a right neighbourhood $U_0$ of zero in which

$$
\varphi_p(x) < 0, \quad \varphi'_p(x) < 0, \quad \dots, \quad \varphi_p^{(6)}(x) < 0 \quad (x \in \mathcal{U}_0)
$$

hold.

(c) According to (5), there is a left neighbourhood $U_{\pi/2}$ of $\pi/2$ in which

$$
\varphi_p(x) > 0, \quad \varphi'_p(x) > 0, \quad \dots, \quad \varphi_p^{(6)}(x) > 0 \quad (x \in \mathcal{U}_{\pi/2})
$$
and

$$
\begin{align}
\varphi_p(x) = & \left(-\frac{2}{\pi} + \frac{2}{3} - \frac{\pi^4}{2880} + \frac{\pi^6}{64} p\right) + \nonumber \\
& + \left(\frac{4}{\pi^2} - \frac{1}{3} - \frac{\pi^3}{360} + \frac{3\pi^5}{16} p\right) \left(x - \frac{\pi}{2}\right) + \nonumber \\
& + \left(-\frac{8}{\pi^3} + \frac{1}{\pi} - \frac{\pi^2}{120} + \frac{15\pi^4}{16} p\right) \left(x - \frac{\pi}{2}\right)^2 + \nonumber \\
& + \left(\frac{16}{\pi^4} - \frac{2}{\pi^2} + \frac{1}{18} - \frac{\pi}{90} + \frac{5\pi^3}{2} p\right) \left(x - \frac{\pi}{2}\right)^3 + \nonumber \\
(5) \qquad & + \left(-\frac{32}{\pi^5} + \frac{4}{\pi^3} - \frac{1}{12\pi} - \frac{1}{180} + \frac{15\pi^2}{4} p\right) \left(x - \frac{\pi}{2}\right)^4 + \nonumber \\
& + \left(\frac{64}{\pi^6} - \frac{8}{\pi^4} + \frac{1}{6\pi^2} - \frac{1}{360} + 3\pi p\right) \left(x - \frac{\pi}{2}\right)^5 + \nonumber \\
& + \left(-\frac{128}{\pi^7} + \frac{16}{\pi^5} - \frac{1}{3\pi^3} + \frac{1}{360\pi} + p\right) \left(x - \frac{\pi}{2}\right)^6 + \nonumber \\
& + \left(\frac{256}{\pi^8} - \frac{32}{\pi^6} + \frac{2}{3\pi^4} - \frac{1}{180\pi^2} + \frac{1}{15120}\right) \left(x - \frac{\pi}{2}\right)^7 + \nonumber \\
& + o\left(\left(x - \frac{\pi}{2}\right)^7\right). \nonumber
\end{align}
$$

For $p \in (A, B)$, functions $\varphi_p(x)$ satisfy all of the conditions of the Nike theorem.
Now we check the fulfillment of the Nike theorem:

(a) Let us observe the seventh derivative

$$
\varphi_p^{(7)}(x) = \frac{1}{3x^8} \left( \begin{aligned} & (x^8 - 21x^6 + 630x^4 - 7560x^2 + 15120) \sin x + \\ & + 3x(x^6 - 42x^4 + 840x^2 - 5040) \cos x \end{aligned} \right)
$$

for $x \in (0, \pi/2)$. According to [3], there exists proof that the numerator of $\varphi_p^{(7)}(x)$ is positive on $[0, \pi/2]$. The proof is given in **Appendix A5**. Thus, for $m = 7$, the first condition of the Nike theorem is satisfied.

(b) According to (4), there is a right neighbourhood $U_0$ of zero in which

$$
\varphi_p(x) < 0, \quad \varphi'_p(x) < 0, \quad \dots, \quad \varphi_p^{(6)}(x) < 0 \quad (x \in U_0)
$$

hold.

(c) According to (5), there is a left neighbourhood $U_{\pi/2}$ of $\pi/2$ in which

$$
\varphi_p(x) > 0, \quad \varphi'_p(x) > 0, \quad \dots, \quad \varphi_p^{(6)}(x) > 0 \quad (x \in U_{\pi/2})
$$
hold. Then, for every function $\varphi_p(x)$, on the interval $(0, \pi/2)$, there exists exactly one extremum $t$, which is minimum, and there exists exactly one zero $x_0$. Hence, for the family of functions $\varphi_p(x)$, conditions of the Nike theorem are satisfied, as well as conditions of Theorem 7, which implies the existence of a minimax approximant. Minimax approximant and error can be numerically determined via Maple software in the following way: $f(x,p) := \varphi_p(x)$ and $F(x,p) := \varphi'_p(x)$, then using the command

$$fsolve(\{F(x,p) = 0, \text{abs}(f(x,p)) = f(\pi/2,p)\}, \{x = 0..\pi/2, p = A..B\});$$

we get

$$\{p = 0.000252341144, x = 1.305655179\}$$

and, for $p_0 = 0.00025234...$, we get

$$f(x, p_0) = -\frac{\sin x}{x} + \frac{\cos x + 2}{3} - \frac{1}{180}x^4 + 0.00025234... x^6$$

and

$$d_0 = f\left(\frac{\pi}{2}, p_0\right) = 0.000014887... .$$

□

Based on the previous considerations, enhancement of Theorem 2 has been obtained in the following form:

**Proposition 2.** For every $0 < x < \pi/2$, the following inequalities hold

$$-\frac{1}{180}x^4 + \frac{\pi^5 - 1920\pi + 5760}{45\pi^7}x^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + \frac{1}{3780}x^6,$$

and the constants $A = \frac{\pi^5 - 1920\pi + 5760}{45\pi^7} = 0.00025135...$ and $B = \frac{1}{3780} = 0.00026455...$ are the best possible.

**Improvement of Theorem 3**

**Lemma 6.** The family of functions

$$\varphi_p(x) = 2 \frac{\sin x}{x} + \frac{\tan x}{x} - 3 - \frac{3}{20} x^4 \frac{1}{\cos x} + p x^6 \frac{1}{\cos x} \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

Let us introduce the function $g(x)$ so that the equivalence

$$\varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+$$

holds. Then

$$g(x) = \frac{3x^5 - 40 \sin x \cos x + 60 x \cos x - 20 \sin x}{20 x^7}, \quad x \in (0, \frac{\pi}{2}).$$

Note that

$$\varphi_p(x) = (p - g(x)) \frac{x^6}{\cos x}.$$
hold. Then, for every function $\varphi_p(x)$, on the interval $(0, \pi/2)$, there exists exactly one extremum $t$, which is minimum, and there exists exactly one zero $x_0$. Hence, for the family of functions $\varphi_p(x)$, conditions of the Nike theorem are satisfied, as well as conditions of Theorem 7, which implies the existence of a minimax approximant. Minimax approximant and error can be numerically determined via Maple software in the following way: $f(x,p) := \varphi_p(x)$ and $F(x,p) := \varphi'_p(x)$, then using the command

$$fsolve(\{F(x,p) = 0, \text{abs}(f(x,p)) = f(\pi/2,p)\}, \{x = 0..\pi/2, p = A..B\});$$

we get

$$\{p = 0.000252341144, x = 1.305655179\}$$

and, for $p_0 = 0.00025234...$, we get

$$f(x, p_0) = -\frac{\sin x}{x} + \frac{\cos x + 2}{3} - \frac{1}{180}x^4 + 0.00025234... x^6$$

and

$$d_0 = f\left(\frac{\pi}{2}, p_0\right) = 0.000014887... .$$

□

Based on the previous considerations, enhancement of Theorem 2 has been obtained in the following form:

**Proposition 2.** For every $0 < x < \pi/2$, the following inequalities hold

$$-\frac{1}{180}x^4 + \frac{\pi^5 - 1920\pi + 5760}{45\pi^7}x^6 < \frac{\sin x}{x} - \frac{\cos x + 2}{3} < -\frac{1}{180}x^4 + \frac{1}{3780}x^6,$$

and the constants $A = \frac{\pi^5 - 1920\pi + 5760}{45\pi^7} = 0.00025135...$ and $B = \frac{1}{3780} = 0.00026455...$ are the best possible.

**Improvement of Theorem 3**

**Lemma 6.** The family of functions

$$\varphi_p(x) = 2 \frac{\sin x}{x} + \frac{\tan x}{x} - 3 - \frac{3}{20} x^4 \frac{1}{\cos x} + p x^6 \frac{1}{\cos x} \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

Let us introduce the function $g(x)$ so that the equivalence

$$\varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+$$

holds. Then

$$g(x) = \frac{3x^5 - 40 \sin x \cos x + 60 x \cos x - 20 \sin x}{20 x^7}, \quad x \in (0, \frac{\pi}{2}).$$

Note that

$$\varphi_p(x) = (p - g(x)) \frac{x^6}{\cos x}.$$
**Lemma 7.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$g'(x) = \frac{-40x \cos^2 x - 190x \cos x + 140 \sin x \cos x - (30x^2 - 70) \sin x - 3x^5 + 20x}{10x^8}.$$

It holds

$$g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}),$$

where

$$f(x) = 40x \cos^2 x + 190x \cos x - 140 \sin x \cos x + (30x^2 - 70) \sin x + 3x^5 - 20x.$$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A6**. $\square$

**Statement 3.** Let

$$A = \frac{3\pi^5 - 640}{5\pi^7} = 0.018412\dots \quad \text{and} \quad B = \frac{3}{140} = 0.021428\dots.$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ &\le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}. \end{aligned}$$

(ii) If $p \in (A, B)$, then $\phi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in (0, x_0^{(p)}) \implies 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}$$

and

$$x \in (x_0^{(p)}, \frac{\pi}{2}) \implies 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < 2 \frac{\sin x}{x} + \frac{\tan x}{x}$$

hold.

(iii) If $p \in [B, \infty)$, then

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\ &< 2 \frac{\sin x}{x} + \frac{\tan x}{x}. \end{aligned}$$
**Lemma 7.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$g'(x) = \frac{-40x \cos^2 x - 190x \cos x + 140 \sin x \cos x - (30x^2 - 70) \sin x - 3x^5 + 20x}{10x^8}.$$

It holds

$$g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}),$$

where

$$f(x) = 40x \cos^2 x + 190x \cos x - 140 \sin x \cos x + (30x^2 - 70) \sin x + 3x^5 - 20x.$$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A6**. $\square$

**Statement 3.** Let

$$A = \frac{3\pi^5 - 640}{5\pi^7} = 0.018412\dots \quad \text{and} \quad B = \frac{3}{140} = 0.021428\dots.$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ &\le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}. \end{aligned}$$

(ii) If $p \in (A, B)$, then $\phi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in (0, x_0^{(p)}) \implies 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}$$

and

$$x \in (x_0^{(p)}, \frac{\pi}{2}) \implies 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < 2 \frac{\sin x}{x} + \frac{\tan x}{x}$$

hold.

(iii) If $p \in [B, \infty)$, then

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\ &< 2 \frac{\sin x}{x} + \frac{\tan x}{x}. \end{aligned}$$
*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2^{-}} g(x) \quad \text{and} \quad B = \lim_{x \to 0^{+}} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 7, strictly decreasing on $(0, \pi/2)$.

(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x)) \frac{x^6}{\cos x} < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$\begin{aligned} x \in (0, \frac{\pi}{2}) \implies & 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ & \le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}. \end{aligned}$$

(ii) If $p \in (A, B)$, based on Lemma 7, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$\begin{aligned} x \in (0, x_0^{(p)}) \implies & g(x) > p \iff \varphi_p(x) < 0 \\ \iff & 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \end{aligned}$$

and

$$\begin{aligned} x \in (x_0^{(p)}, \frac{\pi}{2}) \implies & g(x) < p \iff \varphi_p(x) > 0 \\ \iff & 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < 2 \frac{\sin x}{x} + \frac{\tan x}{x}. \end{aligned}$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x)) \frac{x^6}{\cos x} > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$\begin{aligned} x \in (0, \frac{\pi}{2}) \implies & 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\ & < 2 \frac{\sin x}{x} + \frac{\tan x}{x}. \end{aligned}$$

□
*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2^{-}} g(x) \quad \text{and} \quad B = \lim_{x \to 0^{+}} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 7, strictly decreasing on $(0, \pi/2)$.

(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x)) \frac{x^6}{\cos x} < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$\begin{aligned} x \in (0, \frac{\pi}{2}) \implies & 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ & \le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}. \end{aligned}$$

(ii) If $p \in (A, B)$, based on Lemma 7, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$\begin{aligned} x \in (0, x_0^{(p)}) \implies & g(x) > p \iff \varphi_p(x) < 0 \\ & \iff 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \end{aligned}$$

and

$$\begin{aligned} x \in (x_0^{(p)}, \frac{\pi}{2}) \implies & g(x) < p \iff \varphi_p(x) > 0 \\ & \iff 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < 2 \frac{\sin x}{x} + \frac{\tan x}{x}. \end{aligned}$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x)) \frac{x^6}{\cos x} > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$\begin{aligned} x \in (0, \frac{\pi}{2}) \implies & 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 3 + \frac{3}{20} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\ & < 2 \frac{\sin x}{x} + \frac{\tan x}{x}. \end{aligned}$$

□
Let us notice that $\varphi_B(\pi/2-) = +\infty$. Hence, one of the conditions of Theorem 7 is not satisfied, thus, the minimax approximant is not considered.

Based on the previous considerations, enhancement of Theorem 3 has been obtained in the following form:

**Proposition 3.** For every $0 < x < \pi/2$, the following inequalities hold

$$3 + \left(\frac{3x^4}{20} - \frac{3x^6}{140}\right) \frac{1}{\cos x} < 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \left(\frac{3x^4}{20} - \frac{(3\pi^5 - 640)x^6}{5\pi^7}\right) \frac{1}{\cos x},$$

and the constants $A = \frac{3\pi^5 - 640}{5\pi^7} = 0.018412...$ and $B = \frac{3}{140} = 0.021428...$ are the best possible.

**Improvement of Theorem 4**

**Lemma 8.** The family of functions

$$\varphi_p(x) = \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} - 2 - \frac{8}{45} x^4 \frac{1}{\cos x} + p x^6 \frac{1}{\cos x} \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

Let us introduce the function $g(x)$ so that the equivalence

$$\varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+$$

holds. Then

$$g(x) = \frac{8x^6 + 90x^2 \cos x - 45 \sin^2 x \cos x - 45 x \sin x}{45 x^8}, \quad x \in (0, \frac{\pi}{2}).$$

Note that

$$\varphi_p(x) = (p - g(x)) \frac{x^6}{\cos x}.$$

**Lemma 9.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$g'(x) = \frac{-360 \cos^3 x - 135x \sin x \cos^2 x - (585x^2 - 360) \cos x - (90x^3 - 360x) \sin x - 16x^6}{45x^9}.$$

It holds

$$g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}),$$

where

$$f(x) = 360 \cos^3 x + 135x \sin x \cos^2 x + (585x^2 - 360) \cos x + (90x^3 - 360x) \sin x + 16x^6.$$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A7**. □
Let us notice that $\varphi_B(\pi/2-) = +\infty$. Hence, one of the conditions of Theorem 7 is not satisfied, thus, the minimax approximant is not considered.

Based on the previous considerations, enhancement of Theorem 3 has been obtained in the following form:

**Proposition 3.** For every $0 < x < \pi/2$, the following inequalities hold

$$3 + \left(\frac{3x^4}{20} - \frac{3x^6}{140}\right) \frac{1}{\cos x} < 2 \frac{\sin x}{x} + \frac{\tan x}{x} < 3 + \left(\frac{3x^4}{20} - \frac{(3\pi^5 - 640)x^6}{5\pi^7}\right) \frac{1}{\cos x},$$

and the constants $A = \frac{3\pi^5 - 640}{5\pi^7} = 0.018412...$ and $B = \frac{3}{140} = 0.021428...$ are the best possible.

**Improvement of Theorem 4**

**Lemma 8.** The family of functions

$$\varphi_p(x) = \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} - 2 - \frac{8}{45} x^4 \frac{1}{\cos x} + p x^6 \frac{1}{\cos x} \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is increasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

Let us introduce the function $g(x)$ so that the equivalence

$$\varphi_p(x) = 0 \iff p = g(x), \quad x \in (0, \frac{\pi}{2}), \quad p \in \mathbb{R}^+$$

holds. Then

$$g(x) = \frac{8x^6 + 90x^2 \cos x - 45 \sin^2 x \cos x - 45 x \sin x}{45 x^8}, \quad x \in (0, \frac{\pi}{2}).$$

Note that

$$\varphi_p(x) = (p - g(x)) \frac{x^6}{\cos x}.$$

**Lemma 9.** The function $g(x)$ is strictly decreasing for $x \in (0, \pi/2)$.

*Proof.* Let us notice that the derivative $g'$ is

$$g'(x) = \frac{-360 \cos^3 x - 135x \sin x \cos^2 x - (585x^2 - 360) \cos x - (90x^3 - 360x) \sin x - 16x^6}{45x^9}.$$

It holds

$$g'(x) < 0, \quad x \in (0, \frac{\pi}{2}) \iff f(x) > 0, \quad x \in (0, \frac{\pi}{2}),$$

where

$$f(x) = 360 \cos^3 x + 135x \sin x \cos^2 x + (585x^2 - 360) \cos x + (90x^3 - 360x) \sin x + 16x^6.$$

According to [3], there exists proof that the MTP function $f$ is positive for $x \in (0, \pi/2)$. The proof is given in **Appendix A7**. □
**Statement 4.** Let

$$A = \frac{32\pi^5 - 5760}{45\pi^7} = 0.029670\dots \quad \text{and} \quad B = \frac{4}{105} = 0.038095\dots.$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$x \in (0, \frac{\pi}{2}) \implies \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ \le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}.$$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in (0, x_0^{(p)}) \implies \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}$$

and

$$x \in (x_0^{(p)}, \frac{\pi}{2}) \implies 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in (0, \frac{\pi}{2}) \implies 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\ < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}.$$

*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2^{-}} g(x) \quad \text{and} \quad B = \lim_{x \to 0^{+}} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 9, strictly decreasing on $(0, \pi/2)$.

(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x)) \frac{x^6}{\cos x} < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$x \in (0, \frac{\pi}{2}) \implies \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ \le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}.$$
**Statement 4.** Let

$$A = \frac{32\pi^5 - 5760}{45\pi^7} = 0.029670\dots \quad \text{and} \quad B = \frac{4}{105} = 0.038095\dots.$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ &\le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}. \end{aligned}$$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in (0, x_0^{(p)}) \implies \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}$$

and

$$x \in (x_0^{(p)}, \frac{\pi}{2}) \implies 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}$$

hold.

(iii) If $p \in [B, \infty)$, then

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\ &< \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}. \end{aligned}$$

*Proof.* This statement is based on the results of the paper [1] and the fact that

$$A = \lim_{x \to \pi/2^-} g(x) \quad \text{and} \quad B = \lim_{x \to 0^+} g(x).$$

The function $g(x)$ is continuous and, according to Lemma 9, strictly decreasing on $(0, \pi/2)$.

(i) If $p \in (0, A]$, then

$$g(x) > A \iff (A - g(x)) \frac{x^6}{\cos x} < 0 \iff \varphi_A(x) < 0$$

and, therefore, we can conclude that

$$\begin{aligned} x \in (0, \frac{\pi}{2}) &\implies \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - A x^6 \frac{1}{\cos x} \le \\ &\le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}. \end{aligned}$$
(ii) If $p \in (A, B)$, based on Lemma 9, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$ 
\begin{aligned}
x \in (0, x_0^{(p)}) &\implies g(x) > p \iff \varphi_p(x) < 0 \\
&\iff \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}
\end{aligned}
$$

and

$$ 
\begin{aligned}
x \in (x_0^{(p)}, \frac{\pi}{2}) &\implies g(x) < p \iff \varphi_p(x) > 0 \\
&\iff 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}.
\end{aligned}
$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x)) = \frac{x^6}{\cos x} > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$ 
\begin{aligned}
x \in (0, \frac{\pi}{2}) &\implies 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\
&< \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}.
\end{aligned}
$$

□

Let us notice that $\varphi_B(\pi/2-) = +\infty$. Hence, one of the conditions of Theorem 7 is not satisfied, thus, the minimax approximant is not considered.

Based on the previous considerations, enhancement of Theorem 4 has been obtained in the following form:

**Proposition 4.** For every $0 < x < \pi/2$, the following inequalities hold

$$2 + \left(\frac{8x^4}{45} - \frac{4x^6}{105}\right) \frac{1}{\cos x} < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \left(\frac{8x^4}{45} - \frac{(32\pi^5 - 5760)x^6}{45\pi^7}\right) \frac{1}{\cos x},$$

and the constants $A = \frac{32\pi^5 - 5760}{45\pi^7} = 0.029670...$ and $B = \frac{4}{105} = 0.038095...$ are the best possible.
(ii) If $p \in (A, B)$, based on Lemma 9, the equation

$$g(x) = p$$

has a unique solution $x_0^{(p)}$ and it holds

$$ 
\begin{aligned}
x \in (0, x_0^{(p)}) &\implies g(x) > p \iff \varphi_p(x) < 0 \\
&\iff \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x}
\end{aligned}
$$

and

$$ 
\begin{aligned}
x \in (x_0^{(p)}, \frac{\pi}{2}) &\implies g(x) < p \iff \varphi_p(x) > 0 \\
&\iff 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}.
\end{aligned}
$$

(iii) If $p \in [B, \infty)$, then

$$g(x) < B \iff (B - g(x)) = \frac{x^6}{\cos x} > 0 \iff \varphi_B(x) > 0$$

and, therefore, we can conclude that

$$ 
\begin{aligned}
x \in (0, \frac{\pi}{2}) &\implies 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - p x^6 \frac{1}{\cos x} \le 2 + \frac{8}{45} x^4 \frac{1}{\cos x} - B x^6 \frac{1}{\cos x} \\
&< \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x}.
\end{aligned}
$$

□

Let us notice that $\varphi_B(\pi/2-) = +\infty$. Hence, one of the conditions of Theorem 7 is not satisfied, thus, the minimax approximant is not considered.

Based on the previous considerations, enhancement of Theorem 4 has been obtained in the following form:

**Proposition 4.** For every $0 < x < \pi/2$, the following inequalities hold

$$2 + \left(\frac{8x^4}{45} - \frac{4x^6}{105}\right) \frac{1}{\cos x} < \left(\frac{\sin x}{x}\right)^2 + \frac{\tan x}{x} < 2 + \left(\frac{8x^4}{45} - \frac{(32\pi^5 - 5760)x^6}{45\pi^7}\right) \frac{1}{\cos x},$$

and the constants $A = \frac{32\pi^5 - 5760}{45\pi^7} = 0.029670...$ and $B = \frac{4}{105} = 0.038095...$ are the best possible.
Analogously to Statement 1 and Statement 2, the following statements can be proved:

**Improvement of Theorem 5**

**Lemma 10.** *The family of functions*

$$ \varphi_p(x) = \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} - 2 - p x^4 \quad (\text{for } x \in \left(0, \frac{\pi}{2}\right)) $$

is decreasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

**Statement 5.** Let

$$ A = \frac{2}{45} = 0.044444\dots \quad \text{and} \quad B = \frac{4\pi^2 - 32}{\pi^4} = 0.076773\dots. $$

Then, it holds:

(i) If $p \in (0, A]$, then

$$ x \in \left(0, \frac{\pi}{2}\right) \Rightarrow 2 + px^4 \le 2 + Ax^4 < \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x}. $$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$ x \in \left(0, x_0^{(p)}\right) \Rightarrow \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} < 2 + px^4 $$

and

$$ x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \Rightarrow 2 + px^4 < \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} $$

hold.

(iii) If $p \in [B, \infty)$, then

$$ x \in \left(0, \frac{\pi}{2}\right) \Rightarrow \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} < 2 + Bx^4 \le 2 + px^4. $$

(iv) There is exactly one solution to the following equation

$$ \left|\varphi_p(t^{(p)})\right| = \varphi_p\left(\frac{\pi}{2}-\right), $$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$ p_0 = 0.072425\dots. $$

For the value

$$ d_0 = \left|\varphi_{p_0}(t^{(p_0)})\right| = \varphi_{p_0}\left(\frac{\pi}{2}-\right) = 0.026471\dots, $$
Analogously to Statement 1 and Statement 2, the following statements can be proved:

**Improvement of Theorem 5**

**Lemma 10.** *The family of functions*

$$ \varphi_p(x) = \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} - 2 - p x^4 \quad (\text{for } x \in \left(0, \frac{\pi}{2}\right)) $$

is decreasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

**Statement 5.** Let

$$ A = \frac{2}{45} = 0.044444\dots \quad \text{and} \quad B = \frac{4\pi^2 - 32}{\pi^4} = 0.076773\dots. $$

Then, it holds:

(i) If $p \in (0, A]$, then

$$ x \in \left(0, \frac{\pi}{2}\right) \implies 2 + px^4 \le 2 + Ax^4 < \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x}. $$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$ x \in \left(0, x_0^{(p)}\right) \implies \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} < 2 + px^4 $$

and

$$ x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \implies 2 + px^4 < \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x}. $$

hold.

(iii) If $p \in [B, \infty)$, then

$$ x \in \left(0, \frac{\pi}{2}\right) \implies \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} < 2 + Bx^4 \le 2 + px^4. $$

(iv) There is exactly one solution to the following equation

$$ \left|\varphi_p(t^{(p)})\right| = \varphi_p\left(\frac{\pi}{2}-\right), $$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$ p_0 = 0.072425\dots. $$

For the value

$$ d_0 = \left|\varphi_{p_0}(t^{(p_0)})\right| = \varphi_{p_0}\left(\frac{\pi}{2}-\right) = 0.026471\dots, $$
the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.072425...$, the minimax approximant of the family is determined as

$$\varphi_{p_0}(x) = \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} - 2 - 0.072425... x^4$$

and it determines the corresponding minimax approximation

$$\left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} \approx 2 + 0.072425... x^4.$$

Based on the previous considerations, enhancement of Theorem 5 has been obtained in the following form:

**Proposition 5.** For every $0 < x < \pi/2$, the following inequalities hold

$$2 + \frac{2}{45} x^4 < \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} < 2 + \frac{4\pi^2 - 32}{\pi^4} x^4,$$

and the constants $A = \frac{2}{45} = 0.044444...$ and $B = \frac{4\pi^2 - 32}{\pi^4} = 0.076773...$ are the best possible.

## Improvement of Theorem 6

**Lemma 11.** The family of functions

$$\varphi_p(x) = 3 \frac{x}{\sin x} + \cos x - 4 - \frac{1}{10} x^4 - p x^6 \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is decreasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

**Statement 6.** Let

$$A = \frac{1}{210} = 0.0047619... \quad \text{and} \quad B = \frac{480\pi - 2\pi^4 - 1280}{5\pi^6} = 0.0068954...$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$x \in (0, \frac{\pi}{2}) \implies 4 + \frac{1}{10}x^4 + px^6 \le 4 + \frac{1}{10}x^4 + Ax^6 < 3 \frac{x}{\sin x} + \cos x.$$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in (0, x_0^{(p)}) \implies 3 \frac{x}{\sin x} + \cos x < 4 + \frac{1}{10} x^4 + px^6$$
the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.072425...$, the minimax approximant of the family is determined as

$$\varphi_{p_0}(x) = \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} - 2 - 0.072425... x^4$$

and it determines the corresponding minimax approximation

$$\left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} \approx 2 + 0.072425... x^4.$$

Based on the previous considerations, enhancement of Theorem 5 has been obtained in the following form:

**Proposition 5.** For every $0 < x < \pi/2$, the following inequalities hold

$$2 + \frac{2}{45} x^4 < \left(\frac{x}{\sin x}\right)^2 + \frac{x}{\tan x} < 2 + \frac{4\pi^2 - 32}{\pi^4} x^4,$$

and the constants $A = \frac{2}{45} = 0.044444...$ and $B = \frac{4\pi^2 - 32}{\pi^4} = 0.076773...$ are the best possible.

## Improvement of Theorem 6

**Lemma 11.** The family of functions

$$\varphi_p(x) = 3 \frac{x}{\sin x} + \cos x - 4 - \frac{1}{10} x^4 - p x^6 \quad (\text{for } x \in (0, \frac{\pi}{2}))$$

is decreasingly stratified with respect to parameter $p \in \mathbb{R}^+$.

**Statement 6.** Let

$$A = \frac{1}{210} = 0.0047619... \quad \text{and} \quad B = \frac{480\pi - 2\pi^4 - 1280}{5\pi^6} = 0.0068954...$$

Then, it holds:

(i) If $p \in (0, A]$, then

$$x \in (0, \frac{\pi}{2}) \implies 4 + \frac{1}{10}x^4 + px^6 \le 4 + \frac{1}{10}x^4 + Ax^6 < 3 \frac{x}{\sin x} + \cos x.$$

(ii) If $p \in (A, B)$, then $\varphi_p(x)$ has exactly one zero $x_0^{(p)}$ on $(0, \pi/2)$. Also,

$$x \in (0, x_0^{(p)}) \implies 3 \frac{x}{\sin x} + \cos x < 4 + \frac{1}{10} x^4 + px^6$$
and

$$x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \Longrightarrow 4 + \frac{1}{10}x^4 + px^6 < 3 \frac{x}{\sin x} + \cos x$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow 3 \frac{x}{\sin x} + \cos x < 4 + \frac{1}{10}x^4 + Bx^6 \le 4 + \frac{1}{10}x^4 + px^6.$$

(iv) There is exactly one solution to the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p\left(\frac{\pi}{2}\right),$$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$p_0 = 0.0066982...$$

For the value

$$d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}\left(\frac{\pi}{2}\right) = 0.0029637...,$$

the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.0066982...$, the minimax approximant of the family is determined as

$$\varphi_{p_0}(x) = 3 \frac{x}{\sin x} + \cos x - 4 - \frac{1}{10}x^4 - 0.0066982...x^6$$

and it determines the corresponding minimax approximation

$$3 \frac{x}{\sin x} + \cos x \approx 4 + \frac{1}{10}x^4 + 0.0066982...x^6.$$

Based on the previous considerations, enhancement of Theorem 6 has been obtained in the following form:

**Proposition 6.** For every $0 < x < \pi/2$, the following inequalities hold

$$4 + \frac{1}{10}x^4 + \frac{1}{210}x^6 < 3 \frac{x}{\sin x} + \cos x < 4 + \frac{1}{10}x^4 + \frac{480\pi - 2\pi^4 - 1280}{5\pi^6} x^6,$$

and the constants $A = \frac{1}{210} = 0.0047619...$ and $B = \frac{480\pi - 2\pi^4 - 1280}{5\pi^6} = 0.0068954...$ are the best possible.

The existence of minimax approximant in Statement 5 and Statement 6 is a consequence of Theorem 7' and Theorem 8.
and

$$x \in \left(x_0^{(p)}, \frac{\pi}{2}\right) \Longrightarrow 4 + \frac{1}{10}x^4 + px^6 < 3 \frac{x}{\sin x} + \cos x$$

hold.

(iii) If $p \in [B, \infty)$, then

$$x \in \left(0, \frac{\pi}{2}\right) \Longrightarrow 3 \frac{x}{\sin x} + \cos x < 4 + \frac{1}{10}x^4 + Bx^6 \le 4 + \frac{1}{10}x^4 + px^6.$$

(iv) There is exactly one solution to the following equation

$$|\varphi_p(t^{(p)})| = \varphi_p\left(\frac{\pi}{2}\right),$$

where $t^{(p)}$ is a minimum of $\varphi_p(x)$ on $(0, \pi/2)$, with respect to parameter $p \in (A, B)$, which is numerically determined as

$$p_0 = 0.0066982...$$

For the value

$$d_0 = |\varphi_{p_0}(t^{(p_0)})| = \varphi_{p_0}\left(\frac{\pi}{2}\right) = 0.0029637...,$$

the following holds

$$d_0 = \inf_{p \in \mathbb{R}^+} \sup_{x \in (0, \pi/2)} |\varphi_p(x)|.$$

(v) For the value $p_0 = 0.0066982...$, the minimax approximant of the family is determined as

$$\varphi_{p_0}(x) = 3 \frac{x}{\sin x} + \cos x - 4 - \frac{1}{10}x^4 - 0.0066982...x^6$$

and it determines the corresponding minimax approximation

$$3 \frac{x}{\sin x} + \cos x \approx 4 + \frac{1}{10}x^4 + 0.0066982...x^6.$$

Based on the previous considerations, enhancement of Theorem 6 has been obtained in the following form:

**Proposition 6.** For every $0 < x < \pi/2$, the following inequalities hold

$$4 + \frac{1}{10}x^4 + \frac{1}{210}x^6 < 3 \frac{x}{\sin x} + \cos x < 4 + \frac{1}{10}x^4 + \frac{480\pi - 2\pi^4 - 1280}{5\pi^6} x^6,$$

and the constants $A = \frac{1}{210} = 0.0047619...$ and $B = \frac{480\pi - 2\pi^4 - 1280}{5\pi^6} = 0.0068954...$ are the best possible.

The existence of minimax approximant in Statement 5 and Statement 6 is a consequence of Theorem 7' and Theorem 8.
# 4. CONCLUSION

This paper specifies the results of C. Mortici [1] using the method described in [2]. The mentioned method could be applied for possible improvements of existing results from the Theory of analytic inequalities [12], [13], [28] in terms of determining the corresponding minimax approximants for various inequalities. In the previous section, examples of minimax approximations are presented where they exist. It is important to note that through minimax approximants, the error in approximations is minimized in the considered sense.

The main aim of this paper is to promote SimTheP, an automated theorem prover for MTP inequalities, developed through the doctoral dissertation [15]. All the essential proofs of MTP inequalities in this paper are given in the Appendix and derived using the prover SimTheP. For any given MTP inequality $f(x) > 0$, for $x \in \mathbb{S} \subseteq [0, \pi/2]$, SimTheP provides a structured proof divided into parts I-IV. Each part is designed to allow manual step-by-step verification, demonstrating SimTheP's capability to replicate the human way of proving inequalities.

Many results within the Theory of analytic inequalities, for example, results from [2], [3], [6]-[8], [10]-[13], [18], [24], [26]-[75], could be proved using the prover SimTheP, see the link https://simthep.etf.bg.ac.rs/.

It is crucial to highlight that through Statements 1–6, all Theorems 1–6 have been improved and minimax approximations have been determined wherever feasible. As a result, Propositions 1–6 were obtained, where for the inequalities considered in Theorems 1–6, the best possible constants were identified. Such an approach to Theorems 1–6 was enabled by the utilization of the concept of stratification. Moreover, this paper presents the first paper in which the automated theorem prover SimTheP was utilized to deliver proofs for the MTP inequalities, marking a significant advancement in the field.

## Acknowledgments.

The authors are greatly indebted to Dr. Ivana Jovović for numerous stimulating conversations about the concept of stratification. Her assistance in applying MTP inequalities to various problems, coupled with her ongoing and steadfast commitment to supporting our endeavors, has been instrumental and is deeply appreciated. Special appreciation is also extended to Dr. Marija Nenezić Jović for her invaluable comments that greatly enhanced certain proofs. The authors also express their gratitude to the referees for their thorough reading of the paper and their valuable suggestions and comments.

This work was financially supported by the Ministry of Science, Technological Development and Innovation of the Republic of Serbia under contract numbers: 451-03-65/2024-03/200156 (for the first author), 451-03-65/2024-03/200103 (for the second, fourth and fifth authors) and 451-03-66/2024-03/200103 (for the third author). The research of the first author has also been supported by the Faculty of Technical Sciences, University of Novi Sad through project "Improving the teaching process in the English language in fundamental disciplines" (No. 01-3394/1).
## 4. CONCLUSION

This paper specifies the results of C. Mortici [1] using the method described in [2]. The mentioned method could be applied for possible improvements of existing results from the Theory of analytic inequalities [12], [13], [28] in terms of determining the corresponding minimax approximants for various inequalities. In the previous section, examples of minimax approximations are presented where they exist. It is important to note that through minimax approximants, the error in approximations is minimized in the considered sense.

The main aim of this paper is to promote SimTheP, an automated theorem prover for MTP inequalities, developed through the doctoral dissertation [15]. All the essential proofs of MTP inequalities in this paper are given in the Appendix and derived using the prover SimTheP. For any given MTP inequality $f(x) > 0$, for $x \in \mathbb{S} \subseteq [0, \pi/2]$, SimTheP provides a structured proof divided into parts I-IV. Each part is designed to allow manual step-by-step verification, demonstrating SimTheP's capability to replicate the human way of proving inequalities.

Many results within the Theory of analytic inequalities, for example, results from [2], [3], [6]-[8], [10]-[13], [18], [24], [26]-[75], could be proved using the prover SimTheP, see the link https://simthep.etf.bg.ac.rs/.

It is crucial to highlight that through Statements 1–6, all Theorems 1–6 have been improved and minimax approximations have been determined wherever feasible. As a result, Propositions 1–6 were obtained, where for the inequalities considered in Theorems 1–6, the best possible constants were identified. Such an approach to Theorems 1–6 was enabled by the utilization of the concept of stratification. Moreover, this paper presents the first paper in which the automated theorem prover SimTheP was utilized to deliver proofs for the MTP inequalities, marking a significant advancement in the field.

## Acknowledgments.

The authors are greatly indebted to Dr. Ivana Jovović for numerous stimulating conversations about the concept of stratification. Her assistance in applying MTP inequalities to various problems, coupled with her ongoing and steadfast commitment to supporting our endeavors, has been instrumental and is deeply appreciated. Special appreciation is also extended to Dr. Marija Nenezić Jović for her invaluable comments that greatly enhanced certain proofs. The authors also express their gratitude to the referees for their thorough reading of the paper and their valuable suggestions and comments.

This work was financially supported by the Ministry of Science, Technological Development and Innovation of the Republic of Serbia under contract numbers: 451-03-65/2024-03/200156 (for the first author), 451-03-65/2024-03/200103 (for the second, fourth and fifth authors) and 451-03-66/2024-03/200103 (for the third author). The research of the first author has also been supported by the Faculty of Technical Sciences, University of Novi Sad through project "Improving the teaching process in the English language in fundamental disciplines" (No. 01-3394/1).
## REFERENCES

1. C. MORTICI: *The natural approach of Wilker-Cusa-Huygens inequalities*, Math. Inequal. Appl. **14**:3 (2011), 535-541.

2. B. MALEŠEVIĆ, B. MIHAILOVIĆ: *A Minimax Approximant in the Theory of Analytical Inequalities*, Appl. Anal. Discrete Math. **15**:2 (2021), 486-509.

3. B. MALEŠEVIĆ, M. MAKRAGIĆ: *A Method for Proving Some Inequalities on Mixed Trigonometric Polynomial Functions*, J. Math. Inequal. **10**:3 (2016), 849-876.

4. B. MALEŠEVIĆ, T. LUTOVAC, B. BANJAC: *One Method for Proving Some Classes of Exponential Analytical Inequalities*, Filomat **32**:20 (2018), 6921-6925.

5. B. MALEŠEVIĆ, M. MIĆOVIĆ: *Exponential Polynomials and Stratification in the Theory of Analytic Inequalities*, Journal of Science and Arts **23**:3 (2023), 659-670.

6. M. MIĆOVIĆ, B. MALEŠEVIĆ: *Jordan-Type Inequalities and Stratification*, Axioms **13**:4, 262 (2024), 1-25.

7. B. MALEŠEVIĆ, D. JOVANOVIĆ: *Frame's Types of Inequalities and Stratification*, Cubo. **26**:1 (2024), 1-19.

8. B. MALEŠEVIĆ, B. MIHAILOVIĆ, M. NENEZIĆ JOVIĆ, L. MILINKOVIĆ: *Some minimax approximants of D'Aurizio trigonometric inequalities*, HAL (Preprint) (2022), 1-9, hal-03550277.

9. B. YU, B. DONG: *A Hybrid Polynomial System Solving Method for Mixed Trigonometric Polynomial Systems*, SIAM J. Numer. Anal. **46**:3 (2008) 1503-1518.

10. S. CHEN, Z. LIU: *Automated proving of trigonometric function inequalities using Taylor expansion*, Journal of Systems Science and Mathematical Sciences **36**:8 (2016), 1339-1348. (in Chinese)

11. S. CHEN, Z. LIU: *Automated proof of mixed trigonometric-polynomial inequalities*, J. Symbolic Comput. **101** (2020), 318-329.

12. D. S. MITRINOVIĆ: *Analytic inequalities*, Springer-Verlag, 1970.

13. G. MILOVANOVIĆ, M. RASSIAS (EDITORS): *Analytic Number Theory, Approximation Theory and Special functions*, Springer 2014, Chapter: G.D. Anderson, M. Vuorinen, X. Zhang: *Topics in Special Functions III*, 297-345.

14. M. MAKRAGIĆ: *On trigonometric polynomial ring with applications in the theory of analytic inequalities*, Faculty of Mathematics, Belgrade 2018, Ph.D. thesis in Serbian, see link of National Repository of Dissertations in Serbia https://nardus.mpn.gov.rs/ and mathgenealogy link https://www.mathgenealogy.org/id.php?id=239436

15. B. BANJAC: *System for automatic proving of some classes of analytic inequalities*, School of Electrical Engineering, Belgrade 2019, Ph.D. thesis in Serbian, see link of National Repository of Dissertations in Serbia https://nardus.mpn.gov.rs/ and math-genealogy link https://www.mathgenealogy.org/id.php?id=248798

16. M. NENEZIĆ JOVIĆ: *Stratified Families of Functions in the Theory of Analytical Inequalities With Applications*, School of Electrical Engineering, Belgrade 2023, Ph.D. thesis in Serbian, see link of National Repository of Dissertations in Serbia https://nardus.mpn.gov.rs/ and mathgenealogy link https://www.mathgenealogy.org/id.php?id=307785
REFERENCES

1. C. MORTICI: *The natural approach of Wilker-Cusa-Huygens inequalities*, Math. In-
equal. Appl. **14**:3 (2011), 535–541.

2. B. MALEŠEVIĆ, B. MIHAILOVIĆ: *A Minimax Approximant in the Theory of Analytical Inequalities*, Appl. Anal. Discrete Math. **15**:2 (2021), 486–509.

3. B. MALEŠEVIĆ, M. MAKRAGIĆ: *A Method for Proving Some Inequalities on Mixed Trigonometric Polynomial Functions*, J. Math. Inequal. **10**:3 (2016), 849–876.

4. B. MALEŠEVIĆ, T. LUTOVAC, B. BANJAC: *One Method for Proving Some Classes of Exponential Analytical Inequalities*, Filomat **32**:20 (2018), 6921–6925.

5. B. MALEŠEVIĆ, M. MIĆOVIĆ: *Exponential Polynomials and Stratification in the Theory of Analytic Inequalities*, Journal of Science and Arts **23**:3 (2023), 659–670.

6. M. MIĆOVIĆ, B. MALEŠEVIĆ: *Jordan-Type Inequalities and Stratification*, Axioms **13**:4, 262 (2024), 1–25.

7. B. MALEŠEVIĆ, D. JOVANOVIĆ: *Frame's Types of Inequalities and Stratification*, Cubo. **26**:1 (2024), 1–19.

8. B. MALEŠEVIĆ, B. MIHAILOVIĆ, M. NENEZIĆ JOVIĆ, L. MILINKOVIĆ: *Some minimax approximants of D'Aurizio trigonometric inequalities*, HAL (Preprint) (2022), 1–9, hal-03550277.

9. B. YU, B. DONG: *A Hybrid Polynomial System Solving Method for Mixed Trigonometric Polynomial Systems*, SIAM J. Numer. Anal. **46**:3 (2008) 1503–1518.

10. S. CHEN, Z. LIU: *Automated proving of trigonometric function inequalities using Taylor expansion*, Journal of Systems Science and Mathematical Sciences **36**:8 (2016), 1339-1348. (in Chinese)

11. S. CHEN, Z. LIU: *Automated proof of mixed trigonometric-polynomial inequalities*, J. Symbolic Comput. **101** (2020), 318-329.

12. D. S. MITRINOVIĆ: *Analytic inequalities*, Springer-Verlag, 1970.

13. G. MILOVANOVIĆ, M. RASSIAS (EDITORS): *Analytic Number Theory, Approximation Theory and Special functions*, Springer 2014, Chapter: G.D. Anderson, M. Vuorinen, X. Zhang: *Topics in Special Functions III*, 297–345.

14. M. MAKRAGIĆ: *On trigonometric polynomial ring with applications in the theory of analytic inequalities*, Faculty of Mathematics, Belgrade 2018, Ph.D. thesis in Serbian, see link of National Repository of Dissertations in Serbia https://nardus.mpn.gov.rs/ and mathgenealogy link https://www.mathgenealogy.org/id.php?id=239436

15. B. BANJAC: *System for automatic proving of some classes of analytic inequalities*, School of Electrical Engineering, Belgrade 2019, Ph.D. thesis in Serbian, see link of National Repository of Dissertations in Serbia https://nardus.mpn.gov.rs/ and math-genealogy link https://www.mathgenealogy.org/id.php?id=248798

16. M. NENEZIĆ JOVIĆ: *Stratified Families of Functions in the Theory of Analytical Inequalities With Applications*, School of Electrical Engineering, Belgrade 2023, Ph.D. thesis in Serbian, see link of National Repository of Dissertations in Serbia https://nardus.mpn.gov.rs/ and mathgenealogy link https://www.mathgenealogy.org/id.php?id=307785
17. B. MALEŠEVIĆ: *One Method for Proving Inequalities by Computer*, J. Inequal. Appl. **2007** (2007), 1–8.

18. B. BANJAC, M. MAKRAGIĆ, B. MALEŠEVIĆ: *Some Notes on a Method for Proving Inequalities by Computer*, Results. Math. **69** (2016), 161–176.

19. B. MALEŠEVIĆ, B. BANJAC: *Automated Proving Mixed Trigonometric Polynomial Inequalities*, Proceedings of 27th TELFOR conference, Serbia, Belgrade, November 26-27, 2019.

20. B. MALEŠEVIĆ, B. BANJAC: *One method for proving polynomial inequalities with real coefficients*, Proceedings of 28th TELFOR conference, Serbia, Belgrade, November 24-25, 2020.

21. N. CUTLAND: *Computability - an introduction to recursive function theory*, Cambridge University Press 1980.

22. J.C.F. STURM: *Mémoire sur la résolution des équations numériques*, Bulletin des Sciences de Ferussac **11** (1829), 419–425.

23. B. MALEŠEVIĆ, B. BANJAC, V. ŠEŠUM ČAVIĆ, N. KOROLIJA: *One algorithm for testing annulling of mixed trigonometric polynomial functions on boundary points*, Proceedings of 30th TELFOR conference, Serbia, Belgrade, November 15-16, 2022.

24. H. ALZER, M. K. KWONG: *A refinement of Vietoris' inequality for cosine polynomials*, Anal. Appl. (Singap.) **14**:5 (2016), 615–629.

25. H. ALZER, M. K. KWONG: *On Fejér's inequalities for the Legendre polynomials*, Math. Nachr. **290**:17-18 (2017), 2740–2754.

26. H. ALZER, M. K. KWONG: *On two trigonometric inequalities of Askey and Steinig*, New York J. Math. **26** (2020), 28–36.

27. H. ALZER, M. K. KWONG: *Inequalities for trigonometric sums*, J. Anal. (2024)

28. M. J. CLOUD, B. C. DRACHMAN, L. P. LEBEDEV: *Inequalities with Applications to Engineering*, Springer 2014.

29. S. CHEN, X. GE: *A solution to an open problem for Wilker-type inequalities*, J. Math. Inequal. **15**:1 (2021), 59–65.

30. F. Qi, D.-W. Ni, B.-N. Guo: *Refinements, Generalizations, and Applications of Jordan's Inequality and Related Problems*, J. Inequal. Appl. **2009** (2009), 1–52.

31. B. A. BHAYO, J. SÁNDOR: *On classical inequalities of trigonometric and hyperbolic functions*, arXiv (Preprint) (2014), 1-59, arXiv:1405.0934.

32. M. NENEZIĆ, B. MALEŠEVIĆ, C. MORTICI: *New approximations of some expressions involving trigonometric functions*, Appl. Math. Comput. **283** (2016), 299–315.

33. B. MALEŠEVIĆ, M. NENEZIĆ, L. ZHU, B. BANJAC, M. PETROVIĆ: *Some new estimates of precision of Cusa-Huygens and Huygens approximations*, Appl. Anal. Discrete Math. **15**:1 (2021), 243–259.

34. L. ZHU, M. NENEZIĆ: *New approximation inequalities for circular functions*, J. Inequal. Appl. **2018**:313 (2018), 1–12.

35. B. MALEŠEVIĆ, B. BANJAC, I. JOVOVIĆ: *A proof of two conjectures of Chao-Ping Chen for inverse trigonometric functions*, J. Math. Inequal. **11**:1 (2017), 151–162.

36. B. MALEŠEVIĆ, T. LUTOVAC, B. BANJAC: *A proof of an open problem of Yusuke Nishizawa for a power-exponential function*, J. Math. Inequal. **12**:2 (2018), 473–485.
17. B. MALEŠEVIĆ: *One Method for Proving Inequalities by Computer*, J. Inequal. Appl. **2007** (2007), 1–8.

18. B. BANJAC, M. MAKRAGIĆ, B. MALEŠEVIĆ: *Some Notes on a Method for Proving Inequalities by Computer*, Results. Math. **69** (2016), 161–176.

19. B. MALEŠEVIĆ, B. BANJAC: *Automated Proving Mixed Trigonometric Polynomial Inequalities*, Proceedings of 27th TELFOR conference, Serbia, Belgrade, November 26-27, 2019.

20. B. MALEŠEVIĆ, B. BANJAC: *One method for proving polynomial inequalities with real coefficients*, Proceedings of 28th TELFOR conference, Serbia, Belgrade, November 24-25, 2020.

21. N. CUTLAND: *Computability - an introduction to recursive function theory*, Cambridge University Press 1980.

22. J.C.F. STURM: *Mémoire sur la résolution des équations numériques*, Bulletin des Sciences de Ferussac **11** (1829), 419–425.

23. B. MALEŠEVIĆ, B. BANJAC, V. ŠEŠUM ČAVIĆ, N. KOROLIJA: *One algorithm for testing annulling of mixed trigonometric polynomial functions on boundary points*, Proceedings of 30th TELFOR conference, Serbia, Belgrade, November 15-16, 2022.

24. H. ALZER, M. K. KWONG: *A refinement of Vietoris' inequality for cosine polynomials*, Anal. Appl. (Singap.) **14**:5 (2016), 615–629.

25. H. ALZER, M. K. KWONG: *On Fejér's inequalities for the Legendre polynomials*, Math. Nachr. **290**:17-18 (2017), 2740–2754.

26. H. ALZER, M. K. KWONG: *On two trigonometric inequalities of Askey and Steinig*, New York J. Math. **26** (2020), 28–36.

27. H. ALZER, M. K. KWONG: *Inequalities for trigonometric sums*, J. Anal. (2024)

28. M. J. CLOUD, B. C. DRACHMAN, L. P. LEBEDEV: *Inequalities with Applications to Engineering*, Springer 2014.

29. S. CHEN, X. GE: *A solution to an open problem for Wilker-type inequalities*, J. Math. Inequal. **15**:1 (2021), 59–65.

30. F. Qi, D.-W. Ni, B.-N. Guo: *Refinements, Generalizations, and Applications of Jordan's Inequality and Related Problems*, J. Inequal. Appl. **2009** (2009), 1–52.

31. B. A. BHAYO, J. SÁNDOR: *On classical inequalities of trigonometric and hyperbolic functions*, arXiv (Preprint) (2014), 1-59, arXiv:1405.0934.

32. M. NENEZIĆ, B. MALEŠEVIĆ, C. MORTICI: *New approximations of some expressions involving trigonometric functions*, Appl. Math. Comput. **283** (2016), 299–315.

33. B. MALEŠEVIĆ, M. NENEZIĆ, L. ZHU, B. BANJAC, M. PETROVIĆ: *Some new estimates of precision of Cusa-Huygens and Huygens approximations*, Appl. Anal. Discrete Math. **15**:1 (2021), 243–259.

34. L. ZHU, M. NENEZIĆ: *New approximation inequalities for circular functions*, J. Inequal. Appl. **2018**:313 (2018), 1–12.

35. B. MALEŠEVIĆ, B. BANJAC, I. JOVOVIĆ: *A proof of two conjectures of Chao-Ping Chen for inverse trigonometric functions*, J. Math. Inequal. **11**:1 (2017), 151–162.

36. B. MALEŠEVIĆ, T. LUTOVAC, B. BANJAC: *A proof of an open problem of Yusuke Nishizawa for a power-exponential function*, J. Math. Inequal. **12**:2 (2018), 473–485.
37. T. LUTOVAC, B. MALEŠEVIĆ, C. MORTICI: *The natural algorithmic approach of mixed trigonometric-polynomial problems*, J. Inequal. Appl. **2017**:116 (2017), 1–16.

38. B. MALEŠEVIĆ, T. LUTOVAC, M. RAŠAJSKI, C. MORTICI: *Extensions of the natural approach to refinements and generalizations of some trigonometric inequalities*, Adv. Difference Equ. **2018**:90 (2018), 1–15.

39. C.-P. CHEN, B. MALEŠEVIĆ: *Sharp inequalities related to the Adamović-Mitrinović, Cusa, Wilker and Huygens results*, Filomat **37**:19 (2023), 6319–6334.

40. Y. J. BAGUL, B. BANJAC, C. CHESNEAU, M. KOSTIĆ, B. MALEŠEVIĆ: *New Refinements of Cusa-Huygens Inequality*, Results Math. **76**:107 (2021), 1–16.

41. L. ZHU, B. MALEŠEVIĆ: *New inequalities of Huygens-type involving tangent and sine functions*, Hacet. J. Math. Stat. **52**:1 (2023), 36–61.

42. Y. J. BAGUL, C. CHESNEAU, M. KOSTIĆ: *On the Cusa-Huygens inequality*, Rev. R. Acad. Cienc. Exactas Fís. Nat. Ser. A Math. RACSAM. **115**:29 (2021), 1–12.

43. A. R. CHOUIKHA: *New sharp inequalities related to classical trigonometric inequalities*, J. Inequal. Spec. Funct. **11**:4 (2020), 27–35.

44. A. R. CHOUIKHA: *Sharp inequalities related to Wilker results*, Open Journal of Mathematical Sciences **7**:1 (2023), 19–34.

45. A. R. CHOUIKHA: *On natural approaches related to classical trigonometric inequalities*, Open Journal of Mathematical Sciences **7**:1 (2023), 299–320.

46. A. R. CHOUIKHA, C. CHESNEAU: *Contributions to trigonometric 1-parameter inequalities*, HAL (Preprint) (2024), 1–21, hal-04500965.

47. A. R. CHOUIKHA: *On the 1-parameter trigonometric and hyperbolic inequalities chains*, HAL (Preprint) (2024), 1–13, hal-04435124.

48. A. R. CHOUIKHA: *Other approaches related to Huygens trigonometric inequalities*, HAL (Preprint) (2022), 1–15, hal-03769843.

49. A. R. CHOUIKHA, C. CHESNEAU, Y. J. BAGUL: *Some refinements of well-known inequalities involving trigonometric functions*, J. Ramanujan Math. Soc. **36**:3 (2021), 193–202.

50. Y. HU, C. MORTICI: *A Lower Bound on the Sinc Function and Its Application*, The Scientific World Journal **2014** (2014), 1–4.

51. L. DEBNATH, C. MORTICI, L. ZHU: *Refinements of Jordan-Stečkin and Becker-Stark Inequalities*, Results Math. **67** (2015), 207–215.

52. R. SHINDE, C. CHESNEAU, N. DARKUNDE, S. GHODECHOR, A. LAGAD: *Revisit of an Improved Wilker Type Inequality*, Pan-American Journal of Mathematics **2** (2023), 1-17.

53. Y. J. BAGUL, C. CHESNEAU: *Refined forms of Oppenheim and Cusa-Huygens type inequalities*, Acta Comment. Univ. Tartu. Math. **24**:2 (2020), 183–194.

54. Y. J. BAGUL, C. CHESNEAU, M. KOSTIĆ: *The Cusa-Huygens inequality revisited*, Novi Sad J. Math. **50**:2 (2020), 149–159.

55. Y. J. BAGUL, C. CHESNEAU: *Generalized bounds for sine and cosine functions*, Asian-Eur. J. Math. **15**:1 (2022), 1–16.

56. R. M. DHAIGUDE, C. CHESNEAU, Y. J. BAGUL: *About Trigonometric-polynomial Bounds of Sinc Function*, Math. Sci. Appl. E-Notes. **8**:1 (2020), 100–104.
37. T. LUTOVAC, B. MALEŠEVIĆ, C. MORTICI: *The natural algorithmic approach of mixed trigonometric-polynomial problems*, J. Inequal. Appl. **2017**:116 (2017), 1–16.

38. B. MALEŠEVIĆ, T. LUTOVAC, M. RAŠAJSKI, C. MORTICI: *Extensions of the natural approach to refinements and generalizations of some trigonometric inequalities*, Adv. Difference Equ. **2018**:90 (2018), 1–15.

39. C.-P. CHEN, B. MALEŠEVIĆ: *Sharp inequalities related to the Adamović-Mitrinović, Cusa, Wilker and Huygens results*, Filomat **37**:19 (2023), 6319–6334.

40. Y. J. BAGUL, B. BANJAC, C. CHESNEAU, M. KOSTIĆ, B. MALEŠEVIĆ: *New Refinements of Cusa-Huygens Inequality*, Results Math. **76**:107 (2021), 1–16.

41. L. ZHU, B. MALEŠEVIĆ: *New inequalities of Huygens-type involving tangent and sine functions*, Hacet. J. Math. Stat. **52**:1 (2023), 36–61.

42. Y. J. BAGUL, C. CHESNEAU, M. KOSTIĆ: *On the Cusa-Huygens inequality*, Rev. R. Acad. Cienc. Exactas Fís. Nat. Ser. A Math. RACSAM. **115**:29 (2021), 1–12.

43. A. R. CHOUIKHA: *New sharp inequalities related to classical trigonometric inequalities*, J. Inequal. Spec. Funct. **11**:4 (2020), 27–35.

44. A. R. CHOUIKHA: *Sharp inequalities related to Wilker results*, Open Journal of Mathematical Sciences **7**:1 (2023), 19–34.

45. A. R. CHOUIKHA: *On natural approaches related to classical trigonometric inequalities*, Open Journal of Mathematical Sciences **7**:1 (2023), 299–320.

46. A. R. CHOUIKHA, C. CHESNEAU: *Contributions to trigonometric 1-parameter inequalities*, HAL (Preprint) (2024), 1–21, hal-04500965.

47. A. R. CHOUIKHA: *On the 1-parameter trigonometric and hyperbolic inequalities chains*, HAL (Preprint) (2024), 1–13, hal-04435124.

48. A. R. CHOUIKHA: *Other approaches related to Huygens trigonometric inequalities*, HAL (Preprint) (2022), 1–15, hal-03769843.

49. A. R. CHOUIKHA, C. CHESNEAU, Y. J. BAGUL: *Some refinements of well-known inequalities involving trigonometric functions*, J. Ramanujan Math. Soc. **36**:3 (2021), 193–202.

50. Y. HU, C. MORTICI: *A Lower Bound on the Sinc Function and Its Application*, The Scientific World Journal **2014** (2014), 1–4.

51. L. DEBNATH, C. MORTICI, L. ZHU: *Refinements of Jordan-Stečkin and Becker-Stark Inequalities*, Results Math. **67** (2015), 207–215.

52. R. SHINDE, C. CHESNEAU, N. DARKUNDE, S. GHODECHOR, A. LAGAD: *Revisit of an Improved Wilker Type Inequality*, Pan-American Journal of Mathematics **2** (2023), 1-17.

53. Y. J. BAGUL, C. CHESNEAU: *Refined forms of Oppenheim and Cusa-Huygens type inequalities*, Acta Comment. Univ. Tartu. Math. **24**:2 (2020), 183–194.

54. Y. J. BAGUL, C. CHESNEAU, M. KOSTIĆ: *The Cusa-Huygens inequality revisited*, Novi Sad J. Math. **50**:2 (2020), 149–159.

55. Y. J. BAGUL, C. CHESNEAU: *Generalized bounds for sine and cosine functions*, Asian-Eur. J. Math. **15**:1 (2022), 1–16.

56. R. M. DHAIGUDE, C. CHESNEAU, Y. J. BAGUL: *About Trigonometric-polynomial Bounds of Sinc Function*, Math. Sci. Appl. E-Notes. **8**:1 (2020), 100–104.
57. Y. J. BAGUL, R. M. DHAIGUDE, M. KOSTIĆ, C. CHESNEAU: *Polynomial-Exponential Bounds for Some Trigonometric and Hyperbolic Functions*, Axioms **10**:4, 308 (2021), 1–10.

58. B. ZHANG, C.-P. CHEN: *Sharp Wilker and Huygens type inequalities for trigonometric and inverse trigonometric functions*, J. Math. Inequal. **14**:3 (2020), 673–684.

59. C.-P. CHEN, R. B. PARIS: *On the Wilker and Huygens-type inequalities*, J. Math. Inequal. **14**:3 (2020), 685–705.

60. B. ZHANG, C.-P. CHEN: *Sharpness and generalization of Jordan, Becker-Stark and Papenfuss inequalities with an application*, J. Math. Inequal. **13**:4 (2019), 1209–1234.

61. C.-P. CHEN, N. ELEZOVIĆ: *Sharp Redheffer-type and Becker-Stark-type inequalities with an application*, Math. Inequal. Appl. **21**:4 (2018), 1059–1078.

62. Q.-X. QIAO, C.-P. CHEN: *Approximations to inverse tangent function*, J. Inequal. Appl. **2018**:141 (2018), 1–14.

63. C.-P. CHEN, F. QI: *Inequalities of some trigonometric functions*, Publikacije Elektrotehničkog fakulteta. Serija Matematika **15** (2004), 72–79.

64. B.-N. GUO, Q.-M. LUO, F. QI: *Sharpening and generalizations of Shafer-Fink's double inequality for the arc sine function*, Filomat **27**:2 (2013), 261–265.

65. W.-D. JIANG, Q.-M. LUO, F. QI: *Refinements and Sharpening of some Huygens and Wilker Type Inequalities*, Turkish Journal of Analysis and Number Theory **2**:4 (2014), 134–139.

66. W.-D. JIANG: *New sharp inequalities of Mitrinović-Adamović type*, Appl. Anal. Discrete Math. **17**:1 (2023), 76–91.

67. G. BERCU: *The natural approach of trigonometric inequalities - Padé approximant*, J. Math. Inequal. **11**:1 (2017), 181–191.

68. G. BERCU: *Refinements of Wilker-Huygens-Type Inequalities via Trigonometric Series*, Symmetry **13**:8 (2021), 1–13.

69. C.-P. CHEN, C. MORTICI: *The relationship between Huygens' and Wilker's inequalities and further remarks*, Appl. Anal. Discrete Math. **17**:1 (2023), 92–100.

70. L. ZHU, Z. SUN: *Refinements of Huygens- and Wilker-type inequalities*, AIMS Mathematics **5**:4 (2020), 2967–2978.

71. L. ZHU: *New inequalities of Wilker's type for circular functions*, AIMS Mathematics **5**:5 (2020), 4874–4888.

72. L. ZHU: *New Inequalities of Cusa-Huygens Type*, Mathematics **9**:17 (2021), 1–13.

73. Y. J. BAGUL, S. B. THOOL, C. CHESNEAU, R. M. DHAIGUDE: *Refinements of some classical inequalities involving sinc and hyperbolic sinc functions*, Ann. Math. Sil. **37**:1 (2023), 1–15.

74. N. KASUGA, M. NAKASUJI, Y. NISHIZAWA, T. SEKINE: *Sharped Jordan's type inequalities with exponential approximations*, J. Math. Inequal. **17**:4 (2023), 1539–1550.

75. D.Q. HUY, P.T. HIEU D.T.T. VAN: *New sharp bounds for sinc and hyperbolic sinc functions via cos and cosh functions*, Afr. Mat. **35**:38 (2024), 1–13.
57. Y. J. BAGUL, R. M. DHAIGUDE, M. KOSTIĆ, C. CHESNEAU: *Polynomial-Exponential Bounds for Some Trigonometric and Hyperbolic Functions*, Axioms **10**:4, 308 (2021), 1–10.

58. B. ZHANG, C.-P. CHEN: *Sharp Wilker and Huygens type inequalities for trigonometric and inverse trigonometric functions*, J. Math. Inequal. **14**:3 (2020), 673–684.

59. C.-P. CHEN, R. B. PARIS: *On the Wilker and Huygens-type inequalities*, J. Math. Inequal. **14**:3 (2020), 685–705.

60. B. ZHANG, C.-P. CHEN: *Sharpness and generalization of Jordan, Becker-Stark and Papenfuss inequalities with an application*, J. Math. Inequal. **13**:4 (2019), 1209–1234.

61. C.-P. CHEN, N. ELEZOVIĆ: *Sharp Redheffer-type and Becker-Stark-type inequalities with an application*, Math. Inequal. Appl. **21**:4 (2018), 1059–1078.

62. Q.-X. QIAO, C.-P. CHEN: *Approximations to inverse tangent function*, J. Inequal. Appl. **2018**:141 (2018), 1–14.

63. C.-P. CHEN, F. QI: *Inequalities of some trigonometric functions*, Publikacije Elektrotehničkog fakulteta. Serija Matematika **15** (2004), 72–79.

64. B.-N. GUO, Q.-M. LUO, F. QI: *Sharpening and generalizations of Shafer-Fink's double inequality for the arc sine function*, Filomat **27**:2 (2013), 261–265.

65. W.-D. JIANG, Q.-M. LUO, F. QI: *Refinements and Sharpening of some Huygens and Wilker Type Inequalities*, Turkish Journal of Analysis and Number Theory **2**:4 (2014), 134–139.

66. W.-D. JIANG: *New sharp inequalities of Mitrinović-Adamović type*, Appl. Anal. Discrete Math. **17**:1 (2023), 76–91.

67. G. BERCU: *The natural approach of trigonometric inequalities - Padé approximant*, J. Math. Inequal. **11**:1 (2017), 181–191.

68. G. BERCU: *Refinements of Wilker-Huygens-Type Inequalities via Trigonometric Series*, Symmetry **13**:8 (2021), 1–13.

69. C.-P. CHEN, C. MORTICI: *The relationship between Huygens' and Wilker's inequalities and further remarks*, Appl. Anal. Discrete Math. **17**:1 (2023), 92–100.

70. L. ZHU, Z. SUN: *Refinements of Huygens- and Wilker-type inequalities*, AIMS Mathematics **5**:4 (2020), 2967–2978.

71. L. ZHU: *New inequalities of Wilker's type for circular functions*, AIMS Mathematics **5**:5 (2020), 4874–4888.

72. L. ZHU: *New Inequalities of Cusa-Huygens Type*, Mathematics **9**:17 (2021), 1–13.

73. Y. J. BAGUL, S. B. THOOL, C. CHESNEAU, R. M. DHAIGUDE: *Refinements of some classical inequalities involving sinc and hyperbolic sinc functions*, Ann. Math. Sil. **37**:1 (2023), 1–15.

74. N. KASUGA, M. NAKASUJI, Y. NISHIZAWA, T. SEKINE: *Sharped Jordan's type inequalities with exponential approximations*, J. Math. Inequal. **17**:4 (2023), 1539–1550.

75. D.Q. HUY, P.T. HIEU D.T.T. VAN: *New sharp bounds for sinc and hyperbolic sinc functions via cos and cosh functions*, Afr. Mat. **35**:38 (2024), 1–13.
# APPENDIX

This Appendix was created using the automated prover SimTheP, which for the MTP function and the interval gives as output TeX/PDF files that were directly transferred to the Appendix.

## APPENDIX A1

The initial MTP function is

$$f(x) = 2 \cdot x^7 + 135 \cdot \sin x \cdot \cos^2 x + (15 \cdot x^4 - 135) \cdot \sin x - 45 \cdot x \cdot \cos^3 x + (90 \cdot x^3 + 45 \cdot x) \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.

Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

**I** (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 3.51310... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

**II** (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = -\frac{45}{4} \cdot x \cdot \cos 3x + (15 \cdot x^4 - \frac{405}{4}) \cdot \sin x + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \cos x + 2 \cdot x^7 + \frac{135}{4} \cdot \sin 3x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = \frac{135}{4} \cdot \sin 3x + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \cos x + 15 \cdot x^4 \cdot \sin x + 2 \cdot x^7,$$

$$f^{-}(x) = -\frac{405}{4} \cdot \sin x - \frac{45}{4} \cdot x \cdot \cos 3x.$$

**III** (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^{+}(x)$ and $f^{-}(x)$ respectively

$$P_{i_0, i_1, i_2}^{+}(x) = \frac{135}{4} \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin 0}(3x) + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \underline{T}_{4 \cdot i_1 + 2}^{\cos 0}(x) + 15 \cdot x^4 \cdot \underline{T}_{4 \cdot i_2 + 3}^{\sin 0}(x) + 2 \cdot x^7,$$

$$P_{i_3, i_4}^{-}(x) = -\frac{405}{4} \cdot \overline{T}_{4 \cdot i_3 + 1}^{\sin 0}(x) - \frac{45}{4} \cdot x \cdot \overline{T}_{4 \cdot i_4}^{\cos 0}(3x).$$

For concrete indices $(i_0, i_1, i_2, i_3, i_4) = (2, 2, 1, 2, 3)$, we obtain

$$P_{2,2,1}^{+}(x) = \frac{135}{4} \cdot \underline{T}_{4 \cdot 2 + 3}^{\sin 0}(3x) + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \underline{T}_{4 \cdot 2 + 2}^{\cos 0}(x) + 15 \cdot x^4 \cdot \underline{T}_{4 \cdot 1 + 3}^{\sin 0}(x) + 2 \cdot x^7,$$

$$P_{2,2,1}^{+}(x) = -\frac{1}{40320} \cdot x^{13} - \frac{133523}{887040} \cdot x^{11} + \frac{3281}{1792} \cdot x^{9} - \frac{639}{56} \cdot x^{7} + \frac{621}{16} \cdot x^{5} - \frac{135}{2} \cdot x^{3} + \frac{225}{2} \cdot x$$
# APPENDIX

This Appendix was created using the automated prover SimTheP, which for the MTP function and the interval gives as output TeX/PDF files that were directly transferred to the Appendix.

## APPENDIX A1

The initial MTP function is

$$f(x) = 2 \cdot x^7 + 135 \cdot \sin x \cdot \cos^2 x + (15 \cdot x^4 - 135) \cdot \sin x - 45 \cdot x \cdot \cos^3 x + (90 \cdot x^3 + 45 \cdot x) \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.

Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

**I** (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 3.51310... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

**II** (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = -\frac{45}{4} \cdot x \cdot \cos 3x + (15 \cdot x^4 - \frac{405}{4}) \cdot \sin x + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \cos x + 2 \cdot x^7 + \frac{135}{4} \cdot \sin 3x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = \frac{135}{4} \cdot \sin 3x + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \cos x + 15 \cdot x^4 \cdot \sin x + 2 \cdot x^7,$$

$$f^{-}(x) = -\frac{405}{4} \cdot \sin x - \frac{45}{4} \cdot x \cdot \cos 3x.$$

**III** (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^{+}(x)$ and $f^{-}(x)$ respectively

$$P_{i_0, i_1, i_2}^{+}(x) = \frac{135}{4} \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin 0}(3x) + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \underline{T}_{4 \cdot i_1 + 2}^{\cos 0}(x) + 15 \cdot x^4 \cdot \underline{T}_{4 \cdot i_2 + 3}^{\sin 0}(x) + 2 \cdot x^7,$$

$$P_{i_3, i_4}^{-}(x) = -\frac{405}{4} \cdot \overline{T}_{4 \cdot i_3 + 1}^{\sin 0}(x) - \frac{45}{4} \cdot x \cdot \overline{T}_{4 \cdot i_4}^{\cos 0}(3x).$$

For concrete indices $(i_0, i_1, i_2, i_3, i_4) = (2, 2, 1, 2, 3)$, we obtain

$$P_{2,2,1}^{+}(x) = \frac{135}{4} \cdot \underline{T}_{4 \cdot 2 + 3}^{\sin 0}(3x) + (90 \cdot x^3 + \frac{45}{4} \cdot x) \cdot \underline{T}_{4 \cdot 2 + 2}^{\cos 0}(x) + 15 \cdot x^4 \cdot \underline{T}_{4 \cdot 1 + 3}^{\sin 0}(x) + 2 \cdot x^7,$$

$$P_{2,2,1}^{+}(x) = -\frac{1}{40320} \cdot x^{13} - \frac{133523}{887040} \cdot x^{11} + \frac{3281}{1792} \cdot x^{9} - \frac{639}{56} \cdot x^{7} + \frac{621}{16} \cdot x^{5} - \frac{135}{2} \cdot x^{3} + \frac{225}{2} \cdot x$$
and

$$P_{2,3}^{-}(x) = -\frac{405}{4} \cdot \bar{T}^{\sin,0}_{4 \cdot 2+1}(x) - \frac{45}{4} \cdot x \cdot \bar{T}^{\cos,0}_{4 \cdot 3}(3x),$$

$$P_{2,3}^{-}(x) = -\frac{19683}{1576960} \cdot x^{13} + \frac{6561}{35840} \cdot x^{11} - \frac{3281}{1792} \cdot x^{9} + \frac{639}{56} \cdot x^{7} - \frac{621}{16} \cdot x^{5} + \frac{135}{2} \cdot x^{3} - \frac{225}{2} \cdot x.$$

Finally, for the MTP function

$$f(x) = f^{+}(x) + f^{-}(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_{2,2,1}^{+}(x) + P_{2,3}^{-}(x) = -\frac{25357}{2027520} \cdot x^{13} + \frac{115447}{3548160} \cdot x^{11}$$

over $(0, \frac{\pi}{2})$, i.e. it holds that

$$f(x) > P(x)$$

over $(0, \frac{\pi}{2})$.

IV (The final part) Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over $(0, \frac{\pi}{2})$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ has only one zero over the concrete extended segment $[-0.1, 1.58]$ of the initial interval $(0, \frac{\pi}{2})$.

2. Facts $P(-0.1) \neq 0$, $P(0) = 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2}$ ($P(\frac{\pi}{2}) = 0.24116... > 0$).

Therefore, the following inequality

$$f(x) > 0$$

is true over $(0, \frac{\pi}{2})$. $\square$

## APPENDIX A2

The initial MTP function is

$$f(x) = (-15309 \cdot x^6 + 170100 \cdot x^4 - 476280 \cdot x^2 + 181440) \cdot \sin x \cdot \cos^2 x + (-x^{10} + 3843 \cdot x^6 - 44100 \cdot x^4 + 158760 \cdot x^2 - 181440) \cdot \sin x + (2187 \cdot x^7 - 61236 \cdot x^5 + 340200 \cdot x^3 - 423360 \cdot x) \cdot \cos^3 x + (-1641 \cdot x^7 + 46116 \cdot x^5 - 264600 \cdot x^3 + 423360 \cdot x) \cdot \cos x$$

and the initial interval is $\mathbb{S} = (0, 1]$.

Automated proof that $f(x) > 0$ for $x \in (0, 1]$:

I (Recognition of possible case) Facts $f(0) = 0$ and $f(1) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $1$ ($f(1) = 14.68957... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, 1]$.
and

$$P_{2,3}^{-}(x) = -\frac{405}{4} \cdot \overline{T}^{\sin,0}_{4 \cdot 2+1}(x) - \frac{45}{4} \cdot x \cdot \overline{T}^{\cos,0}_{4 \cdot 3}(3x),$$

$$P_{2,3}^{-}(x) = -\frac{19683}{1576960} \cdot x^{13} + \frac{6561}{35840} \cdot x^{11} - \frac{3281}{1792} \cdot x^{9} + \frac{639}{56} \cdot x^{7} - \frac{621}{16} \cdot x^{5} + \frac{135}{2} \cdot x^{3} - \frac{225}{2} \cdot x.$$

Finally, for the MTP function

$$f(x) = f^{+}(x) + f^{-}(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_{2,2,1}^{+}(x) + P_{2,3}^{-}(x) = -\frac{25357}{2027520} \cdot x^{13} + \frac{115447}{3548160} \cdot x^{11}$$

over $(0, \frac{\pi}{2})$, i.e. it holds that

$$f(x) > P(x)$$

over $(0, \frac{\pi}{2})$.

IV (The final part) Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over $(0, \frac{\pi}{2})$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ has only one zero over the concrete extended segment $[-0.1, 1.58]$ of the initial interval $(0, \frac{\pi}{2})$.

2. Facts $P(-0.1) \neq 0$, $P(0) = 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2}$ ($P(\frac{\pi}{2}) = 0.24116... > 0$).

Therefore, the following inequality

$$f(x) > 0$$

is true over $(0, \frac{\pi}{2})$. $\square$

## APPENDIX A2

The initial MTP function is

$$f(x) = (-15309 \cdot x^6 + 170100 \cdot x^4 - 476280 \cdot x^2 + 181440) \cdot \sin x \cdot \cos^2 x + (-x^{10} + 3843 \cdot x^6 - 44100 \cdot x^4 + 158760 \cdot x^2 - 181440) \cdot \sin x + (2187 \cdot x^7 - 61236 \cdot x^5 + 340200 \cdot x^3 - 423360 \cdot x) \cdot \cos^3 x + (-1641 \cdot x^7 + 46116 \cdot x^5 - 264600 \cdot x^3 + 423360 \cdot x) \cdot \cos x$$

and the initial interval is $\mathbb{S} = (0, 1]$.

Automated proof that $f(x) > 0$ for $x \in (0, 1]$:

I (Recognition of possible case) Facts $f(0) = 0$ and $f(1) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $1$ ($f(1) = 14.68957... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, 1]$.
II (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = \left(-\frac{15309}{4} \cdot x^6 + 42525 \cdot x^4 - 119070 \cdot x^2 + 45360\right) \cdot \sin 3x \\ + \left(\frac{2187}{4} \cdot x^7 - 15309 \cdot x^5 + 85050 \cdot x^3 - 105840 \cdot x\right) \cdot \cos 3x \\ + \left(-x^{10} + \frac{63}{4} \cdot x^6 - 1575 \cdot x^4 + 39690 \cdot x^2 - 136080\right) \cdot \sin x \\ + \left(-\frac{3}{4} \cdot x^7 + 189 \cdot x^5 - 9450 \cdot x^3 + 105840 \cdot x\right) \cdot \cos x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = (42525 \cdot x^{4} + 45360) \cdot \sin 3x + (189 \cdot x^{5} + 105840 \cdot x) \cdot \cos x \\ + \left(\frac{63}{4} \cdot x^{6} + 39690 \cdot x^{2}\right) \cdot \sin x + \left(\frac{2187}{4} \cdot x^{7} + 85050 \cdot x^{3}\right) \cdot \cos 3x,$$

$$f^{-}(x) = \left(-x^{10} - 1575 \cdot x^{4} - 136080\right) \cdot \sin x + \left(-15309 \cdot x^{5} - 105840 \cdot x\right) \cdot \cos 3x \\ + \left(-\frac{15309}{4} \cdot x^{6} - 119070 \cdot x^{2}\right) \cdot \sin 3x + \left(-\frac{3}{4} \cdot x^{7} - 9450 \cdot x^{3}\right) \cdot \cos x.$$

III (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^+(x)$ and $f^-(x)$ respectively

$$P_{i_0, i_1, i_2, i_3}^{+}(x) = (42525 \cdot x^4 + 45360) \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin, 0}(3x) \\ + (189 \cdot x^5 + 105840 \cdot x) \cdot \underline{T}_{4 \cdot i_1 + 2}^{\cos, 0}(x) \\ + (\frac{63}{4} \cdot x^6 + 39690 \cdot x^2) \cdot \underline{T}_{4 \cdot i_2 + 3}^{\sin, 0}(x) \\ + (\frac{2187}{4} \cdot x^7 + 85050 \cdot x^3) \cdot \underline{T}_{4 \cdot i_3 + 2}^{\cos, 0}(3x),$$

$$P_{i_4, i_5, i_6, i_7}^{-}(x) = \left(-x^{10} - 1575 \cdot x^{4} - 136080\right) \cdot \bar{T}_{4 \cdot i_{4}+1}^{\sin, 0}(x) \\ + \left(-15309 \cdot x^{5} - 105840 \cdot x\right) \cdot \bar{T}_{4 \cdot i_{5}}^{\cos, 0}(3x) \\ + \left(-\frac{15309}{4} \cdot x^{6} - 119070 \cdot x^{2}\right) \cdot \bar{T}_{4 \cdot i_{6}+1}^{\sin, 0}(3x) \\ + \left(-\frac{3}{4} \cdot x^{7} - 9450 \cdot x^{3}\right) \cdot \bar{T}_{4 \cdot i_{7}}^{\cos, 0}(x).$$

For concrete indices ($i_0, i_1, i_2, i_3, i_4, i_5, i_6, i_7$) = (3, 3, 3, 3, 3, 3, 3), we obtain

$$P_{3,3,3,3}^{+}(x) = (42525 \cdot x^4 + 45360) \cdot \underline{T}_{4 \cdot 3 + 3}^{\sin, 0}(3x) \\ + (189 \cdot x^5 + 105840 \cdot x) \cdot \underline{T}_{4 \cdot 3 + 2}^{\cos, 0}(x) \\ + (\frac{63}{4} \cdot x^6 + 39690 \cdot x^2) \cdot \underline{T}_{4 \cdot 3 + 3}^{\sin, 0}(x) \\ + (\frac{2187}{4} \cdot x^7 + 85050 \cdot x^3) \cdot \underline{T}_{4 \cdot 3 + 2}^{\cos, 0}(3x),$$

$$P_{3,3,3,3}^{+}(x) = -\frac{335267731}{11176704000} \cdot x^{21} + \frac{38742049}{276756480} \cdot x^{19} - \frac{602542}{225225} \cdot x^{17} \\ - \frac{169795501}{28828800} \cdot x^{15} + \frac{7838771}{20592} \cdot x^{13} - \frac{15677779}{5280} \cdot x^{11} \\ + 76650 \cdot x^{7} - 165312 \cdot x^{5} - 132300 \cdot x^{3} + 241920 \cdot x$$
II (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$ 
\begin{aligned}
f(x) = & \left(-\frac{15309}{4} \cdot x^6 + 42525 \cdot x^4 - 119070 \cdot x^2 + 45360\right) \cdot \sin 3x \\
& + \left(\frac{2187}{4} \cdot x^7 - 15309 \cdot x^5 + 85050 \cdot x^3 - 105840 \cdot x\right) \cdot \cos 3x \\
& + \left(-x^{10} + \frac{63}{4} \cdot x^6 - 1575 \cdot x^4 + 39690 \cdot x^2 - 136080\right) \cdot \sin x \\
& + \left(-\frac{3}{4} \cdot x^7 + 189 \cdot x^5 - 9450 \cdot x^3 + 105840 \cdot x\right) \cdot \cos x.
\end{aligned}
$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$ f^{+}(x) = (42525 \cdot x^{4} + 45360) \cdot \sin 3x + (189 \cdot x^{5} + 105840 \cdot x) \cdot \cos x + \left(\frac{63}{4} \cdot x^{6} + 39690 \cdot x^{2}\right) \cdot \sin x + \left(\frac{2187}{4} \cdot x^{7} + 85050 \cdot x^{3}\right) \cdot \cos 3x, $$

$$ f^{-}(x) = \left(-x^{10} - 1575 \cdot x^{4} - 136080\right) \cdot \sin x + \left(-15309 \cdot x^{5} - 105840 \cdot x\right) \cdot \cos 3x + \left(-\frac{15309}{4} \cdot x^{6} - 119070 \cdot x^{2}\right) \cdot \sin 3x + \left(-\frac{3}{4} \cdot x^{7} - 9450 \cdot x^{3}\right) \cdot \cos x. $$

III (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^+(x)$ and $f^-(x)$ respectively

$$ 
\begin{aligned}
P_{i_0, i_1, i_2, i_3}^{+}(x) = & \left(42525 \cdot x^4 + 45360\right) \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin, 0}(3x) \\
& + \left(189 \cdot x^5 + 105840 \cdot x\right) \cdot \underline{T}_{4 \cdot i_1 + 2}^{\cos, 0}(x) \\
& + \left(\frac{63}{4} \cdot x^6 + 39690 \cdot x^2\right) \cdot \underline{T}_{4 \cdot i_2 + 3}^{\sin, 0}(x) \\
& + \left(\frac{2187}{4} \cdot x^7 + 85050 \cdot x^3\right) \cdot \underline{T}_{4 \cdot i_3 + 2}^{\cos, 0}(3x),
\end{aligned}
$$

$$ 
\begin{aligned}
P_{i_4, i_5, i_6, i_7}^{-}(x) = & \left(-x^{10} - 1575 \cdot x^{4} - 136080\right) \cdot \bar{T}_{4 \cdot i_4 + 1}^{\sin, 0}(x) \\
& + \left(-15309 \cdot x^{5} - 105840 \cdot x\right) \cdot \bar{T}_{4 \cdot i_5}^{\cos, 0}(3x) \\
& + \left(-\frac{15309}{4} \cdot x^{6} - 119070 \cdot x^{2}\right) \cdot \bar{T}_{4 \cdot i_6 + 1}^{\sin, 0}(3x) \\
& + \left(-\frac{3}{4} \cdot x^{7} - 9450 \cdot x^{3}\right) \cdot \bar{T}_{4 \cdot i_7}^{\cos, 0}(x).
\end{aligned}
$$

For concrete indices ($i_0, i_1, i_2, i_3, i_4, i_5, i_6, i_7$) = (3, 3, 3, 3, 3, 3, 3), we obtain

$$ 
\begin{aligned}
P_{3,3,3,3}^{+}(x) = & \left(42525 \cdot x^4 + 45360\right) \cdot \underline{T}_{4 \cdot 3 + 3}^{\sin, 0}(3x) \\
& + \left(189 \cdot x^5 + 105840 \cdot x\right) \cdot \underline{T}_{4 \cdot 3 + 2}^{\cos, 0}(x) \\
& + \left(\frac{63}{4} \cdot x^6 + 39690 \cdot x^2\right) \cdot \underline{T}_{4 \cdot 3 + 3}^{\sin, 0}(x) \\
& + \left(\frac{2187}{4} \cdot x^7 + 85050 \cdot x^3\right) \cdot \underline{T}_{4 \cdot 3 + 2}^{\cos, 0}(3x),
\end{aligned}
$$

$$ 
\begin{aligned}
P_{3,3,3,3}^{+}(x) = & -\frac{335267731}{11176704000} \cdot x^{21} + \frac{38742049}{276756480} \cdot x^{19} - \frac{602542}{225225} \cdot x^{17} \\
& - \frac{169795501}{28828800} \cdot x^{15} + \frac{7838771}{20592} \cdot x^{13} - \frac{15677779}{5280} \cdot x^{11} \\
& + 76650 \cdot x^{7} - 165312 \cdot x^{5} - 132300 \cdot x^{3} + 241920 \cdot x
\end{aligned}
$$
and

$$ P_{3,3,3,3}^{-}(x) = (-x^{10} - 1575 \cdot x^{4} - 136080) \cdot \bar{T}_{4 \cdot 3+1}^{\sin,0}(x) \\ (-15309 \cdot x^{5} - 105840 \cdot x) \cdot \bar{T}_{4 \cdot 3}^{\cos,0}(3x) \\ + (-\frac{15309}{4} \cdot x^{6} - 119070 \cdot x^{2}) \cdot \bar{T}_{4 \cdot 3+1}^{\sin,0}(3x) \\ + (-\frac{3}{4} \cdot x^{7} - 9450 \cdot x^{3}) \cdot \bar{T}_{4 \cdot 3}^{\cos,0}(x), $$

$$ P_{3,3,3,3}^{-}(x) = -\frac{1}{6227020800} \cdot x^{23} + \frac{1}{39916800} \cdot x^{21} - \frac{1355975527}{1383782400} \cdot x^{19} \\ + \frac{4289}{21621600} \cdot x^{17} + \frac{317827231}{28828800} \cdot x^{15} - \frac{8632499}{20592} \cdot x^{13} + \frac{5302897}{1760} \cdot x^{11} \\ -76650 \cdot x^{7} + 165312 \cdot x^{5} + 132300 \cdot x^{3} - 241920 \cdot x. $$

Finally, for the MTP function

$$ f(x) = f^{+}(x) + f^{-}(x) $$

we obtain the concrete downward polynomial approximation

$$ P(x) = P_{3,3,3,3}^{+}(x) + P_{3,3,3,3}^{-}(x) \\ = -\frac{1}{6227020800} \cdot x^{23} - \frac{12417313}{413952000} \cdot x^{21} - \frac{581132641}{691891200} \cdot x^{19} \\ - \frac{4449211}{1663200} \cdot x^{17} + \frac{21361}{4160} \cdot x^{15} - \frac{424}{11} \cdot x^{13} + \frac{656}{15} \cdot x^{11} $$

over (0, 1], i.e. it holds that

$$ f(x) > P(x) $$

over (0, 1].

IV (The final part) Based on the Sturm theorem, the following inequality

$$ P(x) > 0 $$

is true over (0, 1]. The stated conclusion for the polynomial function P is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function P(x) has only one zero over the concrete extended segment [-0.1, 1] of the initial interval (0, 1].

2. Facts P(-0.1) ≠ 0, P(0) = 0 and P(1) ≠ 0 are correct.

3. The polynomial P is positive at boundary point 1 (P(1) = 6.77772... > 0). Therefore, the following inequality

$$ f(x) > 0 $$

is true over (0, 1].

□

APPENDIX A3

The initial MTP function is

$$ h(x) = (-52488 \cdot x^{7} + 816480 \cdot x^{5} - 3810240 \cdot x^{3} + 4354560 \cdot x) \cdot \cos^{3} x \\ + (-6561 \cdot x^{8} + 244944 \cdot x^{6} - 2041200 \cdot x^{4} + 5080320 \cdot x^{2} - 1814400) \cdot \sin x \cdot \cos^{2} x \\ + (-x^{11} + 39384 \cdot x^{7} - 614880 \cdot x^{5} + 2963520 \cdot x^{3} - 4354560 \cdot x) \cdot \cos x \\ + (1641 \cdot x^{8} - 61488 \cdot x^{6} + 529200 \cdot x^{4} - 1693440 \cdot x^{2} + 1814400) \cdot \sin x $$

and the initial interval is S = [1, π/2].
and

$$P_{3,3,3,3}^{-}(x) = (-x^{10} - 1575 \cdot x^{4} - 136080) \cdot \bar{T}_{4 \cdot 3+1}^{\sin,0}(x) \\ (-15309 \cdot x^{5} - 105840 \cdot x) \cdot \bar{T}_{4 \cdot 3}^{\cos,0}(3x) \\ + (-\frac{15309}{4} \cdot x^{6} - 119070 \cdot x^{2}) \cdot \bar{T}_{4 \cdot 3+1}^{\sin,0}(3x) \\ + (-\frac{3}{4} \cdot x^{7} - 9450 \cdot x^{3}) \cdot \bar{T}_{4 \cdot 3}^{\cos,0}(x),$$

$$P_{3,3,3,3}^{-}(x) = -\frac{1}{6227020800} \cdot x^{23} + \frac{1}{39916800} \cdot x^{21} - \frac{1355975527}{1383782400} \cdot x^{19} \\ + \frac{4289}{21621600} \cdot x^{17} + \frac{317827231}{28828800} \cdot x^{15} - \frac{8632499}{20592} \cdot x^{13} + \frac{5302897}{1760} \cdot x^{11} \\ -76650 \cdot x^{7} + 165312 \cdot x^{5} + 132300 \cdot x^{3} - 241920 \cdot x.$$

Finally, for the MTP function

$$f(x) = f^{+}(x) + f^{-}(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_{3,3,3,3}^{+}(x) + P_{3,3,3,3}^{-}(x) \\ = -\frac{1}{6227020800} \cdot x^{23} - \frac{12417313}{413952000} \cdot x^{21} - \frac{581132641}{691891200} \cdot x^{19} \\ - \frac{4449211}{1663200} \cdot x^{17} + \frac{21361}{4160} \cdot x^{15} - \frac{424}{11} \cdot x^{13} + \frac{656}{15} \cdot x^{11}$$

over (0, 1], i.e. it holds that

$$f(x) > P(x)$$

over (0, 1].

IV (The final part) Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over (0, 1]. The stated conclusion for the polynomial function P is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function P(x) has only one zero over the concrete extended segment [-0.1, 1] of the initial interval (0, 1].

2. Facts P(-0.1) ≠ 0, P(0) = 0 and P(1) ≠ 0 are correct.

3. The polynomial P is positive at boundary point 1 (P(1) = 6.77772... > 0). Therefore, the following inequality

$$f(x) > 0$$

is true over (0, 1].

□

APPENDIX A3

The initial MTP function is

$$h(x) = (-52488 \cdot x^7 + 816480 \cdot x^5 - 3810240 \cdot x^3 + 4354560 \cdot x) \cdot \cos^3 x \\ + (-6561 \cdot x^8 + 244944 \cdot x^6 - 2041200 \cdot x^4 + 5080320 \cdot x^2 - 1814400) \cdot \sin x \cdot \cos^2 x \\ + (-x^{11} + 39384 \cdot x^7 - 614880 \cdot x^5 + 2963520 \cdot x^3 - 4354560 \cdot x) \cdot \cos x \\ + (1641 \cdot x^8 - 61488 \cdot x^6 + 529200 \cdot x^4 - 1693440 \cdot x^2 + 1814400) \cdot \sin x$$

and the initial interval is $S = [1, \frac{\pi}{2}]$.
After the multiplication by $-1$, we obtain the MTP function

$$f(x) = (52488 \cdot x^7 - 816480 \cdot x^5 + 3810240 \cdot x^3 - 4354560 \cdot x) \cdot \cos^3 x \\ + (6561 \cdot x^8 - 244944 \cdot x^6 + 2041200 \cdot x^4 - 5080320 \cdot x^2 + 1814400) \cdot \sin x \cdot \cos^2 x \\ + (x^{11} - 39384 \cdot x^7 + 614880 \cdot x^5 - 2963520 \cdot x^3 + 4354560 \cdot x) \cdot \cos x \\ + (-1641 \cdot x^8 + 61488 \cdot x^6 - 529200 \cdot x^4 + 1693440 \cdot x^2 - 1814400) \cdot \sin x.$$

Automated proof that $f(x) > 0$ for $x \in [1, \frac{\pi}{2}]$:

**I** (Recognition of possible case) Facts $f(1) \neq 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $1$ ($f(1) = 27.02986... > 0$) and at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 5021.73462... > 0$). Therefore, it is possible that $f(x) > 0$ over $[1, \frac{\pi}{2}]$.

**II** (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = \left(\frac{6561}{4} \cdot x^8 - 61236 \cdot x^6 + 510300 \cdot x^4 - 1270080 \cdot x^2 + 453600\right) \cdot \sin 3x \\ + \left(13122 \cdot x^7 - 204120 \cdot x^5 + 952560 \cdot x^3 - 1088640 \cdot x\right) \cdot \cos 3x \\ + \left(-\frac{3}{4} \cdot x^8 + 252 \cdot x^6 - 18900 \cdot x^4 + 423360 \cdot x^2 - 1360800\right) \cdot \sin x \\ + \left(x^{11} - 18 \cdot x^7 + 2520 \cdot x^5 - 105840 \cdot x^3 + 1088640 \cdot x\right) \cdot \cos x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = \left(\frac{6561}{4} \cdot x^8 + 510300 \cdot x^4 + 453600\right) \cdot \sin 3x \\ + \left(13122 \cdot x^7 + 952560 \cdot x^3\right) \cdot \cos 3x \\ + \left(252 \cdot x^6 + 423360 \cdot x^2\right) \cdot \sin x \\ + \left(x^{11} + 2520 \cdot x^5 + 1088640 \cdot x\right) \cdot \cos x,$$

$$f^{-}(x) = \left(-61236 \cdot x^6 - 1270080 \cdot x^2\right) \cdot \sin 3x \\ + \left(-204120 \cdot x^5 - 1088640 \cdot x\right) \cdot \cos 3x \\ + \left(-\frac{3}{4} \cdot x^8 - 18900 \cdot x^4 - 1360800\right) \cdot \sin x \\ + \left(-18 \cdot x^7 - 105840 \cdot x^3\right) \cdot \cos x.$$

**III** (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approxima-
After the multiplication by $-1$, we obtain the MTP function

$$f(x) = (52488 \cdot x^7 - 816480 \cdot x^5 + 3810240 \cdot x^3 - 4354560 \cdot x) \cdot \cos^3 x + (6561 \cdot x^8 - 244944 \cdot x^6 + 2041200 \cdot x^4 - 5080320 \cdot x^2 + 1814400) \cdot \sin x \cdot \cos^2 x + (x^{11} - 39384 \cdot x^7 + 614880 \cdot x^5 - 2963520 \cdot x^3 + 4354560 \cdot x) \cdot \cos x + (-1641 \cdot x^8 + 61488 \cdot x^6 - 529200 \cdot x^4 + 1693440 \cdot x^2 - 1814400) \cdot \sin x.$$

Automated proof that $f(x) > 0$ for $x \in [1, \frac{\pi}{2}]$:

**I** (Recognition of possible case) Facts $f(1) \neq 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $1$ ($f(1) = 27.02986... > 0$) and at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 5021.73462... > 0$). Therefore, it is possible that $f(x) > 0$ over $[1, \frac{\pi}{2}]$.

**II** (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = \left(\frac{6561}{4} \cdot x^8 - 61236 \cdot x^6 + 510300 \cdot x^4 - 1270080 \cdot x^2 + 453600\right) \cdot \sin 3x + (13122 \cdot x^7 - 204120 \cdot x^5 + 952560 \cdot x^3 - 1088640 \cdot x) \cdot \cos 3x + (-\frac{3}{4} \cdot x^8 + 252 \cdot x^6 - 18900 \cdot x^4 + 423360 \cdot x^2 - 1360800) \cdot \sin x + (x^{11} - 18 \cdot x^7 + 2520 \cdot x^5 - 105840 \cdot x^3 + 1088640 \cdot x) \cdot \cos x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^+(x) = \left(\frac{6561}{4} \cdot x^8 + 510300 \cdot x^4 + 453600\right) \cdot \sin 3x + (13122 \cdot x^7 + 952560 \cdot x^3) \cdot \cos 3x + (252 \cdot x^6 + 423360 \cdot x^2) \cdot \sin x + (x^{11} + 2520 \cdot x^5 + 1088640 \cdot x) \cdot \cos x,$$

$$f^-(x) = (-61236 \cdot x^6 - 1270080 \cdot x^2) \cdot \sin 3x + (-204120 \cdot x^5 - 1088640 \cdot x) \cdot \cos 3x + (-\frac{3}{4} \cdot x^8 - 18900 \cdot x^4 - 1360800) \cdot \sin x + (-18 \cdot x^7 - 105840 \cdot x^3) \cdot \cos x.$$

**III** (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approxima-
tions, we obtain downward polynomial approximations of $f^+(x)$ and $f^-(x)$ respectively

$$ P_{i_0, i_1, i_2, i_3}^{+}(x) = \left( \frac{6561}{4} \cdot x^8 + 510300 \cdot x^4 + 453600 \right) \cdot \underline{T}_{4, i_0+3}^{\sin, 0}(3x) \\ + (13122 \cdot x^7 + 952560 \cdot x^3) \cdot \underline{T}_{4, i_1+2}^{\cos, 0}(3x) \\ + (252 \cdot x^6 + 423360 \cdot x^2) \cdot \underline{T}_{4, i_2+3}^{\sin, 0}(x) \\ + (x^{11} + 2520 \cdot x^5 + 1088640 \cdot x) \cdot \underline{T}_{4, i_3+2}^{\cos, 0}(x), $$

$$ P_{i_4, i_5, i_6, i_7}^{-}(x) = (-61236 \cdot x^6 - 1270080 \cdot x^2) \cdot \overline{T}_{4, i_4+1}^{\sin, 0}(3x) \\ + (-204120 \cdot x^5 - 1088640 \cdot x) \cdot \overline{T}_{4, i_5}^{\cos, 0}(3x) \\ + (-\frac{3}{4} \cdot x^8 - 18900 \cdot x^4 - 1360800) \cdot \overline{T}_{4, i_6+1}^{\sin, 0}(x) \\ + (-18 \cdot x^7 - 105840 \cdot x^3) \cdot \overline{T}_{4, i_7}^{\cos, 0}(x). $$

For concrete indices $(i_0, i_1, i_2, i_3, i_4, i_5, i_6, i_7) = (3, 4, 1, 2, 4, 4, 2, 2)$, we obtain

$$ P_{3,4,1,2}^{+}(x) = \left( \frac{6561}{4} \cdot x^8 + 510300 \cdot x^4 + 453600 \right) \cdot \underline{T}_{4,3+3}^{\sin, 0}(3x) \\ + (13122 \cdot x^7 + 952560 \cdot x^3) \cdot \underline{T}_{4,4+2}^{\cos, 0}(3x) \\ + (252 \cdot x^6 + 423360 \cdot x^2) \cdot \underline{T}_{4,1+3}^{\sin, 0}(x) \\ + (x^{11} + 2520 \cdot x^5 + 1088640 \cdot x) \cdot \underline{T}_{4,2+2}^{\cos, 0}(x), $$

$$ P_{3,4,1,2}^{+}(x) = -\frac{387420489}{487911424000} \cdot x^{25} + \frac{129140163}{14350336000} \cdot x^{23} - \frac{2208298489}{6175128960} \cdot x^{21} \\ + \frac{129141043}{35481600} \cdot x^{19} - \frac{760514951}{16473600} \cdot x^{17} + \frac{607555181}{2882880} \cdot x^{15} \\ + \frac{53310093}{22880} \cdot x^{13} - \frac{13876823}{440} \cdot x^{11} + 39372 \cdot x^9 + 735840 \cdot x^7 \\ -1859760 \cdot x^5 - 1209600 \cdot x^3 + 2449440 \cdot x $$

and

$$ P_{4,4,2,2}^{-}(x) = (-61236 \cdot x^6 - 1270080 \cdot x^2) \cdot \overline{T}_{4,4+1}^{\sin, 0}(3x) \\ + (-204120 \cdot x^5 - 1088640 \cdot x) \cdot \overline{T}_{4,4}^{\cos, 0}(3x) \\ + (-\frac{3}{4} \cdot x^8 - 18900 \cdot x^4 - 1360800) \cdot \overline{T}_{4,2+1}^{\sin, 0}(x) \\ + (-18 \cdot x^7 - 105840 \cdot x^3) \cdot \overline{T}_{4,2}^{\cos, 0}(x), $$

$$ P_{4,4,2,2}^{-}(x) = -\frac{387420489}{17425408000} \cdot x^{23} + \frac{129140163}{512512000} \cdot x^{21} - \frac{43046721}{8712704} \cdot x^{19} \\ + \frac{19715397503}{345945600} \cdot x^{17} - \frac{127545983}{480480} \cdot x^{15} - \frac{531449}{240} \cdot x^{13} \\ + \frac{314933}{10} \cdot x^{11} - 39372 \cdot x^9 - 735840 \cdot x^7 \\ +1859760 \cdot x^5 + 1209600 \cdot x^3 - 2449440 \cdot x. $$

Finally, for the MTP function

$$ f(x) = f^{+}(x) + f^{-}(x) $$
tions, we obtain downward polynomial approximations of $f^+(x)$ and $f^-(x)$ respectively

$$ P_{i_0, i_1, i_2, i_3}^{+}(x) = \left( \frac{6561}{4} x^8 + 510300 x^4 + 453600 \right) \cdot \underline{T}_{4, i_0+3}^{\sin, 0}(3x) \\ + (13122 \cdot x^7 + 952560 \cdot x^3) \cdot \underline{T}_{4, i_1+2}^{\cos, 0}(3x) \\ + (252 \cdot x^6 + 423360 \cdot x^2) \cdot \underline{T}_{4, i_2+3}^{\sin, 0}(x) \\ + (x^{11} + 2520 \cdot x^5 + 1088640 \cdot x) \cdot \underline{T}_{4, i_3+2}^{\cos, 0}(x), $$

$$ P_{i_4, i_5, i_6, i_7}^{-}(x) = (-61236 \cdot x^6 - 1270080 \cdot x^2) \cdot \overline{T}_{4, i_4+1}^{\sin, 0}(3x) \\ + (-204120 \cdot x^5 - 1088640 \cdot x) \cdot \overline{T}_{4, i_5}^{\cos, 0}(3x) \\ + (-\frac{3}{4} \cdot x^8 - 18900 \cdot x^4 - 1360800) \cdot \overline{T}_{4, i_6+1}^{\sin, 0}(x) \\ + (-18 \cdot x^7 - 105840 \cdot x^3) \cdot \overline{T}_{4, i_7}^{\cos, 0}(x). $$

For concrete indices $(i_0, i_1, i_2, i_3, i_4, i_5, i_6, i_7) = (3, 4, 1, 2, 4, 4, 2, 2)$, we obtain

$$ P_{3,4,1,2}^{+}(x) = \left( \frac{6561}{4} x^8 + 510300 x^4 + 453600 \right) \cdot \underline{T}_{4,3+3}^{\sin, 0}(3x) \\ + (13122 \cdot x^7 + 952560 \cdot x^3) \cdot \underline{T}_{4,4+2}^{\cos, 0}(3x) \\ + (252 \cdot x^6 + 423360 \cdot x^2) \cdot \underline{T}_{4,1+3}^{\sin, 0}(x) \\ + (x^{11} + 2520 \cdot x^5 + 1088640 \cdot x) \cdot \underline{T}_{4,2+2}^{\cos, 0}(x), $$

$$ P_{3,4,1,2}^{+}(x) = -\frac{387420489}{487911424000} \cdot x^{25} + \frac{129140163}{14350336000} \cdot x^{23} - \frac{2208298489}{6175128960} \cdot x^{21} \\ + \frac{129141043}{35481600} \cdot x^{19} - \frac{760514951}{16473600} \cdot x^{17} + \frac{607555181}{2882880} \cdot x^{15} \\ + \frac{53310093}{22880} \cdot x^{13} - \frac{13876823}{440} \cdot x^{11} + 39372 \cdot x^9 + 735840 \cdot x^7 \\ -1859760 \cdot x^5 - 1209600 \cdot x^3 + 2449440 \cdot x $$

and

$$ P_{4,4,2,2}^{-}(x) = (-61236 \cdot x^6 - 1270080 \cdot x^2) \cdot \overline{T}_{4,4+1}^{\sin, 0}(3x) \\ + (-204120 \cdot x^5 - 1088640 \cdot x) \cdot \overline{T}_{4,4}^{\cos, 0}(3x) \\ + (-\frac{3}{4} \cdot x^8 - 18900 \cdot x^4 - 1360800) \cdot \overline{T}_{4,2+1}^{\sin, 0}(x) \\ + (-18 \cdot x^7 - 105840 \cdot x^3) \cdot \overline{T}_{4,2}^{\cos, 0}(x), $$

$$ P_{4,4,2,2}^{-}(x) = -\frac{387420489}{17425408000} \cdot x^{23} + \frac{129140163}{512512000} \cdot x^{21} - \frac{43046721}{8712704} \cdot x^{19} \\ + \frac{19715397503}{345945600} \cdot x^{17} - \frac{127545983}{480480} \cdot x^{15} - \frac{531449}{240} \cdot x^{13} \\ + \frac{314933}{10} \cdot x^{11} - 39372 \cdot x^9 - 735840 \cdot x^7 \\ + 1859760 \cdot x^5 + 1209600 \cdot x^3 - 2449440 \cdot x. $$

Finally, for the MTP function

$$ f(x) = f^{+}(x) + f^{-}(x) $$
we obtain the concrete downward polynomial approximation

$$
\begin{align*}
P(x) &= P_{3,4,1,2}^{+}(x) + P_{4,4,2,2}^{-}(x) \\
&= -\frac{387420489}{487911424000} \cdot x^{25} - \frac{129140163}{9758228480} \cdot x^{23} - \frac{521856760043}{4940103168000} \cdot x^{21} \\
&\quad -\frac{10201878397}{7841433600} \cdot x^{19} + \frac{936145883}{86486400} \cdot x^{17} - \frac{2048321}{37440} \cdot x^{15} \\
&\quad + \frac{1587173}{13728} \cdot x^{13} - \frac{19771}{440} \cdot x^{11}
\end{align*}
$$

over $[1, \frac{\pi}{2}]$, i.e. it holds that

$f(x) > P(x)$

over $[1, \frac{\pi}{2}]$.

IV (The final part) Based on the Sturm theorem, the following inequality

$P(x) > 0$

is true over $[1, \frac{\pi}{2}]$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ does not have zero over the concrete extended segment $[1, 1.58]$ of the initial interval $[1, \frac{\pi}{2}]$.

2. Facts $P(1) \neq 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2} (P(\frac{\pi}{2}) = 1228.02881... > 0)$.
Therefore, the following inequality

$f(x) > 0$

is true over $[1, \frac{\pi}{2}]$. $\square$

APPENDIX A4

The initial MTP function is

$$f(x) = x^{5} - 360 \cdot x + (-30 \cdot x^{2} + 630) \cdot \sin x - 270 \cdot x \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.

Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

I (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 0.054404... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

II (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = (-30 \cdot x^{2} + 630) \cdot \sin x - 270 \cdot x \cdot \cos x + x^{5} - 360 \cdot x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = 630 \cdot \sin x + x^{5},$$

$$f^{-}(x) = -360 \cdot x - 270 \cdot x \cdot \cos x - 30 \cdot x^{2} \cdot \sin x.$$
we obtain the concrete downward polynomial approximation

$$
\begin{align*}
P(x) &= P_{3,4,1,2}^{+}(x) + P_{4,4,2,2}^{-}(x) \\
&= -\frac{387420489}{487911424000} \cdot x^{25} - \frac{129140163}{9758228480} \cdot x^{23} - \frac{521856760043}{4940103168000} \cdot x^{21} \\
&\quad -\frac{10201878397}{7841433600} \cdot x^{19} + \frac{936145883}{86486400} \cdot x^{17} - \frac{2048321}{37440} \cdot x^{15} \\
&\quad + \frac{1587173}{13728} \cdot x^{13} - \frac{19771}{440} \cdot x^{11}
\end{align*}
$$

over $[1, \frac{\pi}{2}]$, i.e. it holds that

$f(x) > P(x)$

over $[1, \frac{\pi}{2}]$.

IV (The final part) Based on the Sturm theorem, the following inequality

$P(x) > 0$

is true over $[1, \frac{\pi}{2}]$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ does not have zero over the concrete extended segment $[1, 1.58]$ of the initial interval $[1, \frac{\pi}{2}]$.

2. Facts $P(1) \neq 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2} (P(\frac{\pi}{2}) = 1228.02881... > 0)$.
Therefore, the following inequality

$f(x) > 0$

is true over $[1, \frac{\pi}{2}]$. $\square$

APPENDIX A4

The initial MTP function is

$$f(x) = x^{5} - 360 \cdot x + (-30 \cdot x^{2} + 630) \cdot \sin x - 270 \cdot x \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.

Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

I (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 0.054404... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

II (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = (-30 \cdot x^{2} + 630) \cdot \sin x - 270 \cdot x \cdot \cos x + x^{5} - 360 \cdot x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = 630 \cdot \sin x + x^{5},$$

$$f^{-}(x) = -360 \cdot x - 270 \cdot x \cdot \cos x - 30 \cdot x^{2} \cdot \sin x.$$
### III (Determination of downward rational polynomial approximation)
After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^+(x)$ and $f^-(x)$ respectively

$$P_{i_0}^+(x) = 630 \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin, 0}(x) + x^5,$$

$$P_{i_1, i_2}^-(x) = -360 \cdot x - 270 \cdot x \cdot \overline{T}_{4 \cdot i_1}^{\cos, 0}(x) - 30 \cdot x^2 \cdot \overline{T}_{4 \cdot i_2 + 1}^{\sin, 0}(x).$$

For concrete indices $(i_0, i_1, i_2) = (2, 2, 2)$, we obtain

$$P_2^+(x) = 630 \cdot \underline{T}_{4 \cdot 2 + 3}^{\sin, 0}(x) + x^5,$$

$$P_2^+(x) = -\frac{1}{63360} \cdot x^{11} + \frac{1}{576} \cdot x^9 - \frac{1}{8} \cdot x^7 + \frac{25}{4} \cdot x^5 - 105 \cdot x^3 + 630 \cdot x$$

and

$$P_{2,2}^-(x) = -360 \cdot x - 270 \cdot x \cdot \overline{T}_{4 \cdot 2}^{\cos, 0}(x) - 30 \cdot x^2 \cdot \overline{T}_{4 \cdot 2 + 1}^{\sin, 0}(x),$$

$$P_{2,2}^-(x) = -\frac{1}{12096} \cdot x^{11} - \frac{1}{1344} \cdot x^9 + \frac{1}{8} \cdot x^7 - \frac{25}{4} \cdot x^5 + 105 \cdot x^3 - 630 \cdot x.$$

Finally, for the MTP function

$$f(x) = f^+(x) + f^-(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_2^+(x) + P_{2,2}^-(x) \\ = -\frac{131}{1330560} \cdot x^{11} + \frac{1}{1008} \cdot x^9$$

over $(0, \frac{\pi}{2})$, i.e. it holds that

$$f(x) > P(x)$$

over $(0, \frac{\pi}{2})$.

### IV (The final part)
Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over $(0, \frac{\pi}{2})$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ has only one zero over the concrete extended segment $[-0.1, 1.58]$ of the initial interval $(0, \frac{\pi}{2})$.

2. Facts $P(-0.1) \neq 0$, $P(0) = 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2} (P(\frac{\pi}{2}) = 0.043615... > 0)$.
Therefore, the following inequality

$$f(x) > 0$$

is true over $(0, \frac{\pi}{2})$. $\square$

## APPENDIX A5

The initial MTP function is

$$f(x) = (x^8 - 21 \cdot x^6 + 630 \cdot x^4 - 7560 \cdot x^2 + 15120) \cdot \sin x \\ + (3 \cdot x^7 - 126 \cdot x^5 + 2520 \cdot x^3 - 15120 \cdot x) \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.
### III (Determination of downward rational polynomial approximation)
After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^+(x)$ and $f^-(x)$ respectively

$$P_{i_0}^+(x) = 630 \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin, 0}(x) + x^5,$$

$$P_{i_1, i_2}^-(x) = -360 \cdot x - 270 \cdot x \cdot \overline{T}_{4 \cdot i_1}^{\cos, 0}(x) - 30 \cdot x^2 \cdot \overline{T}_{4 \cdot i_2 + 1}^{\sin, 0}(x).$$

For concrete indices $(i_0, i_1, i_2) = (2, 2, 2)$, we obtain

$$P_2^+(x) = 630 \cdot \underline{T}_{4 \cdot 2 + 3}^{\sin, 0}(x) + x^5,$$

$$P_2^+(x) = -\frac{1}{63360} \cdot x^{11} + \frac{1}{576} \cdot x^9 - \frac{1}{8} \cdot x^7 + \frac{25}{4} \cdot x^5 - 105 \cdot x^3 + 630 \cdot x$$

and

$$P_{2,2}^-(x) = -360 \cdot x - 270 \cdot x \cdot \overline{T}_{4 \cdot 2}^{\cos, 0}(x) - 30 \cdot x^2 \cdot \overline{T}_{4 \cdot 2 + 1}^{\sin, 0}(x),$$

$$P_{2,2}^-(x) = -\frac{1}{12096} \cdot x^{11} - \frac{1}{1344} \cdot x^9 + \frac{1}{8} \cdot x^7 - \frac{25}{4} \cdot x^5 + 105 \cdot x^3 - 630 \cdot x.$$

Finally, for the MTP function

$$f(x) = f^+(x) + f^-(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_2^+(x) + P_{2,2}^-(x) \\ = -\frac{131}{1330560} \cdot x^{11} + \frac{1}{1008} \cdot x^9$$

over $(0, \frac{\pi}{2})$, i.e. it holds that

$$f(x) > P(x)$$

over $(0, \frac{\pi}{2})$.

### IV (The final part)
Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over $(0, \frac{\pi}{2})$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ has only one zero over the concrete extended segment $[-0.1, 1.58]$ of the initial interval $(0, \frac{\pi}{2})$.

2. Facts $P(-0.1) \neq 0$, $P(0) = 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2} (P(\frac{\pi}{2}) = 0.043615... > 0)$.
Therefore, the following inequality

$$f(x) > 0$$

is true over $(0, \frac{\pi}{2})$.

□

## APPENDIX A5

The initial MTP function is

$$f(x) = (x^8 - 21 \cdot x^6 + 630 \cdot x^4 - 7560 \cdot x^2 + 15120) \cdot \sin x \\ + (3 \cdot x^7 - 126 \cdot x^5 + 2520 \cdot x^3 - 15120 \cdot x) \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.
Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

**I** (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 23.53938... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

**II** (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = (x^8 - 21 \cdot x^6 + 630 \cdot x^4 - 7560 \cdot x^2 + 15120) \cdot \sin x + (3 \cdot x^7 - 126 \cdot x^5 + 2520 \cdot x^3 - 15120 \cdot x) \cdot \cos x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = (x^{8} + 630 \cdot x^{4} + 15120) \cdot \sin x + (3 \cdot x^{7} + 2520 \cdot x^{3}) \cdot \cos x,$$

$$f^{-}(x) = (-126 \cdot x^{5} - 15120 \cdot x) \cdot \cos x + (-21 \cdot x^{6} - 7560 \cdot x^{2}) \cdot \sin x.$$

**III** (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^{+}(x)$ and $f^{-}(x)$ respectively

$$P_{i_0, i_1}^{+}(x) = (x^8 + 630 \cdot x^4 + 15120) \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin, 0}(x) + (3 \cdot x^7 + 2520 \cdot x^3) \cdot \underline{T}_{4 \cdot i_1 + 2}^{\cos, 0}(x),$$

$$P_{i_2, i_3}^{-}(x) = (-126 \cdot x^{5} - 15120 \cdot x) \cdot \overline{T}_{4 \cdot i_2}^{\cos, 0}(x) + (-21 \cdot x^{6} - 7560 \cdot x^{2}) \cdot \overline{T}_{4 \cdot i_3 + 1}^{\sin, 0}(x).$$

For concrete indices $(i_0, i_1, i_2, i_3) = (1, 1, 2, 2)$, we obtain

$$P_{1,1}^{+}(x) = (x^{8} + 630 \cdot x^{4} + 15120) \cdot \underline{T}_{4 \cdot 1 + 3}^{\sin, 0}(x) + (3 \cdot x^{7} + 2520 \cdot x^{3}) \cdot \underline{T}_{4 \cdot 1 + 2}^{\cos, 0}(x),$$

$$P_{1,1}^{+}(x) = -\frac{1}{5040} \cdot x^{15} + \frac{1}{240} \cdot x^{13} - \frac{1}{6} \cdot x^{11} + \frac{5}{4} \cdot x^{9} - 504 \cdot x^{5} + 15120 \cdot x$$

and

$$P_{2,2}^{-}(x) = (-126 \cdot x^{5} - 15120 \cdot x) \cdot \overline{T}_{4 \cdot 2}^{\cos, 0}(x) + (-21 \cdot x^{6} - 7560 \cdot x^{2}) \cdot \overline{T}_{4 \cdot 2 + 1}^{\sin, 0}(x),$$

$$P_{2,2}^{-}(x) = -\frac{1}{17280} \cdot x^{15} + \frac{1}{960} \cdot x^{13} - \frac{1}{48} \cdot x^{11} - \frac{5}{8} \cdot x^{9} + 504 \cdot x^{5} - 15120 \cdot x.$$

Finally, for the MTP function

$$f(x) = f^{+}(x) + f^{-}(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_{1,1}^{+}(x) + P_{2,2}^{-}(x)$$

$$= -\frac{31}{120960} \cdot x^{15} + \frac{1}{192} \cdot x^{13} - \frac{3}{16} \cdot x^{11} + \frac{5}{8} \cdot x^{9}$$

over $(0, \frac{\pi}{2})$, i.e. it holds that

$$f(x) > P(x)$$

over $(0, \frac{\pi}{2})$.
Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

**I** (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 23.53938... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

**II** (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = (x^8 - 21 \cdot x^6 + 630 \cdot x^4 - 7560 \cdot x^2 + 15120) \cdot \sin x + (3 \cdot x^7 - 126 \cdot x^5 + 2520 \cdot x^3 - 15120 \cdot x) \cdot \cos x.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = (x^{8} + 630 \cdot x^{4} + 15120) \cdot \sin x + (3 \cdot x^{7} + 2520 \cdot x^{3}) \cdot \cos x,$$

$$f^{-}(x) = (-126 \cdot x^{5} - 15120 \cdot x) \cdot \cos x + (-21 \cdot x^{6} - 7560 \cdot x^{2}) \cdot \sin x.$$

**III** (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^{+}(x)$ and $f^{-}(x)$ respectively

$$P_{i_0, i_1}^{+}(x) = (x^8 + 630 \cdot x^4 + 15120) \cdot \underline{T}_{4 \cdot i_0 + 3}^{\sin, 0}(x) + (3 \cdot x^7 + 2520 \cdot x^3) \cdot \underline{T}_{4 \cdot i_1 + 2}^{\cos, 0}(x),$$

$$P_{i_2, i_3}^{-}(x) = (-126 \cdot x^{5} - 15120 \cdot x) \cdot \overline{T}_{4 \cdot i_2}^{\cos, 0}(x) + (-21 \cdot x^{6} - 7560 \cdot x^{2}) \cdot \overline{T}_{4 \cdot i_3 + 1}^{\sin, 0}(x).$$

For concrete indices $(i_0, i_1, i_2, i_3) = (1, 1, 2, 2)$, we obtain

$$P_{1,1}^{+}(x) = (x^8 + 630 \cdot x^4 + 15120) \cdot \underline{T}_{4 \cdot 1 + 3}^{\sin, 0}(x) + (3 \cdot x^7 + 2520 \cdot x^3) \cdot \underline{T}_{4 \cdot 1 + 2}^{\cos, 0}(x),$$

$$P_{1,1}^{+}(x) = -\frac{1}{5040} \cdot x^{15} + \frac{1}{240} \cdot x^{13} - \frac{1}{6} \cdot x^{11} + \frac{5}{4} \cdot x^{9} - 504 \cdot x^{5} + 15120 \cdot x$$

and

$$P_{2,2}^{-}(x) = (-126 \cdot x^{5} - 15120 \cdot x) \cdot \overline{T}_{4 \cdot 2}^{\cos, 0}(x) + (-21 \cdot x^{6} - 7560 \cdot x^{2}) \cdot \overline{T}_{4 \cdot 2 + 1}^{\sin, 0}(x),$$

$$P_{2,2}^{-}(x) = -\frac{1}{17280} \cdot x^{15} + \frac{1}{960} \cdot x^{13} - \frac{1}{48} \cdot x^{11} - \frac{5}{8} \cdot x^{9} + 504 \cdot x^{5} - 15120 \cdot x.$$

Finally, for the MTP function

$$f(x) = f^{+}(x) + f^{-}(x)$$

we obtain the concrete downward polynomial approximation

$$P(x) = P_{1,1}^{+}(x) + P_{2,2}^{-}(x)$$

$$= -\frac{31}{120960} \cdot x^{15} + \frac{1}{192} \cdot x^{13} - \frac{3}{16} \cdot x^{11} + \frac{5}{8} \cdot x^{9}$$

over $(0, \frac{\pi}{2})$, i.e. it holds that

$$f(x) > P(x)$$

over $(0, \frac{\pi}{2})$.
IV (The final part) Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over $(0, \frac{\pi}{2})$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ has only one zero over the concrete extended segment $[-0.1, 1.58]$ of the initial interval $(0, \frac{\pi}{2})$.

2. Facts $P(-0.1) \neq 0$, $P(0) = 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2}$ ($P(\frac{\pi}{2}) = 11.074847... > 0$).

Therefore, the following inequality

$$f(x) > 0$$

is true over $(0, \pi/2)$.

□

APPENDIX A6

The initial MTP function is

$$f(x) = 3 \cdot x^5 - 20 \cdot x - 140 \cdot \sin x \cdot \cos x + (30 \cdot x^2 - 70) \cdot \sin x + 40 \cdot x \cdot \cos^2 x + 190 \cdot x \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.

Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

I (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 1.29545... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

II (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = -70 \cdot \sin 2x + 20 \cdot x \cdot \cos 2x + (30 \cdot x^2 - 70) \cdot \sin x + 190 \cdot x \cdot \cos x + 3 \cdot x^5.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = 190 \cdot x \cdot \cos x + 20 \cdot x \cdot \cos 2x + 30 \cdot x^2 \cdot \sin x + 3 \cdot x^5,$$

$$f^{-}(x) = -70 \cdot \sin x - 70 \cdot \sin 2x.$$

III (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^{+}(x)$ and $f^{-}(x)$ respectively

$$P_{i_0, i_1, i_2}^{+}(x) = 190 \cdot x \cdot \frac{\cos 0}{4 \cdot i_0 + 2}(x) + 20 \cdot x \cdot \frac{\cos 0}{4 \cdot i_1 + 2}(2x) + 30 \cdot x^2 \cdot \frac{\sin 0}{4 \cdot i_2 + 3}(x) + 3 \cdot x^5,$$

$$P_{i_3, i_4}^{-}(x) = -70 \cdot \frac{\sin 0}{4 \cdot i_3 + 1}(x) - 70 \cdot \frac{\sin 0}{4 \cdot i_4 + 1}(2x).$$
IV (The final part) Based on the Sturm theorem, the following inequality

$$P(x) > 0$$

is true over $(0, \frac{\pi}{2})$. The stated conclusion for the polynomial function $P$ is correct based on the following facts:

1. We can conclude, by Sturm theorem, that the polynomial function $P(x)$ has only one zero over the concrete extended segment $[-0.1, 1.58]$ of the initial interval $(0, \frac{\pi}{2})$.

2. Facts $P(-0.1) \neq 0$, $P(0) = 0$ and $P(1.58) \neq 0$ are correct.

3. The polynomial $P$ is positive at boundary point $\frac{\pi}{2}$ ($P(\frac{\pi}{2}) = 11.074847... > 0$).

Therefore, the following inequality

$$f(x) > 0$$

is true over $(0, \pi/2)$.

☐

APPENDIX A6

The initial MTP function is

$$f(x) = 3 \cdot x^5 - 20 \cdot x - 140 \cdot \sin x \cdot \cos x + (30 \cdot x^2 - 70) \cdot \sin x + 40 \cdot x \cdot \cos^2 x + 190 \cdot x \cdot \cos x$$

and the initial interval is $S = (0, \frac{\pi}{2})$.

Automated proof that $f(x) > 0$ for $x \in (0, \frac{\pi}{2})$:

I (Recognition of possible case) Facts $f(0) = 0$ and $f(\frac{\pi}{2}) \neq 0$ are correct. The MTP function $f$ is positive at boundary point $\frac{\pi}{2}$ ($f(\frac{\pi}{2}) = 1.29545... > 0$). Therefore, it is possible that $f(x) > 0$ over $(0, \frac{\pi}{2})$.

II (Transformation of angles) After the transformation of terms $\cos^m x \cdot \sin^n x$ ($m, n \in N_0$) into the sum of sine and cosine functions of multiple angles, in the MTP function $f$, we obtain

$$f(x) = -70 \cdot \sin 2x + 20 \cdot x \cdot \cos 2x + (30 \cdot x^2 - 70) \cdot \sin x + 190 \cdot x \cdot \cos x + 3 \cdot x^5.$$

Then, we consider the previous expression as two separate expressions, the first with positive and the second with negative terms next to sine and cosine functions

$$f^{+}(x) = 190 \cdot x \cdot \cos x + 20 \cdot x \cdot \cos 2x + 30 \cdot x^2 \cdot \sin x + 3 \cdot x^5,$$

$$f^{-}(x) = -70 \cdot \sin x - 70 \cdot \sin 2x.$$

III (Determination of downward rational polynomial approximation) After substitution of sine and cosine functions by appropriate (downward or upward) polynomial approximations, we obtain downward polynomial approximations of $f^{+}(x)$ and $f^{-}(x)$ respectively

$$P_{i_0, i_1, i_2}^{+}(x) = 190 \cdot x \cdot \frac{\cos 0}{4 \cdot i_0 + 2}(x) + 20 \cdot x \cdot \frac{\cos 0}{4 \cdot i_1 + 2}(2x) + 30 \cdot x^2 \cdot \frac{\sin 0}{4 \cdot i_2 + 3}(x) + 3 \cdot x^5,$$

$$P_{i_3, i_4}^{-}(x) = -70 \cdot \frac{\sin 0}{4 \cdot i_3 + 1}(x) - 70 \cdot \frac{\sin 0}{4 \cdot i_4 + 1}(2x).$$