Theorem taupi

Description: Relationship between _tau and _pi . This can be seen as connecting the ratio of a circle's circumference to its radius and the ratio of a circle's circumference to its diameter. (Contributed by Jim Kingdon, 19-Feb-2019) (Revised by AV, 1-Oct-2020)

	Ref	Expression
Assertion	taupi	$$⊢\mathrm{\tau }=2\mathrm{\pi }$$

Proof

Step	Hyp	Ref	Expression
1		taupilem2	$$⊢\mathrm{\tau }\le 2\mathrm{\pi }$$
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		2rp	$$⊢2\in {ℝ}^{+}$$
6		pirp	$$⊢\mathrm{\pi }\in {ℝ}^{+}$$
7		rpmulcl	$$⊢\left(2\in {ℝ}^{+}\wedge \mathrm{\pi }\in {ℝ}^{+}\right)\to 2\mathrm{\pi }\in {ℝ}^{+}$$
8	5 6 7	mp2an	$$⊢2\mathrm{\pi }\in {ℝ}^{+}$$
9		cos2pi	$$⊢\cos 2\mathrm{\pi }=1$$
10		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)$$
11	8 9 10	mpbir2an	$$⊢2\mathrm{\pi }\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)$$
12	11	ne0ii	$$⊢{ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\ne \varnothing$$
13		taupilemrplb	$$⊢\exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)x\le y$$
14	4 12 13	3pm3.2i	$$⊢\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\ne \varnothing \wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)x\le y\right)$$
15		2re	$$⊢2\in ℝ$$
16		pire	$$⊢\mathrm{\pi }\in ℝ$$
17	15 16	remulcli	$$⊢2\mathrm{\pi }\in ℝ$$
18		infregelb	$$⊢\left(\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\ne \varnothing \wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)x\le y\right)\wedge 2\mathrm{\pi }\in ℝ\right)\to \left(2\mathrm{\pi }\le inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)\leftrightarrow \forall x\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)2\mathrm{\pi }\le x\right)$$
19	14 17 18	mp2an	$$⊢2\mathrm{\pi }\le inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)\leftrightarrow \forall x\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)2\mathrm{\pi }\le x$$
20		taupilem3	$$⊢x\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)\leftrightarrow \left(x\in {ℝ}^{+}\wedge \cos x=1\right)$$
21		taupilem1	$$⊢\left(x\in {ℝ}^{+}\wedge \cos x=1\right)\to 2\mathrm{\pi }\le x$$
22	20 21	sylbi	$$⊢x\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)\to 2\mathrm{\pi }\le x$$
23	19 22	mprgbir	$$⊢2\mathrm{\pi }\le inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)$$
24		df-tau	$$⊢\mathrm{\tau }=inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)$$
25	23 24	breqtrri	$$⊢2\mathrm{\pi }\le \mathrm{\tau }$$
26		infrecl	$$⊢\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\subseteq ℝ\wedge {ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\ne \varnothing \wedge \exists x\in ℝ\forall y\in \left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)x\le y\right)\to inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)\in ℝ$$
27	14 26	ax-mp	$$⊢inf\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)\in ℝ$$
28	24 27	eqeltri	$$⊢\mathrm{\tau }\in ℝ$$
29	28 17	letri3i	$$⊢\mathrm{\tau }=2\mathrm{\pi }\leftrightarrow \left(\mathrm{\tau }\le 2\mathrm{\pi }\wedge 2\mathrm{\pi }\le \mathrm{\tau }\right)$$
30	1 25 29	mpbir2an	$$⊢\mathrm{\tau }=2\mathrm{\pi }$$