Theorem taupilem2

Description: Lemma for taupi . The smallest positive real whose cosine is one is at most 2 x. _pi . (Contributed by Jim Kingdon, 19-Feb-2019) (Revised by AV, 1-Oct-2020)

	Ref	Expression
Assertion	taupilem2	$$⊢\mathrm{\tau }\le 2\mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		df-tau	$$⊢\mathrm{\tau }=inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)$$
2		inss1	$$⊢{ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\subseteq {ℝ}^{+}$$
3		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
4	2 3	sstri	$$⊢{ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\subseteq ℝ$$
5		taupilemrplb	$$⊢\exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)x\le y$$
6		2rp	$$⊢2\in {ℝ}^{+}$$
7		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
8		rpmulcl	$$⊢\left(2\in {ℝ}^{+}\wedge \mathrm{\pi }\in {ℝ}^{+}\right)\to 2\mathrm{\pi }\in {ℝ}^{+}$$
9	6 7 8	mp2an	$$⊢2\mathrm{\pi }\in {ℝ}^{+}$$
10		cos2pi	$$⊢\cos 2\mathrm{\pi }=1$$
11		taupilem3	$$⊢2\mathrm{\pi }\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)\leftrightarrow \left(2\mathrm{\pi }\in {ℝ}^{+}\wedge \cos 2\mathrm{\pi }=1\right)$$
12	9 10 11	mpbir2an	$$⊢2\mathrm{\pi }\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)$$
13		infrelb	$$⊢\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\subseteq ℝ\wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)x\le y\wedge 2\mathrm{\pi }\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)\right)\to inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)\le 2\mathrm{\pi }$$
14	4 5 12 13	mp3an	$$⊢inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)\le 2\mathrm{\pi }$$
15	1 14	eqbrtri	$$⊢\mathrm{\tau }\le 2\mathrm{\pi }$$