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

Definition df-pi 15175
Description: Define the constant pi, π = 3.14159..., which is the smallest positive number whose sine is zero. Definition of π in [Gleason] p. 311. (Contributed by Paul Chapman, 23-Jan-2008.) (Revised by AV, 14-Sep-2020.)
Assertion
Ref Expression
df-pi π = inf((ℝ+ ∩ (sin “ {0})), ℝ, < )

Detailed syntax breakdown of Definition df-pi
StepHypRef Expression
1 cpi 15169 . 2 class π
2 crp 12112 . . . 4 class +
3 csin 15166 . . . . . 6 class sin
43ccnv 5341 . . . . 5 class sin
5 cc0 10252 . . . . . 6 class 0
65csn 4397 . . . . 5 class {0}
74, 6cima 5345 . . . 4 class (sin “ {0})
82, 7cin 3797 . . 3 class (ℝ+ ∩ (sin “ {0}))
9 cr 10251 . . 3 class
10 clt 10391 . . 3 class <
118, 9, 10cinf 8616 . 2 class inf((ℝ+ ∩ (sin “ {0})), ℝ, < )
121, 11wceq 1658 1 wff π = inf((ℝ+ ∩ (sin “ {0})), ℝ, < )
Colors of variables: wff setvar class
This definition is referenced by:  pilem2  24605  pilem3  24606  pilem3OLD  24607
  Copyright terms: Public domain W3C validator