Definition df-tau

Description: Define the circle constant tau, _tau = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including _tau , a three-legged variant of _pi , or 2pi . Note the difference between this constant tau and the formula variable ta . Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018) (Revised by AV, 1-Oct-2020)

	Ref	Expression
Assertion	df-tau	$$⊢\mathrm{\tau }=sup\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctau	$$class\mathrm{\tau }$$
1		crp	$$class{ℝ}^{+}$$
2		ccos	$$class\cos$$
3	2	ccnv	$$class{\cos }^{-1}$$
4		c1	$$class1$$
5	4	csn	$$class\left\{1\right\}$$
6	3 5	cima	$$class{\cos }^{-1}\left[\left\{1\right\}\right]$$
7	1 6	cin	$$class\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right]\right)$$
8		cr	$$classℝ$$
9		clt	$$class<$$
10	7 8 9	cinf	$$classsup\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)$$
11	0 10	wceq	$$wff\mathrm{\tau }=sup\left({ℝ}^{+}\cap {\cos }^{-1}\left[\left\{1\right\}\right],ℝ,<\right)$$