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

Definition df-tau 15764
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 . 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 15763 . 2 class τ
2 crp 12586 . . . 4 class +
3 ccos 15626 . . . . . 6 class cos
43ccnv 5550 . . . . 5 class cos
5 c1 10730 . . . . . 6 class 1
65csn 4541 . . . . 5 class {1}
74, 6cima 5554 . . . 4 class (cos “ {1})
82, 7cin 3865 . . 3 class (ℝ+ ∩ (cos “ {1}))
9 cr 10728 . . 3 class
10 clt 10867 . . 3 class <
118, 9, 10cinf 9057 . 2 class inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
121, 11wceq 1543 1 wff τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
Colors of variables: wff setvar class
This definition is referenced by:  taupilem2  35227  taupi  35228
  Copyright terms: Public domain W3C validator