MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pi Unicode version

Definition df-pi 12228
Description: Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (We use the inverse of of less-than, " `'  <", to turn supremum into infimum; currently we don't have infimum defined separately.) (Contributed by Paul Chapman, 23-Jan-2008.)
Assertion
Ref Expression
df-pi  |-  pi  =  sup ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )

Detailed syntax breakdown of Definition df-pi
StepHypRef Expression
1 cpi 12222 . 2  class  pi
2 crp 10233 . . . 4  class  RR+
3 csin 12219 . . . . . 6  class  sin
43ccnv 4579 . . . . 5  class  `' sin
5 cc0 8617 . . . . . 6  class  0
65csn 3544 . . . . 5  class  { 0 }
74, 6cima 4583 . . . 4  class  ( `' sin " { 0 } )
82, 7cin 3077 . . 3  class  ( RR+  i^i  ( `' sin " {
0 } ) )
9 cr 8616 . . 3  class  RR
10 clt 8747 . . . 4  class  <
1110ccnv 4579 . . 3  class  `'  <
128, 9, 11csup 7077 . 2  class  sup (
( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
131, 12wceq 1619 1  wff  pi  =  sup ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  `'  <  )
Colors of variables: wff set class
This definition is referenced by:  pilem2  19660  pilem3  19661
  Copyright terms: Public domain W3C validator