Metamath Proof Explorer

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 
|- _tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctau 
 |-  _tau
1 crp 
 |-  RR+
2 ccos 
 |-  cos
3 2 ccnv 
 |-  `' cos
4 c1 
 |-  1
5 4 csn 
 |-  { 1 }
6 3 5 cima 
 |-  ( `' cos " { 1 } )
7 1 6 cin 
 |-  ( RR+ i^i ( `' cos " { 1 } ) )
8 cr 
 |-  RR
9 clt 
 |-  <
10 7 8 9 cinf 
 |-  inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )
11 0 10 wceq 
 |-  _tau = inf ( ( RR+ i^i ( `' cos " { 1 } ) ) , RR , < )