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

Definition df-pi 14104
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 14097 . 2  class  pi
2 crp 11302 . . . 4  class  RR+
3 csin 14094 . . . . . 6  class  sin
43ccnv 4853 . . . . 5  class  `' sin
5 cc0 9538 . . . . . 6  class  0
65csn 4002 . . . . 5  class  { 0 }
74, 6cima 4857 . . . 4  class  ( `' sin " { 0 } )
82, 7cin 3441 . . 3  class  ( RR+  i^i  ( `' sin " {
0 } ) )
9 cr 9537 . . 3  class  RR
10 clt 9674 . . 3  class  <
118, 9, 10cinf 7961 . 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  23263  pilem3  23265
  Copyright terms: Public domain W3C validator