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 16092
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 16091 . 2 class τ
2 crp 12922 . . . 4 class +
3 ccos 15954 . . . . . 6 class cos
43ccnv 5637 . . . . 5 class cos
5 c1 11059 . . . . . 6 class 1
65csn 4591 . . . . 5 class {1}
74, 6cima 5641 . . . 4 class (cos “ {1})
82, 7cin 3914 . . 3 class (ℝ+ ∩ (cos “ {1}))
9 cr 11057 . . 3 class
10 clt 11196 . . 3 class <
118, 9, 10cinf 9384 . 2 class inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
121, 11wceq 1542 1 wff τ = inf((ℝ+ ∩ (cos “ {1})), ℝ, < )
Colors of variables: wff setvar class
This definition is referenced by:  taupilem2  35822  taupi  35823
  Copyright terms: Public domain W3C validator