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

Definition df-pi 14064
Description: Define pi = 3.14159..., which is the smallest positive number whose sine is zero. Definition of pi in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.)
Assertion
Ref Expression
df-pi  |-  pi  = inf ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  <  )

Detailed syntax breakdown of Definition df-pi
StepHypRef Expression
1 cpi 14057 . 2  class  pi
2 crp 11248 . . . 4  class  RR+
3 csin 14054 . . . . . 6  class  sin
43ccnv 4790 . . . . 5  class  `' sin
5 cc0 9485 . . . . . 6  class  0
65csn 3936 . . . . 5  class  { 0 }
74, 6cima 4794 . . . 4  class  ( `' sin " { 0 } )
82, 7cin 3373 . . 3  class  ( RR+  i^i  ( `' sin " {
0 } ) )
9 cr 9484 . . 3  class  RR
10 clt 9621 . . 3  class  <
118, 9, 10cinf 7903 . 2  class inf ( (
RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  <  )
121, 11wceq 1437 1  wff  pi  = inf ( ( RR+  i^i  ( `' sin " { 0 } ) ) ,  RR ,  <  )
Colors of variables: wff setvar class
This definition is referenced by:  pilem2  23344  pilem3  23346
  Copyright terms: Public domain W3C validator