Does $\min |{\cos(n)}|$ exist? Let $f:\mathbb{Z^+}\rightarrow \mathbb{R}$ where $f(n)=|\cos(n)|$ in radians. Does $\min f$ exist?
I think the answer is no and I that have the right approach to proving it.
From Dirichlet approximation theorem we know we can find integers $p$ and $q$ such that $|\frac{\pi}{2}-\frac{p}{q}|<\frac{1}{q^2}\implies |\frac{q\pi}{2}-p|\lt\frac{1}{q}$ so let $p_n$ be our candidate and $q_n=2k+1$(some increasing odd integer for each $n$, and although this could be an interesting question on its own, I think I'm safe to assume it. As we get close to $\frac{\pi}{2}$, the rational approximations have very large numerators and denominators) then $|(2k+1)\frac{\pi}{2}-p_n|\rightarrow 0$ (monotone decreasing) and since the $2k$ term does nothing in $\cos p_n$, we get $\lim \cos(p_n)=0$. Now it remains to show we don't hit zero inbetween, but we can probably choose $p_n$ so that this doesn't happen.
Does this work? Is there a way to do this without Dirichlet?
 A: Your method works. Here is the complete proof.
First, we prove that $$   \inf_{n\in \Bbb Z^*}|\cos(n)| = 0 \tag{1}$$
If we can construct a sequence $\{u_t\}_{t \in \Bbb N^*}\in \Bbb Z^*$ such that
$$u_t \equiv\frac{\pi}{2} +\epsilon_t \pmod{\pi} \tag{2}$$
where $ \epsilon_t \xrightarrow{t\to +\infty}0$, then $|\cos(u_t)| \xrightarrow{t\to +\infty}0$. In other words, $(1)$ holds true (because $|\cos(n)| \ge 0$).
$(2)$ is equivalent to find the sequence $\{(u_t,v_t)\}_{t \in \Bbb N^*} \in (\mathbb{Z},\mathbb{Z})$ such that
$$\left|u_t -\frac{\pi}{2} -\pi v_t\right|\xrightarrow{t\to +\infty}0\iff \left|\frac{u_t -\frac{\pi}{2}}{v_t} -\pi \right|\xrightarrow{t\to +\infty}0 \tag{3}$$
According to the Dirichlet's approximation theorem
, there exists the sequence $\{(u_t,v_t)\}_{t \in \Bbb N^*}$ such that
$$\left|\frac{u_t}{v_t}-\pi \right| \le \frac{1}{v_t^2} \tag{4}$$
Applying $(4)$ to $(3)$ with a sub-sequence of increasing value of $v_{\sigma(t)}$ (for the sake of simplicity, we abuse the notation and still write $v_t$ instead of $v_{\sigma(t)}$), we have
$$\left|\frac{u_t -\frac{\pi}{2}}{v_t} -\pi \right| \le\left|\frac{u_t }{v_t} -\pi \right| + \frac{\pi}{2}\frac{1}{v_t} \le \left(\frac{1}{v_t^2}+\frac{\pi}{2}\frac{1}{v_t} \right)\xrightarrow{v_t\to +\infty} 0$$
Hence, $(1)$ holds true. We can conclude that $ \inf f = 0$
Second, we prove that there doesn't exist $n$ such that $\cos(n) = 0$. It's straightforward because if not, there existed $m \in \Bbb Z$ such that
$$n = \frac{\pi}{2} + m\pi$$
or $$\pi = \frac{n}{\frac{1}{2}+m} \in \Bbb Q$$
which is a contracdiction. We can conclude that $\min f$ doesn't existe
PS: about the last question whether there exists another proof without using the Dirichlet's approximation theorem, I haven't yet this proof without using the Dirichlet's approximation theorem.
A: If a set $S\subset \Bbb R$ has a smallest element $s$, then $\min S=s$. If $S$ has no smallest element, then $\min S$ is undefined.
By contrast, the infimum $\inf S$ of a set $S$ is defined as the largest $x\in\Bbb R$ such that $x\le s$ for every $s\in S$. Thus, for instance, the infimum of $(0,1)$ is $0$, although this set has no minimum element.
So now we can say that if $S=\{|\cos n|\;:\;n\in\Bbb Z\}$, then $\inf S=0$; but $\min S$ is undefined, because $|\cos n|$ is non-zero for all integers $n$.
A: Let $n$ be any fixed natural number. We first note that $n$ can never be an odd multiple of $\frac{\pi}{2}$.
WLOG let the nearest odd multiple of $\frac{\pi}{2}$ to $n$ be $ < n$. Let this odd multiple be denoted by $\pi_n$ and let this distance be $d_n = n - \pi_n$. Now let the decimal expansion of $\pi$ be $3\cdot a_1 a_2 .. a_i .. $. As this series converges to $\pi$, there exists $r \geq 1$ s.t. $d_n > 3 - (3\cdot a_1 a_2 .. a_r)$. Then we can see that the number $n + 3\cdot a_1 a_2 .. a_r \times 10^r$ is closer to $\pi_n + \pi*10^r$ than $n$ is closer to $\pi_n$. Formally:
$$
\begin{align*}
0 < n + 3\cdot a_1 a_2 .. a_r \times 10^r - (\pi_n + \pi*10^r) 
&= d_n - (0.a_{r+1} a_{r+2} ...)  < d_n
\end{align*}
 $$
Hence for any $n$, I've found a another $n' = n + 3\cdot a_1 a_2 .. a_r \times 10^r$ with a smaller value of $|\cos(n)|$, as it's closer to an odd multiple of $\frac{\pi}{2}$ (this can be formalized by the continuity of $|\cos x|$ and noting that $\cos(n) = \cos(\frac{\pi}{2} + d_n) \land \cos(n') = \cos(\frac{\pi}{2}+ d_{n'}) $ where $0 < d_{n'} < d_n$). For the $ > n$ case, we subtract $\pi * 10^r$ instead of adding.
