Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tau Structured version   Visualization version   GIF version

Definition df-tau 15565
 Description: Define the circle constant 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 τ, a three-legged variant of π, or 2π. Note the difference between this constant τ and the formula variable 𝜏. 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.)
Assertion
Ref Expression
df-tau τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )

Detailed syntax breakdown of Definition df-tau
StepHypRef Expression
1 ctau 15564 . 2 class τ
2 crp 12394 . . . 4 class +
3 ccos 15427 . . . . . 6 class cos
43ccnv 5521 . . . . 5 class cos
5 c1 10542 . . . . . 6 class 1
65csn 4527 . . . . 5 class {1}
74, 6cima 5525 . . . 4 class (cos “ {1})
82, 7cin 3881 . . 3 class (ℝ+ ∩ (cos “ {1}))
9 cr 10540 . . 3 class
10 clt 10679 . . 3 class <
118, 9, 10cinf 8904 . 2 class inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
121, 11wceq 1538 1 wff τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
 Colors of variables: wff setvar class This definition is referenced by:  taupilem2  34803  taupi  34804
 Copyright terms: Public domain W3C validator