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	⊢ τ = inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctau	⊢ τ
1		crp	⊢ ℝ+
2		ccos	⊢ cos
3	2	ccnv	⊢ ◡ cos
4		c1	⊢ 1
5	4	csn	⊢ { 1 }
6	3 5	cima	⊢ ( ◡ cos “ { 1 } )
7	1 6	cin	⊢ ( ℝ+ ∩ ( ◡ cos “ { 1 } ) )
8		cr	⊢ ℝ
9		clt	⊢ <
10	7 8 9	cinf	⊢ inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < )
11	0 10	wceq	⊢ τ = inf ( ( ℝ+ ∩ ( ◡ cos “ { 1 } ) ) , ℝ , < )